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

Theorem suceq 6228
 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 4538 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2uneq12d 4094 . 2 (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4 df-suc 6169 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
5 df-suc 6169 . 2 suc 𝐵 = (𝐵 ∪ {𝐵})
63, 4, 53eqtr4g 2861 1 (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3882  {csn 4528  suc csuc 6165 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-suc 6169 This theorem is referenced by:  eqelsuc  6244  suc11  6266  ordunisuc  7531  onsucuni2  7533  onuninsuci  7539  limsuc  7548  tfindes  7561  tfinds2  7562  findes  7597  onnseq  7968  seqomlem0  8072  seqomlem1  8073  seqomlem4  8076  oasuc  8136  onasuc  8140  oa1suc  8143  oa0r  8150  o2p2e4  8153  o2p2e4OLD  8154  oaass  8174  oneo  8194  omeulem1  8195  oeeulem  8214  oeeui  8215  nna0r  8222  nnacom  8230  nnaass  8235  nnmsucr  8238  omabs  8261  nnneo  8265  nneob  8266  omsmolem  8267  omopthlem1  8269  limensuc  8682  infensuc  8683  nneneq  8688  unblem2  8759  unblem3  8760  suc11reg  9070  inf0  9072  inf3lem1  9079  dfom3  9098  cantnflt  9123  cantnflem1  9140  cnfcom  9151  r1elwf  9213  rankidb  9217  rankonidlem  9245  ranklim  9261  rankopb  9269  rankelop  9291  rankxpu  9293  rankmapu  9295  rankxplim  9296  cardsucnn  9402  dif1card  9425  infxpenlem  9428  fseqenlem1  9439  dfac12lem1  9558  dfac12lem2  9559  dfac12r  9561  pwsdompw  9619  ackbij1lem14  9648  ackbij1lem18  9652  ackbij1  9653  ackbij2lem3  9656  cfsmolem  9685  cfsmo  9686  sornom  9692  isfin3ds  9744  isf32lem1  9768  isf32lem2  9769  isf32lem5  9772  isf32lem6  9773  isf32lem7  9774  isf32lem8  9775  isf32lem11  9778  fin1a2lem1  9815  ituniiun  9837  axdc2lem  9863  axdc3lem2  9866  axdc3lem3  9867  axdc3lem4  9868  axdc3  9869  axdc4lem  9870  axcclem  9872  axdclem2  9935  wunex2  10153  om2uzsuci  13315  axdc4uzlem  13350  bnj222  32269  bnj966  32330  bnj1112  32369  gonar  32756  goalr  32758  satffun  32770  noresle  33314  nosupno  33317  nosupdm  33318  nosupfv  33320  nosupres  33321  nosupbnd1lem1  33322  nosupbnd1lem3  33324  nosupbnd1lem5  33326  nosupbnd2  33330  noetalem4  33334  noeta  33336  rankaltopb  33554  ranksng  33742  rankpwg  33744  rankeq1o  33746  ontgsucval  33894  onsucconn  33900  onsucsuccmp  33906  limsucncmp  33908  ordcmp  33909  finxpreclem4  34812  finxp00  34820  limsuc2  39982  aomclem4  39998  aomclem8  40002  suceqd  40914  onsetreclem1  45231
 Copyright terms: Public domain W3C validator