![]() |
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 4451 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | uneq12d 4030 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
4 | df-suc 6035 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
5 | df-suc 6035 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
6 | 3, 4, 5 | 3eqtr4g 2840 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∪ cun 3828 {csn 4441 suc csuc 6031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-v 3418 df-un 3835 df-sn 4442 df-suc 6035 |
This theorem is referenced by: eqelsuc 6110 suc11 6132 ordunisuc 7363 onsucuni2 7365 onuninsuci 7371 limsuc 7380 tfindes 7393 tfinds2 7394 findes 7427 onnseq 7785 seqomlem0 7888 seqomlem1 7889 seqomlem4 7892 oasuc 7951 onasuc 7955 oa1suc 7958 oa0r 7965 o2p2e4 7968 oaass 7988 oneo 8008 omeulem1 8009 oeeulem 8028 oeeui 8029 nna0r 8036 nnacom 8044 nnaass 8049 nnmsucr 8052 omabs 8074 nnneo 8078 nneob 8079 omsmolem 8080 omopthlem1 8082 limensuc 8490 infensuc 8491 nneneq 8496 unblem2 8566 unblem3 8567 suc11reg 8876 inf0 8878 inf3lem1 8885 dfom3 8904 cantnflt 8929 cantnflem1 8946 cnfcom 8957 r1elwf 9019 rankidb 9023 rankonidlem 9051 ranklim 9067 rankopb 9075 rankelop 9097 rankxpu 9099 rankmapu 9101 rankxplim 9102 cardsucnn 9208 dif1card 9230 infxpenlem 9233 fseqenlem1 9244 dfac12lem1 9363 dfac12lem2 9364 dfac12r 9366 pwsdompw 9424 ackbij1lem14 9453 ackbij1lem18 9457 ackbij1 9458 ackbij2lem3 9461 cfsmolem 9490 cfsmo 9491 sornom 9497 isfin3ds 9549 isf32lem1 9573 isf32lem2 9574 isf32lem5 9577 isf32lem6 9578 isf32lem7 9579 isf32lem8 9580 isf32lem11 9583 fin1a2lem1 9620 ituniiun 9642 axdc2lem 9668 axdc3lem2 9671 axdc3lem3 9672 axdc3lem4 9673 axdc3 9674 axdc4lem 9675 axcclem 9677 axdclem2 9740 wunex2 9958 om2uzsuci 13131 axdc4uzlem 13166 bnj222 31799 bnj966 31860 bnj1112 31897 noresle 32718 nosupno 32721 nosupdm 32722 nosupfv 32724 nosupres 32725 nosupbnd1lem1 32726 nosupbnd1lem3 32728 nosupbnd1lem5 32730 nosupbnd2 32734 noetalem4 32738 noeta 32740 rankaltopb 32958 ranksng 33146 rankpwg 33148 rankeq1o 33150 ontgsucval 33297 onsucconn 33303 onsucsuccmp 33309 limsucncmp 33311 ordcmp 33312 finxpreclem4 34113 finxp00 34121 limsuc2 39034 aomclem4 39050 aomclem8 39054 suceqd 39935 onsetreclem1 44172 |
Copyright terms: Public domain | W3C validator |