df-∃1-alt

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	df-∃1	2	((()))
	ax17eq	3	( bound in ())
1, 3	bv-↔	4	( bound in (()))
4	bv-∀	5	( bound in (()))
	ax17-bv	6	( bound in (()))
	eqt>	7	(()(()()))
7	bi.bldbi>d	8	(()((())(())))
8	bi.bldald	9	(()((())(())))
5, 6, 9	cbvex	10	((())(()))
2, 10	bitr	11	((()))