Theorem suceq 6378

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

Syntax hints:   → wi 4   = wceq 1547  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-suc 6316

This theorem is referenced by:  eqelsuc  6396  suc11  6419  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  9082  infensuc  9083  nneneq  9130  unblem2  9193  unblem3  9194  suc11reg  9531  inf0  9533  inf3lem1  9540  dfom3  9559  cantnflt  9584  cantnflem1  9601  cnfcom  9612  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  r1elwf  9711  rankidb  9715  rankonidlem  9743  ranklim  9759  rankopb  9767  rankelop  9789  rankxpu  9791  rankmapu  9793  rankxplim  9794  cardsucnn  9900  dif1card  9923  infxpenlem  9926  fseqenlem1  9937  dfac12lem1  10057  dfac12lem2  10058  dfac12r  10060  pwsdompw  10116  ackbij1lem14  10145  ackbij1lem18  10149  ackbij1  10150  ackbij2lem3  10153  cfsmolem  10183  cfsmo  10184  sornom  10190  isfin3ds  10242  isf32lem1  10266  isf32lem2  10267  isf32lem5  10270  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  isf32lem11  10276  fin1a2lem1  10313  ituniiun  10335  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3lem4  10366  axdc3  10367  axdc4lem  10368  axcclem  10370  axdclem2  10433  wunex2  10652  om2uzsuci  13901  axdc4uzlem  13936  noresle  27679  nosupcbv  27684  nosupno  27685  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  noinfcbv  27699  noinfno  27700  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem3  27707  noinfbnd1lem5  27709  bday1  27824  om2noseqlt  28309  bdayn0sf1o  28380  bnj222  35065  bnj966  35126  bnj1112  35165  fineqvnttrclselem3  35304  fineqvnttrclse  35305  fineqvinfep  35306  gonar  35623  goalr  35625  satffun  35637  rankaltopb  36207  ranksng  36395  rankpwg  36397  rankeq1o  36399  ontgsucval  36660  onsucconn  36666  onsucsuccmp  36672  limsucncmp  36674  ordcmp  36675  finxpreclem4  37756  finxp00  37764  brsucmap  38833  mopre  38838  limsuc2  43486  aomclem4  43502  aomclem8  43506  onsucelab  43708  onsucf1olem  43715  onsucrn  43716  onov0suclim  43719  onsucunifi  43815  sucunisn  43816  onsucunipr  43817  onsucunitp  43818  nadd1suc  43837  naddonnn  43840  onsetreclem1  50195