| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > suceq | 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 19 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 2 | sneq 3644 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
| 3 | 1, 2 | uneq12d 3328 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
| 4 | df-suc 4418 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
| 5 | df-suc 4418 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
| 6 | 3, 4, 5 | 3eqtr4g 2263 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1373 ∪ cun 3164 {csn 3633 suc csuc 4412 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-un 3170 df-sn 3639 df-suc 4418 |
| This theorem is referenced by: eqelsuc 4466 2ordpr 4572 onsucsssucexmid 4575 onsucelsucexmid 4578 ordsucunielexmid 4579 suc11g 4605 onsucuni2 4612 0elsucexmid 4613 ordpwsucexmid 4618 peano2 4643 findes 4651 nn0suc 4652 0elnn 4667 omsinds 4670 tfr1onlemsucaccv 6427 tfrcllemsucaccv 6440 tfrcl 6450 frecabcl 6485 frecsuc 6493 sucinc 6531 sucinc2 6532 oacl 6546 oav2 6549 oasuc 6550 oa1suc 6553 nna0r 6564 nnacom 6570 nnaass 6571 nnmsucr 6574 nnsucelsuc 6577 nnsucsssuc 6578 nnaword 6597 nnaordex 6614 phplem3g 6953 nneneq 6954 php5 6955 php5dom 6960 omp1eomlem 7196 omp1eom 7197 nninfninc 7225 nnnninfeq 7230 nnnninfeq2 7231 nninfwlpoimlemg 7277 nninfwlpoimlemginf 7278 nninfwlpoim 7281 nninfinfwlpo 7282 indpi 7455 ennnfoneleminc 12782 ennnfonelemex 12785 bj-indsuc 15864 bj-bdfindes 15885 bj-nn0suc0 15886 bj-peano4 15891 bj-inf2vnlem1 15906 bj-nn0sucALT 15914 bj-findes 15917 nnsf 15942 nninfsellemdc 15947 nninfself 15950 nninfsellemeqinf 15953 nninfomni 15956 |
| Copyright terms: Public domain | W3C validator |