Description: Derivation of set.mm's original ax-c15 from ax-c11n and the shorter ax-12 that has replaced it.
Theorem ax12 shows the reverse derivation of ax-12 from ax-c15 .
Normally, axc15 should be used rather than ax-c15 , except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Feb-2007) (Proof shortened by Wolf Lammen, 26-Mar-2023) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc15 | |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6ev | |- E. z z = y |
|
| 2 | dveeq2 | |- ( -. A. x x = y -> ( z = y -> A. x z = y ) ) |
|
| 3 | ax12v | |- ( x = z -> ( ph -> A. x ( x = z -> ph ) ) ) |
|
| 4 | equeuclr | |- ( z = y -> ( x = y -> x = z ) ) |
|
| 5 | 4 | sps | |- ( A. x z = y -> ( x = y -> x = z ) ) |
| 6 | 4 | imim1d | |- ( z = y -> ( ( x = z -> ph ) -> ( x = y -> ph ) ) ) |
| 7 | 6 | al2imi | |- ( A. x z = y -> ( A. x ( x = z -> ph ) -> A. x ( x = y -> ph ) ) ) |
| 8 | 7 | imim2d | |- ( A. x z = y -> ( ( ph -> A. x ( x = z -> ph ) ) -> ( ph -> A. x ( x = y -> ph ) ) ) ) |
| 9 | 5 8 | imim12d | |- ( A. x z = y -> ( ( x = z -> ( ph -> A. x ( x = z -> ph ) ) ) -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) ) |
| 10 | 2 3 9 | syl6mpi | |- ( -. A. x x = y -> ( z = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) ) |
| 11 | 10 | exlimdv | |- ( -. A. x x = y -> ( E. z z = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) ) |
| 12 | 1 11 | mpi | |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |