df-∃1-alt5

Theorem.

Arguments:

(sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	ax17-bv	1	( bound in )
1	df-∃1-alt3	2	(((())))
1	df-∃mo-alt2	3	((()))
3	bi.bldan>	4	(()((())))
2, 4	><bitr	5	(())