Theorem suceq 6385

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-suc 6323

This theorem is referenced by:  eqelsuc  6403  suc11  6426  ordunisuc  7774  onsucuni2  7776  onuninsuci  7782  limsuc  7791  tfindes  7805  tfinds2  7806  peano5  7835  findes  7842  onnseq  8276  seqomlem0  8380  seqomlem1  8381  seqomlem4  8384  oasuc  8451  onasuc  8455  oa1suc  8458  oa0r  8465  o2p2e4  8468  oaass  8488  oneo  8508  omeulem1  8509  oeeulem  8529  oeeui  8530  nna0r  8537  nnacom  8545  nnaass  8550  nnmsucr  8553  omabs  8579  nnneo  8583  nneob  8584  omsmolem  8585  omopthlem1  8587  eldifsucnn  8592  naddsuc2  8629  naddoa  8630  limensuc  9082  infensuc  9083  nneneq  9130  unblem2  9193  unblem3  9194  suc11reg  9528  inf0  9530  inf3lem1  9537  dfom3  9556  cantnflt  9581  cantnflem1  9598  cnfcom  9609  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  dmttrcl  9630  rnttrcl  9631  ttrclselem2  9635  r1elwf  9708  rankidb  9712  rankonidlem  9740  ranklim  9756  rankopb  9764  rankelop  9786  rankxpu  9788  rankmapu  9790  rankxplim  9791  cardsucnn  9897  dif1card  9920  infxpenlem  9923  fseqenlem1  9934  dfac12lem1  10054  dfac12lem2  10055  dfac12r  10057  pwsdompw  10113  ackbij1lem14  10142  ackbij1lem18  10146  ackbij1  10147  ackbij2lem3  10150  cfsmolem  10180  cfsmo  10181  sornom  10187  isfin3ds  10239  isf32lem1  10263  isf32lem2  10264  isf32lem5  10267  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  isf32lem11  10273  fin1a2lem1  10310  ituniiun  10332  axdc2lem  10358  axdc3lem2  10361  axdc3lem3  10362  axdc3lem4  10363  axdc3  10364  axdc4lem  10365  axcclem  10367  axdclem2  10430  wunex2  10649  om2uzsuci  13871  axdc4uzlem  13906  noresle  27665  nosupcbv  27670  nosupno  27671  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  noinfcbv  27685  noinfno  27686  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  bday1  27810  om2noseqlt  28295  bdayn0sf1o  28366  bnj222  35039  bnj966  35100  bnj1112  35139  fineqvnttrclselem3  35279  fineqvnttrclse  35280  fineqvinfep  35281  gonar  35589  goalr  35591  satffun  35603  rankaltopb  36173  ranksng  36361  rankpwg  36363  rankeq1o  36365  ontgsucval  36626  onsucconn  36632  onsucsuccmp  36638  limsucncmp  36640  ordcmp  36641  finxpreclem4  37599  finxp00  37607  brsucmap  38650  mopre  38655  limsuc2  43293  aomclem4  43309  aomclem8  43313  onsucelab  43515  onsucf1olem  43522  onsucrn  43523  onov0suclim  43526  onsucunifi  43622  sucunisn  43623  onsucunipr  43624  onsucunitp  43625  nadd1suc  43644  naddonnn  43647  onsetreclem1  49960