Theorem suceq 6429

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

Syntax hints:   → wi 4   = wceq 1570  suc csuc 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-suc 6366

This theorem is referenced by:  eqelsuc  6447  suc11  6470  ordunisuc  7824  onsucuni2  7826  onuninsuci  7832  limsuc  7841  tfindes  7855  tfinds2  7856  peano5  7886  findes  7893  onnseq  8327  seqomlem0  8432  seqomlem1  8433  seqomlem4  8436  oasuc  8505  onasuc  8509  oa1suc  8512  oa0r  8519  o2p2e4  8522  oaass  8542  oneo  8562  omeulem1  8563  oeeulem  8583  oeeui  8584  nna0r  8591  nnacom  8599  nnaass  8604  nnmsucr  8607  omabs  8633  nnneo  8637  nneob  8638  omsmolem  8639  omopthlem1  8641  eldifsucnn  8646  naddsuc2  8684  naddoa  8685  limensuc  9138  infensuc  9139  nneneq  9186  unblem2  9249  unblem3  9250  suc11reg  9584  inf0  9586  inf3lem1  9593  dfom3  9612  cantnflt  9637  cantnflem1  9654  cnfcom  9665  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  dmttrcl  9686  rnttrcl  9687  ttrclselem2  9691  r1elwf  9764  rankidb  9768  rankonidlem  9796  ranklim  9812  rankopb  9820  rankelop  9842  rankxpu  9844  rankmapu  9846  rankxplim  9847  cardsucnn  9967  dif1card  9990  infxpenlem  9993  fseqenlem1  10004  dfac12lem1  10123  dfac12lem2  10124  dfac12r  10126  pwsdompw  10182  ackbij1lem14  10211  ackbij1lem18  10215  ackbij1  10216  ackbij2lem3  10219  cfsmolem  10249  cfsmo  10250  sornom  10256  isfin3ds  10308  isf32lem1  10332  isf32lem2  10333  isf32lem5  10336  isf32lem6  10337  isf32lem7  10338  isf32lem8  10339  isf32lem11  10342  fin1a2lem1  10379  ituniiun  10401  axdc2lem  10427  axdc3lem2  10430  axdc3lem3  10431  axdc3lem4  10432  axdc3  10433  axdc4lem  10434  axcclem  10436  axdclem2  10499  wunex2  10718  om2uzsuci  13980  axdc4uzlem  14015  noresle  27861  nosupcbv  27866  nosupno  27867  nosupdm  27868  nosupfv  27870  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem3  27874  nosupbnd1lem5  27876  noinfcbv  27881  noinfno  27882  noinfdm  27883  noinffv  27885  noinfres  27886  noinfbnd1lem3  27889  noinfbnd1lem5  27891  bday1  28007  om2noseqlt  28492  bdayn0sf1o  28563  bnj222  35271  bnj966  35332  bnj1112  35371  fineqvnttrclselem3  35536  fineqvnttrclse  35537  fineqvinfep  35538  gonar  35887  goalr  35889  satffun  35901  rankaltopb  36471  ranksng  36659  rankpwg  36661  rankeq1o  36663  ontgsucval  36963  onsucconn  36969  onsucsuccmp  36975  limsucncmp  36977  ordcmp  36978  finxpreclem4  38060  finxp00  38068  brsucmap  39135  mopre  39140  limsuc2  43788  aomclem4  43804  aomclem8  43808  onsucelab  44010  onsucf1olem  44017  onsucrn  44018  onov0suclim  44021  onsucunifi  44117  sucunisn  44118  onsucunipr  44119  onsucunitp  44120  nadd1suc  44139  naddonnn  44142  onsetreclem1  50503