Theorem suceq 6388

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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	suceqd 6387	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1540  suc csuc 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-suc 6326

This theorem is referenced by:  eqelsuc  6406  suc11  6429  ordunisuc  7787  onsucuni2  7789  onuninsuci  7796  limsuc  7805  tfindes  7819  tfinds2  7820  peano5  7849  findes  7856  onnseq  8290  seqomlem0  8394  seqomlem1  8395  seqomlem4  8398  oasuc  8465  onasuc  8469  oa1suc  8472  oa0r  8479  o2p2e4  8482  oaass  8502  oneo  8522  omeulem1  8523  oeeulem  8542  oeeui  8543  nna0r  8550  nnacom  8558  nnaass  8563  nnmsucr  8566  omabs  8592  nnneo  8596  nneob  8597  omsmolem  8598  omopthlem1  8600  eldifsucnn  8605  naddsuc2  8642  naddoa  8643  limensuc  9095  infensuc  9096  nneneq  9147  unblem2  9216  unblem3  9217  suc11reg  9548  inf0  9550  inf3lem1  9557  dfom3  9576  cantnflt  9601  cantnflem1  9618  cnfcom  9629  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  dmttrcl  9650  rnttrcl  9651  ttrclselem2  9655  r1elwf  9725  rankidb  9729  rankonidlem  9757  ranklim  9773  rankopb  9781  rankelop  9803  rankxpu  9805  rankmapu  9807  rankxplim  9808  cardsucnn  9914  dif1card  9939  infxpenlem  9942  fseqenlem1  9953  dfac12lem1  10073  dfac12lem2  10074  dfac12r  10076  pwsdompw  10132  ackbij1lem14  10161  ackbij1lem18  10165  ackbij1  10166  ackbij2lem3  10169  cfsmolem  10199  cfsmo  10200  sornom  10206  isfin3ds  10258  isf32lem1  10282  isf32lem2  10283  isf32lem5  10286  isf32lem6  10287  isf32lem7  10288  isf32lem8  10289  isf32lem11  10292  fin1a2lem1  10329  ituniiun  10351  axdc2lem  10377  axdc3lem2  10380  axdc3lem3  10381  axdc3lem4  10382  axdc3  10383  axdc4lem  10384  axcclem  10386  axdclem2  10449  wunex2  10667  om2uzsuci  13889  axdc4uzlem  13924  noresle  27642  nosupcbv  27647  nosupno  27648  nosupdm  27649  nosupfv  27651  nosupres  27652  nosupbnd1lem1  27653  nosupbnd1lem3  27655  nosupbnd1lem5  27657  noinfcbv  27662  noinfno  27663  noinfdm  27664  noinffv  27666  noinfres  27667  noinfbnd1lem3  27670  noinfbnd1lem5  27672  bday1s  27780  om2noseqlt  28233  bdayn0sf1o  28299  bnj222  34866  bnj966  34927  bnj1112  34966  gonar  35375  goalr  35377  satffun  35389  rankaltopb  35960  ranksng  36148  rankpwg  36150  rankeq1o  36152  ontgsucval  36413  onsucconn  36419  onsucsuccmp  36425  limsucncmp  36427  ordcmp  36428  finxpreclem4  37375  finxp00  37383  limsuc2  43023  aomclem4  43039  aomclem8  43043  onsucelab  43245  onsucf1olem  43252  onsucrn  43253  onov0suclim  43256  onsucunifi  43352  sucunisn  43353  onsucunipr  43354  onsucunitp  43355  nadd1suc  43374  naddonnn  43377  onsetreclem1  49687