Theorem ax11el 1362

Description: Basis step for constructing a substitution instance of ax-11o 1216 without using ax-11o 1216. 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 1065	. . 3 |- (A.x(x = z /\ x = w) <-> (A.x x = z /\ A.x x = w))
2		elequ1 1134	. . . . . . . . 9 |- (x = y -> (x e. x <-> y e. x))
3		elequ2 1135	. . . . . . . . 9 |- (x = y -> (y e. x <-> y e. y))
4	2, 3	bitrd 527	. . . . . . . 8 |- (x = y -> (x e. x <-> y e. y))
5	4	adantl 388	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (x e. x <-> y e. y))
6		ax-17 969	. . . . . . . . . 10 |- (v e. v -> A.x v e. v)
7		ax-17 969	. . . . . . . . . 10 |- (y e. y -> A.v y e. y)
8		elequ1 1134	. . . . . . . . . . 11 |- (v = y -> (v e. v <-> y e. v))
9		elequ2 1135	. . . . . . . . . . 11 |- (v = y -> (y e. v <-> y e. y))
10	8, 9	bitrd 527	. . . . . . . . . 10 |- (v = y -> (v e. v <-> y e. y))
11	6, 7, 10	dvelimfALT 1151	. . . . . . . . 9 |- (-. A.x x = y -> (y e. y -> A.x y e. y))
12	4	biimprcd 156	. . . . . . . . . 10 |- (y e. y -> (x = y -> x e. x))
13	12	19.20i 990	. . . . . . . . 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 389	. . . . . . 7 |- ((-. A.x x = y /\ x = y) -> (y e. y -> A.x(x = y -> x e. x)))
16	5, 15	sylbid 203	. . . . . 6 |- ((-. A.x x = y /\ x = y) -> (x e. x -> A.x(x = y -> x e. x)))
17	16	adantl 388	. . . . 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 1134	. . . . . . . . 9 |- (x = z -> (x e. x <-> z e. x))
19		elequ2 1135	. . . . . . . . 9 |- (x = w -> (z e. x <-> z e. w))
20	18, 19	sylan9bb 539	. . . . . . . 8 |- ((x = z /\ x = w) -> (x e. x <-> z e. w))
21	20	a4s 982	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (x e. x <-> z e. w))
22		hba1 1001	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> A.xA.x(x = z /\ x = w))
23	21	imbi2d 611	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> ((x = y -> x e. x) <-> (x = y -> z e. w)))
24	22, 23	albid 1102	. . . . . . 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 625	. . . . . 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 389	. . . . 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 195	. . . 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 377	. . 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 201	. 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 1134	. . . . . . 7 |- (x = y -> (x e. w <-> y e. w))
31	30	ad2antll 407	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w <-> y e. w))
32		ax-15 1358	. . . . . . . . 9 |- (-. A.x x = y -> (-. A.x x = w -> (y e. w -> A.x y e. w)))
33	32	impcom 351	. . . . . . . 8 |- ((-. A.x x = w /\ -. A.x x = y) -> (y e. w -> A.x y e. w))
34	33	adantrr 395	. . . . . . 7 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y e. w -> A.x y e. w))
35	30	biimprcd 156	. . . . . . . 8 |- (y e. w -> (x = y -> x e. w))
36	35	19.20i 990	. . . . . . 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 203	. . . . 5 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x e. w -> A.x(x = y -> x e. w)))
39	38	adantll 392	. . . 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 1134	. . . . . . 7 |- (x = z -> (x e. w <-> z e. w))
41	40	a4s 982	. . . . . 6 |- (A.x x = z -> (x e. w <-> z e. w))
42	41	imbi2d 611	. . . . . . 7 |- (A.x x = z -> ((x = y -> x e. w) <-> (x = y -> z e. w)))
43	42	dral2 1153	. . . . . 6 |- (A.x x = z -> (A.x(x = y -> x e. w) <-> A.x(x = y -> z e. w)))
44	41, 43	imbi12d 625	. . . . 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 404	. . . 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 195	. . 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 377	. 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 1135	. . . . . . 7 |- (x = y -> (z e. x <-> z e. y))
49	48	ad2antll 407	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x <-> z e. y))
50		ax-15 1358	. . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z e. y -> A.x z e. y)))
51	50	imp 350	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (z e. y -> A.x z e. y))
52	51	adantrr 395	. . . . . . 7 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. y -> A.x z e. y))
53	48	biimprcd 156	. . . . . . . 8 |- (z e. y -> (x = y -> z e. x))
54	53	19.20i 990	. . . . . . 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 203	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z e. x -> A.x(x = y -> z e. x)))
57	56	adantlr 393	. . . 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 982	. . . . . 6 |- (A.x x = w -> (z e. x <-> z e. w))
59	58	imbi2d 611	. . . . . . 7 |- (A.x x = w -> ((x = y -> z e. x) <-> (x = y -> z e. w)))
60	59	dral2 1153	. . . . . 6 |- (A.x x = w -> (A.x(x = y -> z e. x) <-> A.x(x = y -> z e. w)))
61	58, 60	imbi12d 625	. . . . 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 405	. . . 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 195	. . 3 |- (((-. A.x x =