![]() |
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 4326 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | uneq12d 3919 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵})) |
4 | df-suc 5872 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
5 | df-suc 5872 | . 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
6 | 3, 4, 5 | 3eqtr4g 2830 | 1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ∪ cun 3721 {csn 4316 suc csuc 5868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-un 3728 df-sn 4317 df-suc 5872 |
This theorem is referenced by: eqelsuc 5949 suc11 5974 ordunisuc 7179 onsucuni2 7181 onuninsuci 7187 limsuc 7196 tfindes 7209 tfinds2 7210 findes 7243 onnseq 7594 seqomlem0 7697 seqomlem1 7698 seqomlem4 7701 oasuc 7758 onasuc 7762 oa1suc 7765 oa0r 7772 o2p2e4 7775 oaass 7795 oneo 7815 omeulem1 7816 oeeulem 7835 oeeui 7836 nna0r 7843 nnacom 7851 nnaass 7856 nnmsucr 7859 omabs 7881 nnneo 7885 nneob 7886 omsmolem 7887 omopthlem1 7889 limensuc 8293 infensuc 8294 nneneq 8299 unblem2 8369 unblem3 8370 suc11reg 8680 inf0 8682 inf3lem1 8689 dfom3 8708 cantnflt 8733 cantnflem1 8750 cnfcom 8761 r1elwf 8823 rankidb 8827 rankonidlem 8855 ranklim 8871 rankopb 8879 rankelop 8901 rankxpu 8903 rankmapu 8905 rankxplim 8906 cardsucnn 9011 dif1card 9033 infxpenlem 9036 fseqenlem1 9047 dfac12lem1 9167 dfac12lem2 9168 dfac12r 9170 pwsdompw 9228 ackbij1lem14 9257 ackbij1lem18 9261 ackbij1 9262 ackbij2lem3 9265 cfsmolem 9294 cfsmo 9295 sornom 9301 isfin3ds 9353 isf32lem1 9377 isf32lem2 9378 isf32lem5 9381 isf32lem6 9382 isf32lem7 9383 isf32lem8 9384 isf32lem11 9387 fin1a2lem1 9424 ituniiun 9446 axdc2lem 9472 axdc3lem2 9475 axdc3lem3 9476 axdc3lem4 9477 axdc3 9478 axdc4lem 9479 axcclem 9481 axdclem2 9544 wunex2 9762 om2uzsuci 12955 axdc4uzlem 12990 bnj222 31291 bnj966 31352 bnj1112 31389 noresle 32183 nosupno 32186 nosupdm 32187 nosupfv 32189 nosupres 32190 nosupbnd1lem1 32191 nosupbnd1lem3 32193 nosupbnd1lem5 32195 nosupbnd2 32199 noetalem4 32203 noeta 32205 rankaltopb 32423 ranksng 32611 rankpwg 32613 rankeq1o 32615 ontgsucval 32768 onsucconn 32774 onsucsuccmp 32780 limsucncmp 32782 ordcmp 32783 finxpreclem4 33568 finxp00 33576 limsuc2 38137 aomclem4 38153 aomclem8 38157 onsetreclem1 42979 |
Copyright terms: Public domain | W3C validator |