bv-∃

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

( bound in )

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	bv-¬	2	( bound in )
2	bv-∀	3	( bound in )
3	bv-¬	4	( bound in )
	df-ex	5	()
4, 5	bvdef	6	( bound in )