df-∃mo-alt2

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	df-∃mo	2	(())
	aln.ex	3	()
	<neg	4	((()))
4	im.bldal	5	((()))
	spec-ex	6	((())(()))
5, 6	syl	7	((()))
3, 7	brpi21<	8	((()))
1	∃1→∃mo-0	9	((()))
8, 9	ja-pre	10	(()(()))
1	df-∃1-alt3	11	(((())))
11	exp	12	(((())))
12	com12i	13	((())())
10, 13	>bii	14	(()(()))
2, 14	bitr	15	((()))