eqt-∃1-d

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

(())

( bound in )

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
		2	( bound in )
1	bi.bldbi<d	3	(((())(())))
2, 3	bi.bldald	4	(((())(())))
4	bi.bldexd	5	(((())(())))
	df-∃1	6	((()))
	df-∃1	7	((()))
5, 6, 7	<2bitrg	8	(())