bv-∃1b

Theorem.

Arguments:

(sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

( bound in )

Proof:

Hyp	Ref	Line	Expr
	bv-∀b	1	( bound in (()))
1	bv-∃	2	( bound in (()))
2	df-Bvp	3	((())(()))
	df-∃1	4	((()))
4	eqt-∀-i	5	((()))
3, 4, 5	<imtr	6	()
6	df-Bvp	7	( bound in )