bv-∃b

Theorem.

Arguments:

(sv), (pr),

Assertions:

( bound in )

Proof:

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