df-∃1-alt4

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ), (, ),

Hypotheses:

(()())

Assertions:

(((()())))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
	df-∃1-alt5	2	(())
1	df-∃mo-alt4	3	((()()))
3	bi.bldan>	4	(()((()())))
2, 4	bitr	5	(((()())))