df-∃mo-alt3

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

((([/])()))

Proof:

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