Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  suceq Structured version   Visualization version   GIF version

Theorem suceq 5752
 Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
suceq (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Proof of Theorem suceq
StepHypRef Expression
1 id 22 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
2 sneq 4163 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2uneq12d 3751 . 2 (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4 df-suc 5691 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
5 df-suc 5691 . 2 suc 𝐵 = (𝐵 ∪ {𝐵})
63, 4, 53eqtr4g 2685 1 (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480   ∪ cun 3558  {csn 4153  suc csuc 5687 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-sn 4154  df-suc 5691 This theorem is referenced by:  eqelsuc  5768  suc11  5793  ordunisuc  6980  onsucuni2  6982  onuninsuci  6988  limsuc  6997  tfindes  7010  tfinds2  7011  findes  7044  onnseq  7387  seqomlem0  7490  seqomlem1  7491  seqomlem4  7494  oasuc  7550  onasuc  7554  oa1suc  7557  oa0r  7564  o2p2e4  7567  oaass  7587  oneo  7607  omeulem1  7608  oeeulem  7627  oeeui  7628  nna0r  7635  nnacom  7643  nnaass  7648  nnmsucr  7651  omabs  7673  nnneo  7677  nneob  7678  omsmolem  7679  omopthlem1  7681  limensuc  8082  infensuc  8083  nneneq  8088  unblem2  8158  unblem3  8159  suc11reg  8461  inf0  8463  inf3lem1  8470  dfom3  8489  cantnflt  8514  cantnflem1  8531  cnfcom  8542  r1elwf  8604  rankidb  8608  rankonidlem  8636  ranklim  8652  rankopb  8660  rankelop  8682  rankxpu  8684  rankmapu  8686  rankxplim  8687  cardsucnn  8756  dif1card  8778  infxpenlem  8781  fseqenlem1  8792  dfac12lem1  8910  dfac12lem2  8911  dfac12r  8913  pwsdompw  8971  ackbij1lem5  8991  ackbij1lem14  9000  ackbij1lem18  9004  ackbij1  9005  ackbij2lem3  9008  cfsmolem  9037  cfsmo  9038  sornom  9044  isfin3ds  9096  isf32lem1  9120  isf32lem2  9121  isf32lem5  9124  isf32lem6  9125  isf32lem7  9126  isf32lem8  9127  isf32lem11  9130  fin1a2lem1  9167  ituniiun  9189  axdc2lem  9215  axdc3lem2  9218  axdc3lem3  9219  axdc3lem4  9220  axdc3  9221  axdc4lem  9222  axcclem  9224  axdclem2  9287  wunex2  9505  om2uzsuci  12684  axdc4uzlem  12719  bnj222  30653  bnj966  30714  bnj1112  30751  noreslege  31563  nosino  31567  nosifv  31568  nosires  31569  rankaltopb  31720  ranksng  31908  rankpwg  31910  rankeq1o  31912  ontgsucval  32065  onsucconn  32071  onsucsuccmp  32077  limsucncmp  32079  ordcmp  32080  finxpreclem4  32855  finxp00  32863  limsuc2  37077  aomclem4  37093  aomclem8  37097  onsetreclem1  41715
 Copyright terms: Public domain W3C validator