mo-sb2

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

((([/][/])()))

Proof:

Hyp	Ref	Line	Expr
	df-∃mo-alt3	1	((([/])()))
1	spec	2	([/](([/])()))
	eqt<	3	(()(()()))
	eq-sb>b	4	(()([/]))
4	bi>	5	(()([/]))
4	bi.bldan<d	6	(()(([/])([/][/])))
3, 6	bi.bldim<>d	7	(()((([/])())(([/][/])())))
7	bi.bldald	8	(()((([/])())(([/][/])())))
	ax17-bv	9	( bound in ())
	bv-sbb-dv	10	( bound in [/])
	bv-sbb-dv	11	( bound in [/])
10, 11	bv-∧	12	( bound in ([/][/]))
9, 12	bv-→	13	( bound in (([/][/])()))
13	bv-∀	14	( bound in (([/][/])()))
8, 14	sb-xplw	15	([/](([/])())(([/][/])()))
2, 15	brpi22	16	((([/][/])()))
16	spec	17	([/](([/][/])()))
	eqt>	18	(()(()()))
	eq-sb>b	19	(()([/][/][/]))
	sbco2w	20	([/][/][/])
20	ax1	21	(()([/][/][/]))
19, 21	bitrd	22	(()([/][/]))
22	bi>	23	(()([/][/]))
22	bi.bldan>d	24	(()(([/][/])([/][/])))
18, 24	bi.bldim<>d	25	(()((([/][/])())(([/][/])())))
	ax17-bv	26	( bound in (([/][/])()))
25, 26	sb-xplw	27	([/](([/][/])())(([/][/])()))
17, 27	brpi22	28	((([/][/])()))