Theorem suceq 6437

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  suc csuc 6370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-un 4153  df-sn 4588  df-suc 6374

This theorem is used by:  eqelsuc  6455  suc11  6478  ordunisuc  7850  onsucuni2  7852  onuninsuci  7858  limsuc  7867  tfindes  7881  tfinds2  7882  peano5  7912  findes  7919  onnseq  8363  seqomlem0  8470  seqomlem1  8471  seqomlem4  8474  oasuc  8543  onasuc  8547  oa1suc  8550  oa0r  8557  o2p2e4  8560  oaass  8580  oneo  8600  omeulem1  8601  oeeulem  8621  oeeui  8622  nna0r  8629  nnacom  8637  nnaass  8642  nnmsucr  8645  omabs  8671  nnneo  8675  nneob  8676  omsmolem  8677  omopthlem1  8679  eldifsucnn  8684  naddsuc2  8722  naddoa  8723  limensuc  9184  infensuc  9185  nneneq  9232  unblem2  9296  unblem3  9297  suc11reg  9630  inf0  9632  inf3lem1  9639  dfom3  9658  cantnflt  9683  cantnflem1  9700  cnfcom  9711  brttrcl2  9725  ssttrcl  9726  ttrcltr  9727  ttrclss  9731  dmttrcl  9732  rnttrcl  9733  ttrclselem2  9737  r1elwf  9814  rankidb  9818  rankonidlem  9848  rankpwg  9867  ranklim  9868  rankopb  9876  ranksng  9884  rankelop  9901  rankxpu  9903  rankmapu  9905  rankxplim  9906  cardsucnn  10076  dif1card  10099  infxpenlem  10102  fseqenlem1  10113  dfac12lem1  10232  dfac12lem2  10233  dfac12r  10235  pwsdompw  10291  ackbij1lem14  10320  ackbij1lem18  10324  ackbij1  10325  ackbij2lem3  10328  cfsmolem  10358  cfsmo  10359  sornom  10365  isfin3ds  10417  isf32lem1  10441  isf32lem2  10442  isf32lem5  10445  isf32lem6  10446  isf32lem7  10447  isf32lem8  10448  isf32lem11  10451  fin1a2lem1  10488  ituniiun  10510  axdc2lem  10536  axdc3lem2  10539  axdc3lem3  10540  axdc3lem4  10541  axdc3  10542  axdc4lem  10543  axcclem  10545  axdclem2  10608  wunex2  10833  om2uzsuci  14101  axdc4uzlem  14136  noresle  28066  nosupcbv  28071  nosupno  28072  nosupdm  28073  nosupfv  28075  nosupres  28076  nosupbnd1lem1  28077  nosupbnd1lem3  28079  nosupbnd1lem5  28081  noinfcbv  28086  noinfno  28087  noinfdm  28088  noinffv  28090  noinfres  28091  noinfbnd1lem3  28094  noinfbnd1lem5  28096  bday1  28212  om2noseqlt  28697  bdayn0sf1o  28768  bnj222  35566  bnj966  35627  bnj1112  35666  fineqvnttrclselem3  35862  fineqvnttrclse  35863  fineqvinfep  35864  onprcf1acwevdlem2  36000  gonar  36281  goalr  36283  satffun  36295  mirimanoffr  36581  rankaltopb  36871  rankeq1o  37059  ontgsucval  37347  onsucconn  37353  onsucsuccmp  37359  limsucncmp  37361  ordcmp  37362  finxpreclem4  38457  finxp00  38465  brsucmap  39538  mopre  39543  limsuc2  44188  aomclem4  44199  aomclem8  44203  onsucelab  44405  onsucf1olem  44412  onsucrn  44413  onov0suclim  44416  onsucunifi  44512  sucunisn  44513  onsucunipr  44514  onsucunitp  44515  nadd1suc  44534  naddonnn  44537  onsetreclem1  51012