![]() |
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 3603 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | uneq12d 3290 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
4 | df-suc 4371 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
5 | df-suc 4371 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
6 | 3, 4, 5 | 3eqtr4g 2235 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∪ cun 3127 {csn 3592 suc csuc 4365 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3598 df-suc 4371 |
This theorem is referenced by: eqelsuc 4419 2ordpr 4523 onsucsssucexmid 4526 onsucelsucexmid 4529 ordsucunielexmid 4530 suc11g 4556 onsucuni2 4563 0elsucexmid 4564 ordpwsucexmid 4569 peano2 4594 findes 4602 nn0suc 4603 0elnn 4618 omsinds 4621 tfr1onlemsucaccv 6341 tfrcllemsucaccv 6354 tfrcl 6364 frecabcl 6399 frecsuc 6407 sucinc 6445 sucinc2 6446 oacl 6460 oav2 6463 oasuc 6464 oa1suc 6467 nna0r 6478 nnacom 6484 nnaass 6485 nnmsucr 6488 nnsucelsuc 6491 nnsucsssuc 6492 nnaword 6511 nnaordex 6528 phplem3g 6855 nneneq 6856 php5 6857 php5dom 6862 omp1eomlem 7092 omp1eom 7093 nnnninfeq 7125 nnnninfeq2 7126 nninfwlpoimlemg 7172 nninfwlpoimlemginf 7173 nninfwlpoim 7175 indpi 7340 ennnfoneleminc 12411 ennnfonelemex 12414 bj-indsuc 14650 bj-bdfindes 14671 bj-nn0suc0 14672 bj-peano4 14677 bj-inf2vnlem1 14692 bj-nn0sucALT 14700 bj-findes 14703 nnsf 14724 nninfsellemdc 14729 nninfself 14732 nninfsellemeqinf 14735 nninfomni 14738 |
Copyright terms: Public domain | W3C validator |