∃1→∃

Theorem.

Arguments:

(sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	ax17-bv	1	( bound in )
1	df-∃1-alt1	2	((([/]())))
	ex.andi	3	((([/]()))(([/]())))
2, 3	brpi21	4	((([/]())))
4	siman<	5	()