Theorem suceq 6433

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-suc 6370

This theorem is used by:  eqelsuc  6451  suc11  6474  ordunisuc  7834  onsucuni2  7836  onuninsuci  7842  limsuc  7851  tfindes  7865  tfinds2  7866  peano5  7896  findes  7903  onnseq  8337  seqomlem0  8442  seqomlem1  8443  seqomlem4  8446  oasuc  8515  onasuc  8519  oa1suc  8522  oa0r  8529  o2p2e4  8532  oaass  8552  oneo  8572  omeulem1  8573  oeeulem  8593  oeeui  8594  nna0r  8601  nnacom  8609  nnaass  8614  nnmsucr  8617  omabs  8643  nnneo  8647  nneob  8648  omsmolem  8649  omopthlem1  8651  eldifsucnn  8656  naddsuc2  8694  naddoa  8695  limensuc  9149  infensuc  9150  nneneq  9197  unblem2  9260  unblem3  9261  suc11reg  9595  inf0  9597  inf3lem1  9604  dfom3  9623  cantnflt  9648  cantnflem1  9665  cnfcom  9676  brttrcl2  9690  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  dmttrcl  9697  rnttrcl  9698  ttrclselem2  9702  r1elwf  9775  rankidb  9779  rankonidlem  9807  ranklim  9823  rankopb  9831  rankelop  9853  rankxpu  9855  rankmapu  9857  rankxplim  9858  cardsucnn  9987  dif1card  10010  infxpenlem  10013  fseqenlem1  10024  dfac12lem1  10143  dfac12lem2  10144  dfac12r  10146  pwsdompw  10202  ackbij1lem14  10231  ackbij1lem18  10235  ackbij1  10236  ackbij2lem3  10239  cfsmolem  10269  cfsmo  10270  sornom  10276  isfin3ds  10328  isf32lem1  10352  isf32lem2  10353  isf32lem5  10356  isf32lem6  10357  isf32lem7  10358  isf32lem8  10359  isf32lem11  10362  fin1a2lem1  10399  ituniiun  10421  axdc2lem  10447  axdc3lem2  10450  axdc3lem3  10451  axdc3lem4  10452  axdc3  10453  axdc4lem  10454  axcclem  10456  axdclem2  10519  wunex2  10740  om2uzsuci  14004  axdc4uzlem  14039  noresle  27914  nosupcbv  27919  nosupno  27920  nosupdm  27921  nosupfv  27923  nosupres  27924  nosupbnd1lem1  27925  nosupbnd1lem3  27927  nosupbnd1lem5  27929  noinfcbv  27934  noinfno  27935  noinfdm  27936  noinffv  27938  noinfres  27939  noinfbnd1lem3  27942  noinfbnd1lem5  27944  bday1  28060  om2noseqlt  28545  bdayn0sf1o  28616  bnj222  35338  bnj966  35399  bnj1112  35438  fineqvnttrclselem3  35595  fineqvnttrclse  35596  fineqvinfep  35597  gonar  35926  goalr  35928  satffun  35940  rankaltopb  36510  ranksng  36698  rankpwg  36700  rankeq1o  36702  ontgsucval  37002  onsucconn  37008  onsucsuccmp  37014  limsucncmp  37016  ordcmp  37017  finxpreclem4  38099  finxp00  38107  brsucmap  39175  mopre  39180  limsuc2  43828  aomclem4  43844  aomclem8  43848  onsucelab  44050  onsucf1olem  44057  onsucrn  44058  onov0suclim  44061  onsucunifi  44157  sucunisn  44158  onsucunipr  44159  onsucunitp  44160  nadd1suc  44179  naddonnn  44182  onsetreclem1  50542