Theorem ax11el 2194

Description: Basis step for constructing a substitution instance of ax-11o 2141 without using ax-11o 2141. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax11el	|- (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w))))

Proof of Theorem ax11el

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26 1593	. . 3 |- (A.x(x = z /\ x = w) <-> (A.x x = z /\ A.x x = w))
2		elequ1 1713	. . . . . . . . 9 |- (x = y -> (x e. x <-> y e. x))
3		elequ2 1715	. . . . . . . . 9 |- (x = y -> (y e. x <-> y e. y))
4	2, 3	bitrd 244	. . . . . . . 8 |- (x = y -> (x e. x <-> y e. y))
5	4	adantl 452	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (x e. x <-> y e. y))
6		ax-17 1616	. . . . . . . . . 10 |- (v e. v -> A.x v e. v)
7		ax-17 1616	. . . . . . . . . 10 |- (y e. y -> A.v y e. y)
8		elequ1 1713	. . . . . . . . . . 11 |- (v = y -> (v e. v <-> y e. v))
9		elequ2 1715	. . . . . . . . . . 11 |- (v = y -> (y e. v <-> y e. y))
10	8, 9	bitrd 244	. . . . . . . . . 10 |- (v = y -> (v e. v <-> y e. y))
11	6, 7, 10	dvelimf-o 2180	. . . . . . . . 9 |- (-. A.x x = y -> (y e. y -> A.x y e. y))
12	4	biimprcd 216	. . . . . . . . . 10 |- (y e. y -> (x = y -> x e. x))
13	12	alimi 1559	. . . . . . . . 9 |- (A.x y e. y -> A.x(x = y -> x e. x))
14	11, 13	syl6 29	. . . . . . . 8 |- (-. A.x x = y -> (y e. y -> A.x(x = y -> x e. x)))
15	14	adantr 451	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (y e. y -> A.x(x = y -> x e. x)))
16	5, 15	sylbid 206	. . . . . 6 |- ((-. A.x x = y /\ x = y) -> (x e. x -> A.x(x = y -> x e. x)))
17	16	adantl 452	. . . . 5 |- ((A.x(x = z /\ x = w) /\ (-. A.x x = y /\ x = y)) -> (x e. x -> A.x(x = y -> x e. x)))
18		elequ1 1713	. . . . . . . . 9 |- (x = z -> (x e. x <-> z e. x))
19		elequ2 1715	. . . . . . . . 9 |- (x = w -> (z e. x <-> z e. w))
20	18, 19	sylan9bb 680	. . . . . . . 8 |- ((x = z /\ x = w) -> (x e. x <-> z e. w))
21	20	sps-o 2159	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (x e. x <-> z e. w))
22		nfa1-o 2166	. . . . . . . 8 |- F/xA.x(x = z /\ x = w)
23	21	imbi2d 307	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> ((x = y -> x e. x) <-> (x = y -> z e. w)))
24	22, 23	albid 1772	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (A.x(x = y -> x e. x) <-> A.x(x = y -> z e. w)))
25	21, 24	imbi12d 311	. . . . . 6 |- (A.x(x = z /\ x = w) -> ((x e. x -> A.x(x = y -> x e. x)) <-> (z e. w -> A.x(x = y -> z e. w))))
26	25	adantr 451	. . . . 5 |- ((A.x(x = z /\ x = w) /\ (-. A.x x = y /\ x = y)) -> ((x e. x -> A.x(x = y -> x e. x)) <-> (z e. w -> A.x(x = y -> z e. w))))
27	17, 26	mpbid 201	. . . 4 |- ((A.x(x = z /\ x = w) /\ (-. A.x x = y /\ x = y)) -> (z e. w -> A.x(x = y -> z e. w)))
28	27	exp32 588	. . 3 |- (A.x(x = z /\ x = w) -> (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w)))))
29	1, 28	sylbir 204	. 2 |- ((A.x x = z /\ A.x x = w) -> (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w)))))
30		elequ1 1713	. . . . . . 7 |- (x = y -> (x e. w <-> y e. w))
31	30	ad2antll 709	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w <-> y e. w))
32		ax-15 2143	. . . . . . . . 9 |- (-. A.x x = y -> (-. A.x x = w -> (y e. w -> A.x y e. w)))
33	32	impcom 419	. . . . . . . 8 |- ((-. A.x x = w /\ -. A.x x = y) -> (y e. w -> A.x y e. w))
34	33	adantrr 697	. . . . . . 7 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y e. w -> A.x y e. w))
35	30	biimprcd 216	. . . . . . . 8 |- (y e. w -> (x = y -> x e. w))
36	35	alimi 1559	. . . . . . 7 |- (A.x y e. w -> A.x(x = y -> x e. w))
37	34, 36	syl6 29	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y e. w -> A.x(x = y -> x e. w)))
38	31, 37	sylbid 206	. . . . 5 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w -> A.x(x = y -> x e. w)))
39	38	adantll 694	. . . 4 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (x e. w -> A.x(x = y -> x e. w)))
40		elequ1 1713	. . . . . . 7 |- (x = z -> (x e. w <-> z e. w))
41	40	sps-o 2159	. . . . . 6 |- (A.x x = z -> (x e. w <-> z e. w))
42	41	imbi2d 307	. . . . . . 7 |- (A.x x = z -> ((x = y -> x e. w) <-> (x = y -> z e. w)))
43	42	dral2-o 2181	. . . . . 6 |- (A.x x = z -> (A.x(x = y -> x e. w) <-> A.x(x = y -> z e. w)))
44	41, 43	imbi12d 311	. . . . 5 |- (A.x x = z -> ((x e. w -> A.x(x = y -> x e. w)) <-> (z e. w -> A.x(x = y -> z e. w))))
45	44	ad2antrr 706	. . . 4 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> ((x e. w -> A.x(x = y -> x e. w)) <-> (z e. w -> A.x(x = y -> z e. w))))
46	39, 45	mpbid 201	. . 3 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z e. w -> A.x(x = y -> z e. w)))
47	46	exp32 588	. 2 |- ((A.x x = z /\ -. A.x x = w) -> (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w)))))
48		elequ2 1715	. . . . . . 7 |- (x = y -> (z e. x <-> z e. y))
49	48	ad2antll 709	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x <-> z e. y))
50		ax-15 2143	. . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z e. y -> A.x z e. y)))
51	50	imp 418	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (z e. y -> A.x z e. y))
52	51	adantrr 697	. . . . . . 7 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. y -> A.x z e. y))
53	48	biimprcd 216	. . . . . . . 8 |- (z e. y -> (x = y -> z e. x))
54	53	alimi 1559	. . . . . . 7 |- (A.x z e. y -> A.x(x = y -> z e. x))
55	52, 54	syl6 29	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. y -> A.x(x = y -> z e. x)))
56	49, 55	sylbid 206	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x -> A.x(x = y -> z e. x)))
57	56	adantlr 695	. . . 4 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z e. x -> A.x(x = y -> z e. x)))
58	19	sps-o 2159	. . . . . 6 |- (A.x x = w -> (z e. x <-> z e. w))
59	58	imbi2d 307	. . . . . . 7 |- (A.x x = w -> ((x = y -> z e. x) <-> (x = y -> z e. w)))
60	59	dral2-o 2181	. . . . . 6 |- (A.x x = w -> (A.x(x = y -> z e. x) <-> A.x(x = y -> z e. w)))
61	58, 60	imbi12d 311	. . . . 5 |- (A.x x = w -> ((z e. x -> A.x(x = y -> z e. x)) <-> (z e. w -> A.x(x = y -> z e. w))))
62	61	ad2antlr 707	. . . 4 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> ((z e. x -> A.x(x = y -> z e. x)) <-> (z e. w -> A.x(x = y -> z e. w))))
63	57, 62	mpbid 201	. . 3 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z e. w -> A.x(x = y -> z e. w)))
64	63	exp32 588	. 2 |- ((-. A.x x = z /\ A.x x = w) -> (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w)))))
65		a9ev 1656	. . . . 5 |- E.u u = w
66		a9ev 1656	. . . . . . 7 |- E.v v = z
67		ax-1 6	. . . . . . . . . . 11 |- (v e. u -> (x = y -> v e. u))
68	67	alrimiv 1631	. . . . . . . . . 10 |- (v e. u -> A.x(x = y -> v e. u))
69		elequ1 1713	. . . . . . . . . . . . 13 |- (v = z -> (v e. u <-> z e. u))
70		elequ2 1715	. . . . . . . . . . . . 13 |- (u = w -> (z e. u <-> z e. w))
71	69, 70	sylan9bb 680	. . . . . . . . . . . 12 |- ((v = z /\ u = w) -> (v e. u <-> z e. w))
72	71	adantl 452	. . . . . . . . . . 11 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (v e. u <-> z e. w))
73		dveeq2-o 2184	. . . . . . . . . . . . . . 15 |- (-. A.x x = z -> (v = z -> A.x v = z))
74		dveeq2-o 2184	. . . . . . . . . . . . . . 15 |- (-. A.x x = w -> (u = w -> A.x u = w))
75	73, 74	im2anan9 808	. . . . . . . . . . . . . 14 |- ((-. A.x x = z /\ -. A.x x = w) -> ((v = z /\ u = w) -> (A.x v = z /\ A.x u = w)))
76	75	imp 418	. . . . . . . . . . . . 13 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (A.x v = z /\ A.x u = w))
77		19.26 1593	. . . . . . . . . . . . 13 |- (A.x(v = z /\ u = w) <-> (A.x v = z /\ A.x u = w))
78	76, 77	sylibr 203	. . . . . . . . . . . 12 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> A.x(v = z /\ u = w))
79		nfa1-o 2166	. . . . . . . . . . . . 13 |- F/xA.x(v = z /\ u = w)
80	71	sps-o 2159	. . . . . . . . . . . . . 14 |- (A.x(v = z /\ u = w) -> (v e. u <-> z e. w))
81	80	imbi2d 307	. . . . . . . . . . . . 13 |- (A.x(v = z /\ u = w) -> ((x = y -> v e. u) <-> (x = y -> z e. w)))
82	79, 81	albid 1772	. . . . . . . . . . . 12 |- (A.x(v = z /\ u = w) -> (A.x(x = y -> v e. u) <-> A.x(x = y -> z e. w)))
83	78, 82	syl 15	. . . . . . . . . . 11 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (A.x(x = y -> v e. u) <-> A.x(x = y -> z e. w)))
84	72, 83	imbi12d 311	. . . . . . . . . 10 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> ((v e. u -> A.x(x = y -> v e. u)) <-> (z e. w -> A.x(x = y -> z e. w))))
85	68, 84	mpbii 202	. . . . . . . . 9 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (z e. w -> A.x(x = y -> z e. w)))
86	85	exp32 588	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = w) -> (v = z -> (u = w -> (z e. w -> A.x(x = y -> z e. w)))))
87	86	exlimdv 1636	. . . . . . 7 |- ((-. A.x x = z /\ -. A.x x = w) -> (E.v v = z -> (u = w -> (z e. w -> A.x(x = y -> z e. w)))))
88	66, 87	mpi 16	. . . . . 6 |- ((-. A.x x = z /\ -. A.x x = w) -> (u = w -> (z e. w -> A.x(x = y -> z e. w))))
89	88	exlimdv 1636	. . . . 5 |- ((-. A.x x = z /\ -. A.x x = w) -> (E.u u = w -> (z e. w -> A.x(x = y -> z e. w))))
90	65, 89	mpi 16	. . . 4 |- ((-. A.x x = z /\ -. A.x x = w) -> (z e. w -> A.x(x = y -> z e. w)))
91	90	a1d 22	. . 3 |- ((-. A.x x = z /\ -. A.x x = w) -> (x = y -> (z e. w -> A.x(x = y -> z e. w))))
92	91	a1d 22	. 2 |- ((-. A.x x = z /\ -. A.x x = w) -> (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w)))))
93	29, 47, 64, 92	4cases 915	1 |- (-. A.x x = y -> (x = y -> (z e. w -> A.x(x = y -> z e. w))))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-4 2135  ax-5o 2136  ax-6o 2137  ax-10o 2139  ax-12o 2142  ax-15 2143

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by: (None)