fv.eqex

Theorem.

Arguments:

(sv), (pr),

Hypotheses:

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	df-Bvp	2	()
	spec-ex	3	()
	df-ex	4	()
2	con	5	()
5	im.bldal	6	()
6	con	7	()
	ax6	8	()
7, 8	syl	9	()
4, 9	brpi21	10	()
3, 10	>bii	11	()