cbv-∃1

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

(()())

( bound in )

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
		3	( bound in )
3	chvar-∃1	4	([/])
1, 2	sb-xpl	5	([/])
5	eqt-∃1-i	6	([/])
4, 6	bitr	7	()