Theorem suceq 6383

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 6382	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1541  suc csuc 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-suc 6321

This theorem is referenced by:  eqelsuc  6401  suc11  6424  ordunisuc  7772  onsucuni2  7774  onuninsuci  7780  limsuc  7789  tfindes  7803  tfinds2  7804  peano5  7833  findes  7840  onnseq  8274  seqomlem0  8378  seqomlem1  8379  seqomlem4  8382  oasuc  8449  onasuc  8453  oa1suc  8456  oa0r  8463  o2p2e4  8466  oaass  8486  oneo  8506  omeulem1  8507  oeeulem  8527  oeeui  8528  nna0r  8535  nnacom  8543  nnaass  8548  nnmsucr  8551  omabs  8577  nnneo  8581  nneob  8582  omsmolem  8583  omopthlem1  8585  eldifsucnn  8590  naddsuc2  8627  naddoa  8628  limensuc  9080  infensuc  9081  nneneq  9128  unblem2  9191  unblem3  9192  suc11reg  9526  inf0  9528  inf3lem1  9535  dfom3  9554  cantnflt  9579  cantnflem1  9596  cnfcom  9607  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  dmttrcl  9628  rnttrcl  9629  ttrclselem2  9633  r1elwf  9706  rankidb  9710  rankonidlem  9738  ranklim  9754  rankopb  9762  rankelop  9784  rankxpu  9786  rankmapu  9788  rankxplim  9789  cardsucnn  9895  dif1card  9918  infxpenlem  9921  fseqenlem1  9932  dfac12lem1  10052  dfac12lem2  10053  dfac12r  10055  pwsdompw  10111  ackbij1lem14  10140  ackbij1lem18  10144  ackbij1  10145  ackbij2lem3  10148  cfsmolem  10178  cfsmo  10179  sornom  10185  isfin3ds  10237  isf32lem1  10261  isf32lem2  10262  isf32lem5  10265  isf32lem6  10266  isf32lem7  10267  isf32lem8  10268  isf32lem11  10271  fin1a2lem1  10308  ituniiun  10330  axdc2lem  10356  axdc3lem2  10359  axdc3lem3  10360  axdc3lem4  10361  axdc3  10362  axdc4lem  10363  axcclem  10365  axdclem2  10428  wunex2  10647  om2uzsuci  13869  axdc4uzlem  13904  noresle  27663  nosupcbv  27668  nosupno  27669  nosupdm  27670  nosupfv  27672  nosupres  27673  nosupbnd1lem1  27674  nosupbnd1lem3  27676  nosupbnd1lem5  27678  noinfcbv  27683  noinfno  27684  noinfdm  27685  noinffv  27687  noinfres  27688  noinfbnd1lem3  27691  noinfbnd1lem5  27693  bday1s  27802  om2noseqlt  28260  bdayn0sf1o  28328  bnj222  34988  bnj966  35049  bnj1112  35088  fineqvnttrclselem3  35228  fineqvnttrclse  35229  fineqvinfep  35230  gonar  35538  goalr  35540  satffun  35552  rankaltopb  36122  ranksng  36310  rankpwg  36312  rankeq1o  36314  ontgsucval  36575  onsucconn  36581  onsucsuccmp  36587  limsucncmp  36589  ordcmp  36590  finxpreclem4  37538  finxp00  37546  brsucmap  38579  mopre  38584  limsuc2  43225  aomclem4  43241  aomclem8  43245  onsucelab  43447  onsucf1olem  43454  onsucrn  43455  onov0suclim  43458  onsucunifi  43554  sucunisn  43555  onsucunipr  43556  onsucunitp  43557  nadd1suc  43576  naddonnn  43579  onsetreclem1  49892