sbid

Theorem.

Arguments:

(sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	df-sb	1	([/](()(())))
	ax9ex	2	()
2	jct<	3	((()))
	ax17-bv	4	( bound in )
4	exan>	5	((())(()))
3, 5	brpi22<	6	((()))
	eqcomi	7	(()())
7	im.bldan<	8	((())(()))
	spec-ex	9	((())(()))
8, 9	syl	10	((())(()))
	siman<	11	((())())
10, 11	jca	12	((())(()(())))
12	im.bldex	13	((())(()(())))
6, 13	syl	14	((()(())))
1, 14	brpi22<	15	([/])
4	dfsb-alt	16	([/](()(())))
	eqcomi	17	(()())
	ax4	18	((())(()))
18	im.bldan>	19	((()(()))(()(())))
17	im.bldan<	20	((()(()))(()(())))
	mpclosedan	21	((()(())))
19, 20, 21	3syl	22	((()(())))
4, 22	imgen<i	23	((()(())))
16, 23	syl	24	([/])
15, 24	>bii	25	([/])