df-∃mo-alt4

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Hypotheses:

(()())

( bound in )

Assertions:

((()()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
	ax17-bv	3	( bound in )
3	df-∃mo-alt3	4	((([/])()))
1, 2	sb-xpl	5	([/])
5	bi.bldan>	6	(([/])())
6	bi.bldim<	7	((([/])())(()()))
7	eqt-∀-i	8	((([/])())(()()))
8	eqt-∀-i	9	((([/])())(()()))
4, 9	bitr	10	((()()))