equf

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

( bound in )

Assertions:

(()(()()))

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 (()()))
	df-equ	6	(()(()()))
	ax17-bv	7	( bound in (()()))
	eqt<	8	(()(()()))
	eqt<	9	(()(()()))
8, 9	bi.bldbi<>d	10	(()((()())(()())))
5, 7, 10	cbval	11	((()())(()()))
6, 11	><bitr	12	(()(()()))