Theorem suceq 6457

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  suc csuc 6390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-suc 6394

This theorem is used by:  eqelsuc  6475  suc11  6498  ordunisuc  7877  onsucuni2  7879  onuninsuci  7885  limsuc  7894  tfindes  7908  tfinds2  7909  peano5  7939  findes  7946  onnseq  8390  seqomlem0  8497  seqomlem1  8498  seqomlem4  8501  oasuc  8570  onasuc  8574  oa1suc  8577  oa0r  8584  o2p2e4  8587  oaass  8607  oneo  8627  omeulem1  8628  oeeulem  8648  oeeui  8649  nna0r  8656  nnacom  8664  nnaass  8669  nnmsucr  8672  omabs  8698  nnneo  8702  nneob  8703  omsmolem  8704  omopthlem1  8706  eldifsucnn  8711  naddsuc2  8749  naddoa  8750  limensuc  9211  infensuc  9212  nneneq  9259  unblem2  9323  unblem3  9324  suc11reg  9657  inf0  9659  inf3lem1  9666  dfom3  9685  cantnflt  9710  cantnflem1  9727  cnfcom  9738  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  dmttrcl  9759  rnttrcl  9760  ttrclselem2  9764  r1elwf  9841  rankidb  9845  rankonidlem  9875  rankpwg  9894  ranklim  9895  rankopb  9903  ranksng  9911  rankelop  9928  rankxpu  9930  rankmapu  9932  rankxplim  9933  cardsucnn  10105  dif1card  10128  infxpenlem  10131  fseqenlem1  10142  dfac12lem1  10261  dfac12lem2  10262  dfac12r  10264  pwsdompw  10320  ackbij1lem14  10349  ackbij1lem18  10353  ackbij1  10354  ackbij2lem3  10357  cfsmolem  10387  cfsmo  10388  sornom  10394  isfin3ds  10446  isf32lem1  10470  isf32lem2  10471  isf32lem5  10474  isf32lem6  10475  isf32lem7  10476  isf32lem8  10477  isf32lem11  10480  fin1a2lem1  10517  ituniiun  10539  axdc2lem  10565  axdc3lem2  10568  axdc3lem3  10569  axdc3lem4  10570  axdc3  10571  axdc4lem  10572  axcclem  10574  axdclem2  10637  wunex2  10862  om2uzsuci  14131  axdc4uzlem  14166  noresle  28111  nosupcbv  28116  nosupno  28117  nosupdm  28118  nosupfv  28120  nosupres  28121  nosupbnd1lem1  28122  nosupbnd1lem3  28124  nosupbnd1lem5  28126  noinfcbv  28131  noinfno  28132  noinfdm  28133  noinffv  28135  noinfres  28136  noinfbnd1lem3  28139  noinfbnd1lem5  28141  bday1  28257  om2noseqlt  28742  bdayn0sf1o  28813  bnj222  35624  bnj966  35685  bnj1112  35724  fineqvnttrclselem3  35932  fineqvnttrclse  35933  fineqvinfep  35934  onprcf1acwevdlem2  36087  gonar  36368  goalr  36370  satffun  36382  mirimanoffr  36668  rankaltopb  36959  rankeq1o  37147  ontgsucval  37435  onsucconn  37441  onsucsuccmp  37447  limsucncmp  37449  ordcmp  37450  finxpreclem4  38585  finxp00  38593  brsucmap  39664  mopre  39669  limsuc2  44314  aomclem4  44325  aomclem8  44329  onsucelab  44526  onsucf1olem  44533  onsucrn  44534  onov0suclim  44537  onsucunifi  44633  sucunisn  44634  onsucunipr  44635  onsucunitp  44636  nadd1suc  44655  naddonnn  44658  onsetreclem1  51204