bv-=

Theorem.

Arguments:

(coll), (coll), (sv),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ),

Hypotheses:

( bound in )

( bound in )

Assertions:

( bound in ())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
		2	( bound in )
2	df-bvt	3	( bound in ())
1	df-bvt	4	( bound in ())
3, 4	bv-↔	5	( bound in (()()))
5	bv-∀	6	( bound in (()()))
	df-equ	7	(()(()()))
6, 7	bvdef	8	( bound in ())