Theorem ax11el 1406

Description: Basis step for constructing a substitution instance of ax-11o 1260 without using ax-11o 1260. Atomic formula for membership predicate.

Assertion

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

Proof of Theorem ax11el

Step	Hyp	Ref	Expression
1		19.26 1108	. . 3 |- (A.x(x = z /\ x = w) <-> (A.x x = z /\ A.x x = w))
2		elequ1 1178	. . . . . . . . 9 |- (x = y -> (x e. x <-> y e. x))
3		elequ2 1179	. . . . . . . . 9 |- (x = y -> (y e. x <-> y e. y))
4	2, 3	bitrd 539	. . . . . . . 8 |- (x = y -> (x e. x <-> y e. y))
5	4	adantl 397	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (x e. x <-> y e. y))
6		ax-17 1012	. . . . . . . . . 10 |- (v e. v -> A.x v e. v)
7		ax-17 1012	. . . . . . . . . 10 |- (y e. y -> A.v y e. y)
8		elequ1 1178	. . . . . . . . . . 11 |- (v = y -> (v e. v <-> y e. v))
9		elequ2 1179	. . . . . . . . . . 11 |- (v = y -> (y e. v <-> y e. y))
10	8, 9	bitrd 539	. . . . . . . . . 10 |- (v = y -> (v e. v <-> y e. y))
11	6, 7, 10	dvelimfALT 1195	. . . . . . . . 9 |- (-. A.x x = y -> (y e. y -> A.x y e. y))
12	4	biimprcd 163	. . . . . . . . . 10 |- (y e. y -> (x = y -> x e. x))
13	12	19.20i 1033	. . . . . . . . 9 |- (A.x y e. y -> A.x(x = y -> x e. x))
14	11, 13	syl6 22	. . . . . . . 8 |- (-. A.x x = y -> (y e. y -> A.x(x = y -> x e. x)))
15	14	adantr 398	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (y e. y -> A.x(x = y -> x e. x)))
16	5, 15	sylbid 210	. . . . . 6 |- ((-. A.x x = y /\ x = y) -> (x e. x -> A.x(x = y -> x e. x)))
17	16	adantl 397	. . . . 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 1178	. . . . . . . . 9 |- (x = z -> (x e. x <-> z e. x))
19		elequ2 1179	. . . . . . . . 9 |- (x = w -> (z e. x <-> z e. w))
20	18, 19	sylan9bb 551	. . . . . . . 8 |- ((x = z /\ x = w) -> (x e. x <-> z e. w))
21	20	a4s 1025	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (x e. x <-> z e. w))
22		hba1 1044	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> A.xA.x(x = z /\ x = w))
23	21	imbi2d 623	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> ((x = y -> x e. x) <-> (x = y -> z e. w)))
24	22, 23	albid 1145	. . . . . . 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 637	. . . . . 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 398	. . . . 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 202	. . . 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 386	. . 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 208	. 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 1178	. . . . . . 7 |- (x = y -> (x e. w <-> y e. w))
31	30	ad2antll 416	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w <-> y e. w))
32		ax-15 1402	. . . . . . . . 9 |- (-. A.x x = y -> (-. A.x x = w -> (y e. w -> A.x y e. w)))
33	32	impcom 358	. . . . . . . 8 |- ((-. A.x x = w /\ -. A.x x = y) -> (y e. w -> A.x y e. w))
34	33	adantrr 404	. . . . . . 7 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y e. w -> A.x y e. w))
35	30	biimprcd 163	. . . . . . . 8 |- (y e. w -> (x = y -> x e. w))
36	35	19.20i 1033	. . . . . . 7 |- (A.x y e. w -> A.x(x = y -> x e. w))
37	34, 36	syl6 22	. . . . . 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 210	. . . . 5 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w -> A.x(x = y -> x e. w)))
39	38	adantll 401	. . . 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 1178	. . . . . . 7 |- (x = z -> (x e. w <-> z e. w))
41	40	a4s 1025	. . . . . 6 |- (A.x x = z -> (x e. w <-> z e. w))
42	41	imbi2d 623	. . . . . . 7 |- (A.x x = z -> ((x = y -> x e. w) <-> (x = y -> z e. w)))
43	42	dral2 1197	. . . . . 6 |- (A.x x = z -> (A.x(x = y -> x e. w) <-> A.x(x = y -> z e. w)))
44	41, 43	imbi12d 637	. . . . 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 413	. . . 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 202	. . 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 386	. 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 1179	. . . . . . 7 |- (x = y -> (z e. x <-> z e. y))
49	48	ad2antll 416	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x <-> z e. y))
50		ax-15 1402	. . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z e. y -> A.x z e. y)))
51	50	imp 357	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (z e. y -> A.x z e. y))
52	51	adantrr 404	. . . . . . 7 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. y -> A.x z e. y))
53	48	biimprcd 163	. . . . . . . 8 |- (z e. y -> (x = y -> z e. x))
54	53	19.20i 1033	. . . . . . 7 |- (A.x z e. y -> A.x(x = y -> z e. x))
55	52, 54	syl6 22	. . . . . 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 210	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x -> A.x(x = y -> z e. x)))
57	56	adantlr 402	. . . 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	a4s 1025	. . . . . 6 |- (A.x x = w -> (z e. x <-> z e. w))
59	58	imbi2d 623	. . . . . . 7 |- (A.x x = w -> ((x = y -> z e. x) <-> (x = y -> z e. w)))
60	59	dral2 1197	. . . . . 6 |- (A.x x = w -> (A.x(x = y -> z e. x) <-> A.x(x = y -> z e. w)))
61	58, 60	imbi12d 637	. . . . 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 414	. . . 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 202	. . 3 |- ((