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 ) ) ) )