Theorem suceq 6403

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-suc 6341

This theorem is referenced by:  eqelsuc  6421  suc11  6444  ordunisuc  7810  onsucuni2  7812  onuninsuci  7819  limsuc  7828  tfindes  7842  tfinds2  7843  peano5  7872  findes  7879  onnseq  8316  seqomlem0  8420  seqomlem1  8421  seqomlem4  8424  oasuc  8491  onasuc  8495  oa1suc  8498  oa0r  8505  o2p2e4  8508  oaass  8528  oneo  8548  omeulem1  8549  oeeulem  8568  oeeui  8569  nna0r  8576  nnacom  8584  nnaass  8589  nnmsucr  8592  omabs  8618  nnneo  8622  nneob  8623  omsmolem  8624  omopthlem1  8626  eldifsucnn  8631  naddsuc2  8668  naddoa  8669  limensuc  9124  infensuc  9125  nneneq  9176  unblem2  9247  unblem3  9248  suc11reg  9579  inf0  9581  inf3lem1  9588  dfom3  9607  cantnflt  9632  cantnflem1  9649  cnfcom  9660  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  dmttrcl  9681  rnttrcl  9682  ttrclselem2  9686  r1elwf  9756  rankidb  9760  rankonidlem  9788  ranklim  9804  rankopb  9812  rankelop  9834  rankxpu  9836  rankmapu  9838  rankxplim  9839  cardsucnn  9945  dif1card  9970  infxpenlem  9973  fseqenlem1  9984  dfac12lem1  10104  dfac12lem2  10105  dfac12r  10107  pwsdompw  10163  ackbij1lem14  10192  ackbij1lem18  10196  ackbij1  10197  ackbij2lem3  10200  cfsmolem  10230  cfsmo  10231  sornom  10237  isfin3ds  10289  isf32lem1  10313  isf32lem2  10314  isf32lem5  10317  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  isf32lem11  10323  fin1a2lem1  10360  ituniiun  10382  axdc2lem  10408  axdc3lem2  10411  axdc3lem3  10412  axdc3lem4  10413  axdc3  10414  axdc4lem  10415  axcclem  10417  axdclem2  10480  wunex2  10698  om2uzsuci  13920  axdc4uzlem  13955  noresle  27616  nosupcbv  27621  nosupno  27622  nosupdm  27623  nosupfv  27625  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem3  27629  nosupbnd1lem5  27631  noinfcbv  27636  noinfno  27637  noinfdm  27638  noinffv  27640  noinfres  27641  noinfbnd1lem3  27644  noinfbnd1lem5  27646  bday1s  27750  om2noseqlt  28200  bdayn0sf1o  28266  bnj222  34880  bnj966  34941  bnj1112  34980  gonar  35389  goalr  35391  satffun  35403  rankaltopb  35974  ranksng  36162  rankpwg  36164  rankeq1o  36166  ontgsucval  36427  onsucconn  36433  onsucsuccmp  36439  limsucncmp  36441  ordcmp  36442  finxpreclem4  37389  finxp00  37397  limsuc2  43037  aomclem4  43053  aomclem8  43057  onsucelab  43259  onsucf1olem  43266  onsucrn  43267  onov0suclim  43270  onsucunifi  43366  sucunisn  43367  onsucunipr  43368  onsucunitp  43369  nadd1suc  43388  naddonnn  43391  onsetreclem1  49698