chvar-∃1

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax17eq	2	( bound in ())
1, 2	bv-↔	3	( bound in (()))
3	chvar-∀	4	([/](())(()))
	sb-eqat<	5	([/]()())
5	sb-bi>	6	([/](())([/]()))
6	eqt-∀-i	7	([/](())([/]()))
4, 7	<>bitr	8	((())([/]()))
8	eqt-∃-i	9	((())([/]()))
	df-∃1	10	((()))
	df-∃1	11	([/]([/]()))
9, 10, 11	<2bitr	12	([/])