df-∃1-alt2

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

(((([/])())))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	∃1→∃	2	()
1	∃1→∃mo-0	3	((()))
1	df-∃mo-alt0	4	((())(([/])()))
3, 4	brpi22	5	((([/])()))
2, 5	jca	6	(((([/])())))
	alexan<	7	(((([/])()))((([/])())))
	impexp	8	((([/])())(([/]())))
8	eqt-∀-i	9	((([/])())(([/]())))
1	imgen>	10	((([/]()))(([/]())))
9, 10	bitr	11	((([/])())(([/]())))
11	bi.bldan>	12	(((([/])()))((([/]()))))
	abai	13	((([/]()))((([/]()))))
12, 13	><bitr	14	(((([/])()))(([/]())))
14	eqt-∃-i	15	(((([/])()))(([/]())))
7, 15	brpi22	16	(((([/])()))(([/]())))
1	df-∃1-alt1	17	((([/]())))
16, 17	brpi22<	18	(((([/])())))
6, 18	>bii	19	(((([/])())))