Theorem suceq 6374

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

Syntax hints:   → wi 4   = wceq 1541  suc csuc 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-suc 6312

This theorem is referenced by:  eqelsuc  6392  suc11  6415  ordunisuc  7762  onsucuni2  7764  onuninsuci  7770  limsuc  7779  tfindes  7793  tfinds2  7794  peano5  7823  findes  7830  onnseq  8264  seqomlem0  8368  seqomlem1  8369  seqomlem4  8372  oasuc  8439  onasuc  8443  oa1suc  8446  oa0r  8453  o2p2e4  8456  oaass  8476  oneo  8496  omeulem1  8497  oeeulem  8516  oeeui  8517  nna0r  8524  nnacom  8532  nnaass  8537  nnmsucr  8540  omabs  8566  nnneo  8570  nneob  8571  omsmolem  8572  omopthlem1  8574  eldifsucnn  8579  naddsuc2  8616  naddoa  8617  limensuc  9067  infensuc  9068  nneneq  9115  unblem2  9177  unblem3  9178  suc11reg  9509  inf0  9511  inf3lem1  9518  dfom3  9537  cantnflt  9562  cantnflem1  9579  cnfcom  9590  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  rnttrcl  9612  ttrclselem2  9616  r1elwf  9689  rankidb  9693  rankonidlem  9721  ranklim  9737  rankopb  9745  rankelop  9767  rankxpu  9769  rankmapu  9771  rankxplim  9772  cardsucnn  9878  dif1card  9901  infxpenlem  9904  fseqenlem1  9915  dfac12lem1  10035  dfac12lem2  10036  dfac12r  10038  pwsdompw  10094  ackbij1lem14  10123  ackbij1lem18  10127  ackbij1  10128  ackbij2lem3  10131  cfsmolem  10161  cfsmo  10162  sornom  10168  isfin3ds  10220  isf32lem1  10244  isf32lem2  10245  isf32lem5  10248  isf32lem6  10249  isf32lem7  10250  isf32lem8  10251  isf32lem11  10254  fin1a2lem1  10291  ituniiun  10313  axdc2lem  10339  axdc3lem2  10342  axdc3lem3  10343  axdc3lem4  10344  axdc3  10345  axdc4lem  10346  axcclem  10348  axdclem2  10411  wunex2  10629  om2uzsuci  13855  axdc4uzlem  13890  noresle  27636  nosupcbv  27641  nosupno  27642  nosupdm  27643  nosupfv  27645  nosupres  27646  nosupbnd1lem1  27647  nosupbnd1lem3  27649  nosupbnd1lem5  27651  noinfcbv  27656  noinfno  27657  noinfdm  27658  noinffv  27660  noinfres  27661  noinfbnd1lem3  27664  noinfbnd1lem5  27666  bday1s  27775  om2noseqlt  28229  bdayn0sf1o  28295  bnj222  34895  bnj966  34956  bnj1112  34995  fineqvnttrclselem3  35143  fineqvnttrclse  35144  gonar  35439  goalr  35441  satffun  35453  rankaltopb  36023  ranksng  36211  rankpwg  36213  rankeq1o  36215  ontgsucval  36476  onsucconn  36482  onsucsuccmp  36488  limsucncmp  36490  ordcmp  36491  finxpreclem4  37438  finxp00  37446  brsucmap  38489  mopre  38494  limsuc2  43144  aomclem4  43160  aomclem8  43164  onsucelab  43366  onsucf1olem  43373  onsucrn  43374  onov0suclim  43377  onsucunifi  43473  sucunisn  43474  onsucunipr  43475  onsucunitp  43476  nadd1suc  43495  naddonnn  43498  onsetreclem1  49816