Metamath Proof Explorer

Theorem ax12el

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

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

Proof

Step Hyp Ref Expression
1 19.26 
 |-  ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2 elequ1 
 |-  ( x = y -> ( x e. x <-> y e. x ) )
3 elequ2 
 |-  ( x = y -> ( y e. x <-> y e. y ) )
4 2 3 bitrd 
 |-  ( x = y -> ( x e. x <-> y e. y ) )
5 4 adantl 
 |-  ( ( -. A. x x = y /\ x = y ) -> ( x e. x <-> y e. y ) )
6 ax-5 
 |-  ( v e. v -> A. x v e. v )
7 ax-5 
 |-  ( y e. y -> A. v y e. y )
8 elequ1 
 |-  ( v = y -> ( v e. v <-> y e. v ) )
9 elequ2 
 |-  ( v = y -> ( y e. v <-> y e. y ) )
10 8 9 bitrd 
 |-  ( v = y -> ( v e. v <-> y e. y ) )
11 6 7 10 dvelimf-o 
 |-  ( -. A. x x = y -> ( y e. y -> A. x y e. y ) )
12 4 biimprcd 
 |-  ( y e. y -> ( x = y -> x e. x ) )
13 12 alimi 
 |-  ( A. x y e. y -> A. x ( x = y -> x e. x ) )
14 11 13 syl6 
 |-  ( -. A. x x = y -> ( y e. y -> A. x ( x = y -> x e. x ) ) )
15 14 adantr 
 |-  ( ( -. A. x x = y /\ x = y ) -> ( y e. y -> A. x ( x = y -> x e. x ) ) )
16 5 15 sylbid 
 |-  ( ( -. A. x x = y /\ x = y ) -> ( x e. x -> A. x ( x = y -> x e. x ) ) )
17 16 adantl 
 |-  ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( x e. x -> A. x ( x = y -> x e. x ) ) )
18 elequ1 
 |-  ( x = z -> ( x e. x <-> z e. x ) )
19 elequ2 
 |-  ( x = w -> ( z e. x <-> z e. w ) )
20 18 19 sylan9bb 
 |-  ( ( x = z /\ x = w ) -> ( x e. x <-> z e. w ) )
21 20 sps-o 
 |-  ( A. x ( x = z /\ x = w ) -> ( x e. x <-> z e. w ) )
22 nfa1-o 
 |-  F/ x A. x ( x = z /\ x = w )
23 21 imbi2d 
 |-  ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x e. x ) <-> ( x = y -> z e. w ) ) )
24 22 23 albid 
 |-  ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x e. x ) <-> A. x ( x = y -> z e. w ) ) )
25 21 24 imbi12d 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( x = y -> ( x e. w <-> y e. w ) )
31 30 ad2antll 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x e. w <-> y e. w ) )
32 ax-c14 
 |-  ( -. A. x x = y -> ( -. A. x x = w -> ( y e. w -> A. x y e. w ) ) )
33 32 impcom 
 |-  ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y e. w -> A. x y e. w ) )
34 33 adantrr 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y e. w -> A. x y e. w ) )
35 30 biimprcd 
 |-  ( y e. w -> ( x = y -> x e. w ) )
36 35 alimi 
 |-  ( A. x y e. w -> A. x ( x = y -> x e. w ) )
37 34 36 syl6 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y e. w -> A. x ( x = y -> x e. w ) ) )
38 31 37 sylbid 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x e. w -> A. x ( x = y -> x e. w ) ) )
39 38 adantll 
 |-  ( ( ( 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 
 |-  ( x = z -> ( x e. w <-> z e. w ) )
41 40 sps-o 
 |-  ( A. x x = z -> ( x e. w <-> z e. w ) )
42 41 imbi2d 
 |-  ( A. x x = z -> ( ( x = y -> x e. w ) <-> ( x = y -> z e. w ) ) )
43 42 dral2-o 
 |-  ( A. x x = z -> ( A. x ( x = y -> x e. w ) <-> A. x ( x = y -> z e. w ) ) )
44 41 43 imbi12d 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( x = y -> ( z e. x <-> z e. y ) )
49 48 ad2antll 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z e. x <-> z e. y ) )
50 ax-c14 
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( z e. y -> A. x z e. y ) ) )
51 50 imp 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z e. y -> A. x z e. y ) )
52 51 adantrr 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z e. y -> A. x z e. y ) )
53 48 biimprcd 
 |-  ( z e. y -> ( x = y -> z e. x ) )
54 53 alimi 
 |-  ( A. x z e. y -> A. x ( x = y -> z e. x ) )
55 52 54 syl6 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z e. y -> A. x ( x = y -> z e. x ) ) )
56 49 55 sylbid 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z e. x -> A. x ( x = y -> z e. x ) ) )
57 56 adantlr 
 |-  ( ( ( -. 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 
 |-  ( A. x x = w -> ( z e. x <-> z e. w ) )
59 58 imbi2d 
 |-  ( A. x x = w -> ( ( x = y -> z e. x ) <-> ( x = y -> z e. w ) ) )
60 59 dral2-o 
 |-  ( A. x x = w -> ( A. x ( x = y -> z e. x ) <-> A. x ( x = y -> z e. w ) ) )
61 58 60 imbi12d 
 |-  ( 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 
 |-  ( ( ( -. 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 
 |-  ( ( ( -. 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 
 |-  ( ( -. 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 ax6ev 
 |-  E. u u = w
66 ax6ev 
 |-  E. v v = z
67 ax-1 
 |-  ( v e. u -> ( x = y -> v e. u ) )
68 67 alrimiv 
 |-  ( v e. u -> A. x ( x = y -> v e. u ) )
69 elequ1 
 |-  ( v = z -> ( v e. u <-> z e. u ) )
70 elequ2 
 |-  ( u = w -> ( z e. u <-> z e. w ) )
71 69 70 sylan9bb 
 |-  ( ( v = z /\ u = w ) -> ( v e. u <-> z e. w ) )
72 71 adantl 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v e. u <-> z e. w ) )
73 dveeq2-o 
 |-  ( -. A. x x = z -> ( v = z -> A. x v = z ) )
74 dveeq2-o 
 |-  ( -. A. x x = w -> ( u = w -> A. x u = w ) )
75 73 74 im2anan9 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
76 75 imp 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
77 19.26 
 |-  ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
78 76 77 sylibr 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
79 nfa1-o 
 |-  F/ x A. x ( v = z /\ u = w )
80 71 sps-o 
 |-  ( A. x ( v = z /\ u = w ) -> ( v e. u <-> z e. w ) )
81 80 imbi2d 
 |-  ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v e. u ) <-> ( x = y -> z e. w ) ) )
82 79 81 albid 
 |-  ( A. x ( v = z /\ u = w ) -> ( A. x ( x = y -> v e. u ) <-> A. x ( x = y -> z e. w ) ) )
83 78 82 syl 
 |-  ( ( ( -. 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 
 |-  ( ( ( -. 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 
 |-  ( ( ( -. 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 
 |-  ( ( -. 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 
 |-  ( ( -. 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 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( u = w -> ( z e. w -> A. x ( x = y -> z e. w ) ) ) )
89 88 exlimdv 
 |-  ( ( -. 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 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( z e. w -> A. x ( x = y -> z e. w ) ) )
91 90 a1d 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( x = y -> ( z e. w -> A. x ( x = y -> z e. w ) ) ) )
92 91 a1d 
 |-  ( ( -. 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 
 |-  ( -. A. x x = y -> ( x = y -> ( z e. w -> A. x ( x = y -> z e. w ) ) ) )