fv.eqal

Theorem.

Arguments:

(sv), (pr),

Hypotheses:

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	df-Bvp	2	()
	ax4	3	()
2, 3	>bii	4	()