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 4135 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | uneq12d 3730 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
4 | df-suc 5646 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
5 | df-suc 5646 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
6 | 3, 4, 5 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∪ cun 3538 {csn 4125 suc csuc 5642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-sn 4126 df-suc 5646 |
This theorem is referenced by: eqelsuc 5723 suc11 5748 ordunisuc 6924 onsucuni2 6926 onuninsuci 6932 limsuc 6941 tfindes 6954 tfinds2 6955 findes 6988 onnseq 7328 seqomlem0 7431 seqomlem1 7432 seqomlem4 7435 oasuc 7491 onasuc 7495 oa1suc 7498 oa0r 7505 o2p2e4 7508 oaass 7528 oneo 7548 omeulem1 7549 oeeulem 7568 oeeui 7569 nna0r 7576 nnacom 7584 nnaass 7589 nnmsucr 7592 omabs 7614 nnneo 7618 nneob 7619 omsmolem 7620 omopthlem1 7622 limensuc 8022 infensuc 8023 nneneq 8028 unblem2 8098 unblem3 8099 suc11reg 8399 inf0 8401 inf3lem1 8408 dfom3 8427 cantnflt 8452 cantnflem1 8469 cnfcom 8480 r1elwf 8542 rankidb 8546 rankonidlem 8574 ranklim 8590 rankopb 8598 rankelop 8620 rankxpu 8622 rankmapu 8624 rankxplim 8625 cardsucnn 8694 dif1card 8716 infxpenlem 8719 fseqenlem1 8730 dfac12lem1 8848 dfac12lem2 8849 dfac12r 8851 pwsdompw 8909 ackbij1lem5 8929 ackbij1lem14 8938 ackbij1lem18 8942 ackbij1 8943 ackbij2lem3 8946 cfsmolem 8975 cfsmo 8976 sornom 8982 isfin3ds 9034 isf32lem1 9058 isf32lem2 9059 isf32lem5 9062 isf32lem6 9063 isf32lem7 9064 isf32lem8 9065 isf32lem11 9068 fin1a2lem1 9105 ituniiun 9127 axdc2lem 9153 axdc3lem2 9156 axdc3lem3 9157 axdc3lem4 9158 axdc3 9159 axdc4lem 9160 axcclem 9162 axdclem2 9225 wunex2 9439 om2uzsuci 12609 axdc4uzlem 12644 bnj222 30207 bnj966 30268 bnj1112 30305 nofulllem1 31101 nofulllem2 31102 rankaltopb 31256 ranksng 31444 rankpwg 31446 rankeq1o 31448 ontgsucval 31601 onsuccon 31607 onsucsuccmp 31613 limsucncmp 31615 ordcmp 31616 finxpreclem4 32407 finxp00 32415 limsuc2 36629 aomclem4 36645 aomclem8 36649 onsetreclem1 42247 |
Copyright terms: Public domain | W3C validator |