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

Theorem suceq 5788
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 4185 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2uneq12d 3766 . 2 (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4 df-suc 5727 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
5 df-suc 5727 . 2 suc 𝐵 = (𝐵 ∪ {𝐵})
63, 4, 53eqtr4g 2680 1 (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  cun 3570  {csn 4175  suc csuc 5723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-sn 4176  df-suc 5727
This theorem is referenced by:  eqelsuc  5804  suc11  5829  ordunisuc  7029  onsucuni2  7031  onuninsuci  7037  limsuc  7046  tfindes  7059  tfinds2  7060  findes  7093  onnseq  7438  seqomlem0  7541  seqomlem1  7542  seqomlem4  7545  oasuc  7601  onasuc  7605  oa1suc  7608  oa0r  7615  o2p2e4  7618  oaass  7638  oneo  7658  omeulem1  7659  oeeulem  7678  oeeui  7679  nna0r  7686  nnacom  7694  nnaass  7699  nnmsucr  7702  omabs  7724  nnneo  7728  nneob  7729  omsmolem  7730  omopthlem1  7732  limensuc  8134  infensuc  8135  nneneq  8140  unblem2  8210  unblem3  8211  suc11reg  8513  inf0  8515  inf3lem1  8522  dfom3  8541  cantnflt  8566  cantnflem1  8583  cnfcom  8594  r1elwf  8656  rankidb  8660  rankonidlem  8688  ranklim  8704  rankopb  8712  rankelop  8734  rankxpu  8736  rankmapu  8738  rankxplim  8739  cardsucnn  8808  dif1card  8830  infxpenlem  8833  fseqenlem1  8844  dfac12lem1  8962  dfac12lem2  8963  dfac12r  8965  pwsdompw  9023  ackbij1lem5  9043  ackbij1lem14  9052  ackbij1lem18  9056  ackbij1  9057  ackbij2lem3  9060  cfsmolem  9089  cfsmo  9090  sornom  9096  isfin3ds  9148  isf32lem1  9172  isf32lem2  9173  isf32lem5  9176  isf32lem6  9177  isf32lem7  9178  isf32lem8  9179  isf32lem11  9182  fin1a2lem1  9219  ituniiun  9241  axdc2lem  9267  axdc3lem2  9270  axdc3lem3  9271  axdc3lem4  9272  axdc3  9273  axdc4lem  9274  axcclem  9276  axdclem2  9339  wunex2  9557  om2uzsuci  12742  axdc4uzlem  12777  bnj222  30938  bnj966  30999  bnj1112  31036  noresle  31830  nosupno  31833  nosupdm  31834  nosupfv  31836  nosupres  31837  nosupbnd1lem1  31838  nosupbnd1lem3  31840  nosupbnd1lem5  31842  nosupbnd2  31846  noetalem4  31850  noeta  31852  rankaltopb  32070  ranksng  32258  rankpwg  32260  rankeq1o  32262  ontgsucval  32415  onsucconn  32421  onsucsuccmp  32427  limsucncmp  32429  ordcmp  32430  finxpreclem4  33211  finxp00  33219  limsuc2  37437  aomclem4  37453  aomclem8  37457  onsetreclem1  42219
  Copyright terms: Public domain W3C validator