∃1→∃mo-0

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	df-∃1-alt	2	((()))
	bi>	3	((())(()))
3	im.bldal	4	((())(()))
4	im.bldex	5	((())(()))
2, 5	brpi21	6	((()))