bv-→

Theorem.

Arguments:

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

Hypotheses:

( bound in )

( bound in )

Assertions:

( bound in ())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
		2	( bound in )
2	df-Bvp	3	()
1	df-Bvp	4	()
3, 4	fv-im	5	(()())
5	df-Bvp	6	( bound in ())