Theorem suceq 6426

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-suc 6363

This theorem is used by:  eqelsuc  6444  suc11  6467  ordunisuc  7829  onsucuni2  7831  onuninsuci  7837  limsuc  7846  tfindes  7860  tfinds2  7861  peano5  7891  findes  7898  onnseq  8334  seqomlem0  8439  seqomlem1  8440  seqomlem4  8443  oasuc  8512  onasuc  8516  oa1suc  8519  oa0r  8526  o2p2e4  8529  oaass  8549  oneo  8569  omeulem1  8570  oeeulem  8590  oeeui  8591  nna0r  8598  nnacom  8606  nnaass  8611  nnmsucr  8614  omabs  8640  nnneo  8644  nneob  8645  omsmolem  8646  omopthlem1  8648  eldifsucnn  8653  naddsuc2  8691  naddoa  8692  limensuc  9153  infensuc  9154  nneneq  9201  unblem2  9264  unblem3  9265  suc11reg  9599  inf0  9601  inf3lem1  9608  dfom3  9627  cantnflt  9652  cantnflem1  9669  cnfcom  9680  brttrcl2  9694  ssttrcl  9695  ttrcltr  9696  ttrclss  9700  dmttrcl  9701  rnttrcl  9702  ttrclselem2  9706  r1elwf  9779  rankidb  9783  rankonidlem  9811  ranklim  9827  rankopb  9835  rankelop  9857  rankxpu  9859  rankmapu  9861  rankxplim  9862  cardsucnn  9991  dif1card  10014  infxpenlem  10017  fseqenlem1  10028  dfac12lem1  10147  dfac12lem2  10148  dfac12r  10150  pwsdompw  10206  ackbij1lem14  10235  ackbij1lem18  10239  ackbij1  10240  ackbij2lem3  10243  cfsmolem  10273  cfsmo  10274  sornom  10280  isfin3ds  10332  isf32lem1  10356  isf32lem2  10357  isf32lem5  10360  isf32lem6  10361  isf32lem7  10362  isf32lem8  10363  isf32lem11  10366  fin1a2lem1  10403  ituniiun  10425  axdc2lem  10451  axdc3lem2  10454  axdc3lem3  10455  axdc3lem4  10456  axdc3  10457  axdc4lem  10458  axcclem  10460  axdclem2  10523  wunex2  10748  om2uzsuci  14013  axdc4uzlem  14048  noresle  27934  nosupcbv  27939  nosupno  27940  nosupdm  27941  nosupfv  27943  nosupres  27944  nosupbnd1lem1  27945  nosupbnd1lem3  27947  nosupbnd1lem5  27949  noinfcbv  27954  noinfno  27955  noinfdm  27956  noinffv  27958  noinfres  27959  noinfbnd1lem3  27962  noinfbnd1lem5  27964  bday1  28080  om2noseqlt  28565  bdayn0sf1o  28636  bnj222  35393  bnj966  35454  bnj1112  35493  fineqvnttrclselem3  35650  fineqvnttrclse  35651  fineqvinfep  35652  gonar  35975  goalr  35977  satffun  35989  rankaltopb  36560  ranksng  36748  rankpwg  36750  rankeq1o  36752  ontgsucval  37052  onsucconn  37058  onsucsuccmp  37064  limsucncmp  37066  ordcmp  37067  finxpreclem4  38149  finxp00  38157  brsucmap  39215  mopre  39220  limsuc2  43883  aomclem4  43899  aomclem8  43903  onsucelab  44105  onsucf1olem  44112  onsucrn  44113  onov0suclim  44116  onsucunifi  44212  sucunisn  44213  onsucunipr  44214  onsucunitp  44215  nadd1suc  44234  naddonnn  44237  onsetreclem1  50632