bv-∃mo

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

( bound in )

Proof:

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