df-∃1-alt3

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

(((())))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	df-∃1-alt2	2	(((([/])())))
1	df-∃mo-alt0	3	((())(([/])()))
3	bi.bldan>	4	(((()))((([/])())))
2, 4	><bitr	5	(((())))