bv-sbb-dv

Theorem.

Arguments:

(st), (sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Assertions:

( bound in [/])

Proof:

Hyp	Ref	Line	Expr
	bv-∃b	1	( bound in (()))
	ax17-bv	2	( bound in ())
1, 2	bv-∧	3	( bound in (()(())))
3	bv-∃	4	( bound in (()(())))
	df-sb	5	([/](()(())))
4, 5	bvdef	6	( bound in [/])