bv-∃mob

Theorem.

Arguments:

(sv), (pr),

Assertions:

( bound in )

Proof:

Hyp	Ref	Line	Expr
	bv-∃b	1	( bound in )
	bv-∃1b	2	( bound in )
1, 2	bv-→	3	( bound in ())
	df-∃mo	4	(())
3, 4	bvdef	5	( bound in )