df-∃1-alt1

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

((([/]())))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	bv-sbb-dv	2	( bound in [/])
2	df-∃1-alt	3	([/]([/]()))
1	chvar-∃1	4	([/])
	com	5	(()())
5	bi.bldim>	6	(([/]())([/]()))
6	eqt-∀-i	7	(([/]())([/]()))
	dfsb-dval	8	([/][/](()[/]))
1	sbco2	9	([/][/][/])
	sbid	10	([/])
9, 10	bitr	11	([/][/])
8, 11	<>bitr	12	((()[/]))
7, 12	bi.bldan<>	13	((([/]()))(([/]())(()[/])))
	ancom	14	((([/]()))(([/]())))
	al.dfbi	15	(([/]())(([/]())(()[/])))
13, 14, 15	<2bitr	16	((([/]()))([/]()))
16	eqt-∃-i	17	((([/]()))([/]()))
3, 4, 17	<2bitr	18	((([/]())))