chvar-∃

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	bv-¬	2	( bound in )
	sb-neg	3	([/][/])
3	eqt-∀-i	4	([/][/])
2	chvar-∀	5	([/])
4, 5	<>bitr	6	([/])
6	bi.bldneg	7	([/])
	df-ex	8	([/][/])
	df-ex	9	()
7, 8, 9	<2bitr	10	([/])