# 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 ) )`
` |-  ( ( -. 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 ) ) )`
` |-  ( ( -. 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 ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( -. 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 ) )`
` |-  ( ( -. 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 ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( -. 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 ) )`
` |-  ( ( -. 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 ) ) )`
` |-  ( ( ( -. 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 ) ) ) )`
` |-  ( ( ( -. 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 ) )`
` |-  ( ( ( -. 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 ) ) ) )`