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 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6ev | ⊢ ∃ 𝑧 𝑧 = 𝑦 | |
| 2 | dveeq2 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) | |
| 3 | ax12v | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) | |
| 4 | equeuclr | ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) ) | |
| 5 | 4 | sps | ⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) ) |
| 6 | 4 | imim1d | ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 = 𝑧 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| 7 | 6 | al2imi | ⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| 8 | 7 | imim2d | ⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |
| 9 | 5 8 | imim12d | ⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) ) |
| 10 | 2 3 9 | syl6mpi | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) ) |
| 11 | 10 | exlimdv | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) ) |
| 12 | 1 11 | mpi | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |