df-∃mo-alt0

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax17eq	2	( bound in ())
1, 2	bv-→	3	( bound in (()))
3	bv-∀	4	( bound in (()))
	ax17-bv	5	( bound in (()))
	eqt>	6	(()(()()))
6	bi.bldim>d	7	(()((())(())))
7	bi.bldald	8	(()((())(())))
4, 5, 8	cbvex	9	((())(()))
	bv-sbb-dv	10	( bound in [/])
	ax17eq	11	( bound in ())
10, 11	bv-→	12	( bound in ([/]()))
	eq-sb>b	13	(()([/]))
13	bi<	14	(()([/]))
	ax8	15	(()(()()))
14, 15	syl34d	16	(()((())([/]())))
3, 12, 16	cbv3	17	((())([/]()))
17	anc<	18	((())((())([/]())))
3, 12	aaan	19	(((())([/]()))((())([/]())))
18, 19	brpi22<	20	((())((())([/]())))
	praeclarum	21	(((())([/]()))(([/])(()())))
	tr-an<	22	((()())())
21, 22	rpi33	23	(((())([/]()))(([/])()))
23	im.bldal	24	(((())([/]()))(([/])()))
24	im.bldal	25	(((())([/]()))(([/])()))
20, 25	syl	26	((())(([/])()))
26	imgen<i	27	((())(([/])()))
9, 27	brpi21<	28	((())(([/])()))
	al.imdi	29	(([/](()))([/](())))
29	im.bldal	30	(([/](()))([/](())))
30	ax7	31	(([/](()))([/](())))
	im.bldext	32	(([/](()))([/](())))
31, 32	syl	33	(([/](()))([/](())))
	bv-sbb-dv	34	( bound in [/])
34	df-Bvp	35	([/][/])
35	im.bldex	36	([/][/])
33, 36	rpi32	37	(([/](()))([/](())))
37	com12i	38	([/](([/](()))(())))
	impexp	39	((([/])())(([/]())))
	bcom12	40	((([/]()))([/](())))
39, 40	bitr	41	((([/])())([/](())))
41	eqt-∀-i	42	((([/])())([/](())))
42	eqt-∀-i	43	((([/])())([/](())))
38, 43	brpi32	44	([/]((([/])())(())))
	aln.ex	45	([/][/])
34	bv-¬	46	( bound in [/])
1	bv-¬	47	( bound in )
13	bi>	48	(()([/]))
48	eqcomi	49	(()([/]))
49	con	50	(()([/]))
46, 47, 50	cbv3	51	([/])
	<neg	52	((()))
52	im.bldal	53	((()))
	spec-ex	54	((())(()))
51, 53, 54	3syl	55	([/](()))
45, 55	brpi21<	56	([/](()))
56	ax1	57	([/]((([/])())(())))
44, 57	casei	58	((([/])())(()))
28, 58	>bii	59	((())(([/])()))