Theorem suceq 6393

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

Syntax hints:   → wi 4   = wceq 1542  suc csuc 6327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-suc 6331

This theorem is referenced by:  eqelsuc  6411  suc11  6434  ordunisuc  7784  onsucuni2  7786  onuninsuci  7792  limsuc  7801  tfindes  7815  tfinds2  7816  peano5  7845  findes  7852  onnseq  8286  seqomlem0  8390  seqomlem1  8391  seqomlem4  8394  oasuc  8461  onasuc  8465  oa1suc  8468  oa0r  8475  o2p2e4  8478  oaass  8498  oneo  8518  omeulem1  8519  oeeulem  8539  oeeui  8540  nna0r  8547  nnacom  8555  nnaass  8560  nnmsucr  8563  omabs  8589  nnneo  8593  nneob  8594  omsmolem  8595  omopthlem1  8597  eldifsucnn  8602  naddsuc2  8639  naddoa  8640  limensuc  9094  infensuc  9095  nneneq  9142  unblem2  9205  unblem3  9206  suc11reg  9540  inf0  9542  inf3lem1  9549  dfom3  9568  cantnflt  9593  cantnflem1  9610  cnfcom  9621  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  r1elwf  9720  rankidb  9724  rankonidlem  9752  ranklim  9768  rankopb  9776  rankelop  9798  rankxpu  9800  rankmapu  9802  rankxplim  9803  cardsucnn  9909  dif1card  9932  infxpenlem  9935  fseqenlem1  9946  dfac12lem1  10066  dfac12lem2  10067  dfac12r  10069  pwsdompw  10125  ackbij1lem14  10154  ackbij1lem18  10158  ackbij1  10159  ackbij2lem3  10162  cfsmolem  10192  cfsmo  10193  sornom  10199  isfin3ds  10251  isf32lem1  10275  isf32lem2  10276  isf32lem5  10279  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  isf32lem11  10285  fin1a2lem1  10322  ituniiun  10344  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3lem4  10375  axdc3  10376  axdc4lem  10377  axcclem  10379  axdclem2  10442  wunex2  10661  om2uzsuci  13883  axdc4uzlem  13918  noresle  27677  nosupcbv  27682  nosupno  27683  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  noinfcbv  27697  noinfno  27698  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  bday1  27822  om2noseqlt  28307  bdayn0sf1o  28378  bnj222  35059  bnj966  35120  bnj1112  35159  fineqvnttrclselem3  35301  fineqvnttrclse  35302  fineqvinfep  35303  gonar  35611  goalr  35613  satffun  35625  rankaltopb  36195  ranksng  36383  rankpwg  36385  rankeq1o  36387  ontgsucval  36648  onsucconn  36654  onsucsuccmp  36660  limsucncmp  36662  ordcmp  36663  finxpreclem4  37649  finxp00  37657  brsucmap  38717  mopre  38722  limsuc2  43398  aomclem4  43414  aomclem8  43418  onsucelab  43620  onsucf1olem  43627  onsucrn  43628  onov0suclim  43631  onsucunifi  43727  sucunisn  43728  onsucunipr  43729  onsucunitp  43730  nadd1suc  43749  naddonnn  43752  onsetreclem1  50064