fv-exx

Theorem.

Arguments:

(sv), (pr),

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	fv-nalx	1	( bound in )
1	df-Bvp	2	()
	df-ex	3	()
3	eqt-∀-i	4	()
2, 3, 4	<imtr	5	()