Theorem suceq 6430

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	suceqd 6429	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1567  suc csuc 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-suc 6367

This theorem is referenced by:  eqelsuc  6448  suc11  6471  ordunisuc  7828  onsucuni2  7830  onuninsuci  7836  limsuc  7845  tfindes  7859  tfinds2  7860  peano5  7890  findes  7897  onnseq  8331  seqomlem0  8436  seqomlem1  8437  seqomlem4  8440  oasuc  8509  onasuc  8513  oa1suc  8516  oa0r  8523  o2p2e4  8526  oaass  8546  oneo  8566  omeulem1  8567  oeeulem  8587  oeeui  8588  nna0r  8595  nnacom  8603  nnaass  8608  nnmsucr  8611  omabs  8637  nnneo  8641  nneob  8642  omsmolem  8643  omopthlem1  8645  eldifsucnn  8650  naddsuc2  8688  naddoa  8689  limensuc  9142  infensuc  9143  nneneq  9190  unblem2  9253  unblem3  9254  suc11reg  9588  inf0  9590  inf3lem1  9597  dfom3  9616  cantnflt  9641  cantnflem1  9658  cnfcom  9669  brttrcl2  9683  ssttrcl  9684  ttrcltr  9685  ttrclss  9689  dmttrcl  9690  rnttrcl  9691  ttrclselem2  9695  r1elwf  9768  rankidb  9772  rankonidlem  9800  ranklim  9816  rankopb  9824  rankelop  9846  rankxpu  9848  rankmapu  9850  rankxplim  9851  cardsucnn  9971  dif1card  9994  infxpenlem  9997  fseqenlem1  10008  dfac12lem1  10127  dfac12lem2  10128  dfac12r  10130  pwsdompw  10186  ackbij1lem14  10215  ackbij1lem18  10219  ackbij1  10220  ackbij2lem3  10223  cfsmolem  10254  cfsmo  10255  sornom  10261  isfin3ds  10313  isf32lem1  10337  isf32lem2  10338  isf32lem5  10341  isf32lem6  10342  isf32lem7  10343  isf32lem8  10344  isf32lem11  10347  fin1a2lem1  10384  ituniiun  10406  axdc2lem  10432  axdc3lem2  10435  axdc3lem3  10436  axdc3lem4  10437  axdc3  10438  axdc4lem  10439  axcclem  10441  axdclem2  10504  wunex2  10723  om2uzsuci  13984  axdc4uzlem  14019  noresle  27827  nosupcbv  27832  nosupno  27833  nosupdm  27834  nosupfv  27836  nosupres  27837  nosupbnd1lem1  27838  nosupbnd1lem3  27840  nosupbnd1lem5  27842  noinfcbv  27847  noinfno  27848  noinfdm  27849  noinffv  27851  noinfres  27852  noinfbnd1lem3  27855  noinfbnd1lem5  27857  bday1  27973  om2noseqlt  28458  bdayn0sf1o  28529  bnj222  35216  bnj966  35277  bnj1112  35316  fineqvnttrclselem3  35459  fineqvnttrclse  35460  fineqvinfep  35461  gonar  35786  goalr  35788  satffun  35800  rankaltopb  36370  ranksng  36558  rankpwg  36560  rankeq1o  36562  ontgsucval  36832  onsucconn  36838  onsucsuccmp  36844  limsucncmp  36846  ordcmp  36847  finxpreclem4  37928  finxp00  37936  brsucmap  39005  mopre  39010  limsuc2  43660  aomclem4  43676  aomclem8  43680  onsucelab  43882  onsucf1olem  43889  onsucrn  43890  onov0suclim  43893  onsucunifi  43989  sucunisn  43990  onsucunipr  43991  onsucunitp  43992  nadd1suc  44011  naddonnn  44014  onsetreclem1  50368