| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > suceq | Structured version Visualization version GIF version | ||
| Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| Ref | Expression |
|---|---|
| suceq | ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 2 | sneq 4636 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
| 3 | 1, 2 | uneq12d 4169 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
| 4 | df-suc 6390 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
| 5 | df-suc 6390 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
| 6 | 3, 4, 5 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
| Copyright terms: Public domain | W3C validator |