Theorem suceq 6375

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

Syntax hints:   → wi 4   = wceq 1540  suc csuc 6309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-suc 6313

This theorem is referenced by:  eqelsuc  6393  suc11  6416  ordunisuc  7765  onsucuni2  7767  onuninsuci  7773  limsuc  7782  tfindes  7796  tfinds2  7797  peano5  7826  findes  7833  onnseq  8267  seqomlem0  8371  seqomlem1  8372  seqomlem4  8375  oasuc  8442  onasuc  8446  oa1suc  8449  oa0r  8456  o2p2e4  8459  oaass  8479  oneo  8499  omeulem1  8500  oeeulem  8519  oeeui  8520  nna0r  8527  nnacom  8535  nnaass  8540  nnmsucr  8543  omabs  8569  nnneo  8573  nneob  8574  omsmolem  8575  omopthlem1  8577  eldifsucnn  8582  naddsuc2  8619  naddoa  8620  limensuc  9071  infensuc  9072  nneneq  9120  unblem2  9182  unblem3  9183  suc11reg  9515  inf0  9517  inf3lem1  9524  dfom3  9543  cantnflt  9568  cantnflem1  9585  cnfcom  9596  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  dmttrcl  9617  rnttrcl  9618  ttrclselem2  9622  r1elwf  9692  rankidb  9696  rankonidlem  9724  ranklim  9740  rankopb  9748  rankelop  9770  rankxpu  9772  rankmapu  9774  rankxplim  9775  cardsucnn  9881  dif1card  9904  infxpenlem  9907  fseqenlem1  9918  dfac12lem1  10038  dfac12lem2  10039  dfac12r  10041  pwsdompw  10097  ackbij1lem14  10126  ackbij1lem18  10130  ackbij1  10131  ackbij2lem3  10134  cfsmolem  10164  cfsmo  10165  sornom  10171  isfin3ds  10223  isf32lem1  10247  isf32lem2  10248  isf32lem5  10251  isf32lem6  10252  isf32lem7  10253  isf32lem8  10254  isf32lem11  10257  fin1a2lem1  10294  ituniiun  10316  axdc2lem  10342  axdc3lem2  10345  axdc3lem3  10346  axdc3lem4  10347  axdc3  10348  axdc4lem  10349  axcclem  10351  axdclem2  10414  wunex2  10632  om2uzsuci  13855  axdc4uzlem  13890  noresle  27607  nosupcbv  27612  nosupno  27613  nosupdm  27614  nosupfv  27616  nosupres  27617  nosupbnd1lem1  27618  nosupbnd1lem3  27620  nosupbnd1lem5  27622  noinfcbv  27627  noinfno  27628  noinfdm  27629  noinffv  27631  noinfres  27632  noinfbnd1lem3  27635  noinfbnd1lem5  27637  bday1s  27745  om2noseqlt  28198  bdayn0sf1o  28264  bnj222  34856  bnj966  34917  bnj1112  34956  fineqvnttrclselem3  35082  fineqvnttrclse  35083  gonar  35378  goalr  35380  satffun  35392  rankaltopb  35963  ranksng  36151  rankpwg  36153  rankeq1o  36155  ontgsucval  36416  onsucconn  36422  onsucsuccmp  36428  limsucncmp  36430  ordcmp  36431  finxpreclem4  37378  finxp00  37386  limsuc2  43024  aomclem4  43040  aomclem8  43044  onsucelab  43246  onsucf1olem  43253  onsucrn  43254  onov0suclim  43257  onsucunifi  43353  sucunisn  43354  onsucunipr  43355  onsucunitp  43356  nadd1suc  43375  naddonnn  43378  onsetreclem1  49700