Theorem suceq 6431

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  suc csuc 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-suc 6368

This theorem is used by:  eqelsuc  6449  suc11  6472  ordunisuc  7843  onsucuni2  7845  onuninsuci  7851  limsuc  7860  tfindes  7874  tfinds2  7875  peano5  7905  findes  7912  onnseq  8352  seqomlem0  8459  seqomlem1  8460  seqomlem4  8463  oasuc  8532  onasuc  8536  oa1suc  8539  oa0r  8546  o2p2e4  8549  oaass  8569  oneo  8589  omeulem1  8590  oeeulem  8610  oeeui  8611  nna0r  8618  nnacom  8626  nnaass  8631  nnmsucr  8634  omabs  8660  nnneo  8664  nneob  8665  omsmolem  8666  omopthlem1  8668  eldifsucnn  8673  naddsuc2  8711  naddoa  8712  limensuc  9173  infensuc  9174  nneneq  9221  unblem2  9285  unblem3  9286  suc11reg  9620  inf0  9622  inf3lem1  9629  dfom3  9648  cantnflt  9673  cantnflem1  9690  cnfcom  9701  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  dmttrcl  9722  rnttrcl  9723  ttrclselem2  9727  r1elwf  9804  rankidb  9808  rankonidlem  9838  rankpwg  9857  ranklim  9858  rankopb  9866  ranksng  9874  rankelop  9891  rankxpu  9893  rankmapu  9895  rankxplim  9896  cardsucnn  10066  dif1card  10089  infxpenlem  10092  fseqenlem1  10103  dfac12lem1  10222  dfac12lem2  10223  dfac12r  10225  pwsdompw  10281  ackbij1lem14  10310  ackbij1lem18  10314  ackbij1  10315  ackbij2lem3  10318  cfsmolem  10348  cfsmo  10349  sornom  10355  isfin3ds  10407  isf32lem1  10431  isf32lem2  10432  isf32lem5  10435  isf32lem6  10436  isf32lem7  10437  isf32lem8  10438  isf32lem11  10441  fin1a2lem1  10478  ituniiun  10500  axdc2lem  10526  axdc3lem2  10529  axdc3lem3  10530  axdc3lem4  10531  axdc3  10532  axdc4lem  10533  axcclem  10535  axdclem2  10598  wunex2  10823  om2uzsuci  14091  axdc4uzlem  14126  noresle  28054  nosupcbv  28059  nosupno  28060  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  noinfcbv  28074  noinfno  28075  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem5  28084  bday1  28200  om2noseqlt  28685  bdayn0sf1o  28756  bnj222  35513  bnj966  35574  bnj1112  35613  fineqvnttrclselem3  35791  fineqvnttrclse  35792  fineqvinfep  35793  onprcf1acwevdlem2  35896  gonar  36160  goalr  36162  satffun  36174  rankaltopb  36744  rankeq1o  36932  ontgsucval  37220  onsucconn  37226  onsucsuccmp  37232  limsucncmp  37234  ordcmp  37235  finxpreclem4  38317  finxp00  38325  brsucmap  39398  mopre  39403  limsuc2  44047  aomclem4  44058  aomclem8  44062  onsucelab  44264  onsucf1olem  44271  onsucrn  44272  onov0suclim  44275  onsucunifi  44371  sucunisn  44372  onsucunipr  44373  onsucunitp  44374  nadd1suc  44393  naddonnn  44396  onsetreclem1  50797