dfsb-dvex

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

([/](()))

Proof:

Hyp	Ref	Line	Expr
	df-sb	1	([/](()(())))
	ax17-bv	2	( bound in ())
	eqt>	3	(()(()()))
3	bi.bldan<d	4	(()((())(())))
2, 4	bi.bldexd	5	(()((())(())))
5	bi>	6	(()((())(())))
5	bi<	7	(()((())(())))
	siman<	8	((()(()))())
	siman<	9	((()(()))())
	siman>	10	((()(()))(()))
	siman>	11	((()(()))(()))
6, 8	syl	12	((()(()))((())(())))
10, 12	mpd	13	((()(()))(()))
8, 13	jca	14	((()(()))(()(())))
7, 9	syl	15	((()(()))((())(())))
11, 15	mpd	16	((()(()))(()))
9, 16	jca	17	((()(()))(()(())))
14, 17	>bii	18	((()(()))(()(())))
18	eqt-∃-i	19	((()(()))(()(())))
	ax17-bv	20	( bound in (()))
20	exan>	21	((()(()))(()(())))
1, 19, 21	2bitr	22	([/](()(())))
	ax9ex	23	()
23	an-true<	24	((())(()(())))
22, 24	><bitr	25	([/](()))