Metamath Proof Explorer

Theorem ax12eq

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

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

Proof

Step Hyp Ref Expression
1 19.26 
 |-  ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2 equid 
 |-  x = x
3 2 a1i 
 |-  ( x = y -> x = x )
4 3 ax-gen 
 |-  A. x ( x = y -> x = x )
5 4 a1i 
 |-  ( x = x -> A. x ( x = y -> x = x ) )
6 equequ1 
 |-  ( x = z -> ( x = x <-> z = x ) )
7 equequ2 
 |-  ( x = w -> ( z = x <-> z = w ) )
8 6 7 sylan9bb 
 |-  ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9 8 sps-o 
 |-  ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10 nfa1-o 
 |-  F/ x A. x ( x = z /\ x = w )
11 9 imbi2d 
 |-  ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12 10 11 albid 
 |-  ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13 9 12 imbi12d 
 |-  ( A. x ( x = z /\ x = w ) -> ( ( x = x -> A. x ( x = y -> x = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
14 13 adantr 
 |-  ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( x = x -> A. x ( x = y -> x = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
15 5 14 mpbii 
 |-  ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
16 15 exp32 
 |-  ( A. x ( x = z /\ x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
17 1 16 sylbir 
 |-  ( ( A. x x = z /\ A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
18 equequ1 
 |-  ( x = y -> ( x = w <-> y = w ) )
19 18 ad2antll 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20 axc9 
 |-  ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21 20 impcom 
 |-  ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22 21 adantrr 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23 equtrr 
 |-  ( y = w -> ( x = y -> x = w ) )
24 23 alimi 
 |-  ( A. x y = w -> A. x ( x = y -> x = w ) )
25 22 24 syl6 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x ( x = y -> x = w ) ) )
26 19 25 sylbid 
 |-  ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
27 26 adantll 
 |-  ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
28 equequ1 
 |-  ( x = z -> ( x = w <-> z = w ) )
29 28 sps-o 
 |-  ( A. x x = z -> ( x = w <-> z = w ) )
30 29 imbi2d 
 |-  ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31 30 dral2-o 
 |-  ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32 29 31 imbi12d 
 |-  ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33 32 ad2antrr 
 |-  ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
34 27 33 mpbid 
 |-  ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
35 34 exp32 
 |-  ( ( A. x x = z /\ -. A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
36 equequ2 
 |-  ( x = y -> ( z = x <-> z = y ) )
37 36 ad2antll 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38 axc9 
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39 38 imp 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40 39 adantrr 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x z = y ) )
41 36 biimprcd 
 |-  ( z = y -> ( x = y -> z = x ) )
42 41 alimi 
 |-  ( A. x z = y -> A. x ( x = y -> z = x ) )
43 40 42 syl6 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x ( x = y -> z = x ) ) )
44 37 43 sylbid 
 |-  ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
45 44 adantlr 
 |-  ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
46 7 sps-o 
 |-  ( A. x x = w -> ( z = x <-> z = w ) )
47 46 imbi2d 
 |-  ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48 47 dral2-o 
 |-  ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49 46 48 imbi12d 
 |-  ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50 49 ad2antlr 
 |-  ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
51 45 50 mpbid 
 |-  ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
52 51 exp32 
 |-  ( ( -. A. x x = z /\ A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
53 ax6ev 
 |-  E. u u = w
54 ax6ev 
 |-  E. v v = z
55 ax-1 
 |-  ( v = u -> ( x = y -> v = u ) )
56 55 alrimiv 
 |-  ( v = u -> A. x ( x = y -> v = u ) )
57 equequ1 
 |-  ( v = z -> ( v = u <-> z = u ) )
58 equequ2 
 |-  ( u = w -> ( z = u <-> z = w ) )
59 57 58 sylan9bb 
 |-  ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60 59 adantl 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61 dveeq2-o 
 |-  ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62 dveeq2-o 
 |-  ( -. A. x x = w -> ( u = w -> A. x u = w ) )
63 61 62 im2anan9 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
64 63 imp 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65 19.26 
 |-  ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
66 64 65 sylibr 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
67 nfa1-o 
 |-  F/ x A. x ( v = z /\ u = w )
68 59 sps-o 
 |-  ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69 68 imbi2d 
 |-  ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70 67 69 albid 
 |-  ( A. x ( v = z /\ u = w ) -> ( A. x ( x = y -> v = u ) <-> A. x ( x = y -> z = w ) ) )
71 66 70 syl 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x ( x = y -> v = u ) <-> A. x ( x = y -> z = w ) ) )
72 60 71 imbi12d 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( ( v = u -> A. x ( x = y -> v = u ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
73 56 72 mpbii 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
74 73 exp32 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75 74 exlimdv 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( E. v v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
76 54 75 mpi 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
77 76 exlimdv 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( E. u u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
78 53 77 mpi 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
79 78 a1d 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
80 79 a1d 
 |-  ( ( -. A. x x = z /\ -. A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
81 17 35 52 80 4cases 
 |-  ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )