Theorem suceq 6414

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

Syntax hints:   → wi 4   = wceq 1560  suc csuc 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-suc 6352

This theorem is referenced by:  eqelsuc  6432  suc11  6455  ordunisuc  7812  onsucuni2  7814  onuninsuci  7820  limsuc  7829  tfindes  7843  tfinds2  7844  peano5  7874  findes  7881  onnseq  8315  seqomlem0  8420  seqomlem1  8421  seqomlem4  8424  oasuc  8493  onasuc  8497  oa1suc  8500  oa0r  8507  o2p2e4  8510  oaass  8530  oneo  8550  omeulem1  8551  oeeulem  8571  oeeui  8572  nna0r  8579  nnacom  8587  nnaass  8592  nnmsucr  8595  omabs  8621  nnneo  8625  nneob  8626  omsmolem  8627  omopthlem1  8629  eldifsucnn  8634  naddsuc2  8672  naddoa  8673  limensuc  9126  infensuc  9127  nneneq  9174  unblem2  9237  unblem3  9238  suc11reg  9574  inf0  9576  inf3lem1  9583  dfom3  9602  cantnflt  9627  cantnflem1  9644  cnfcom  9655  brttrcl2  9669  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  dmttrcl  9676  rnttrcl  9677  ttrclselem2  9681  r1elwf  9754  rankidb  9758  rankonidlem  9786  ranklim  9802  rankopb  9810  rankelop  9832  rankxpu  9834  rankmapu  9836  rankxplim  9837  cardsucnn  9943  dif1card  9966  infxpenlem  9969  fseqenlem1  9980  dfac12lem1  10100  dfac12lem2  10101  dfac12r  10103  pwsdompw  10159  ackbij1lem14  10188  ackbij1lem18  10192  ackbij1  10193  ackbij2lem3  10196  cfsmolem  10227  cfsmo  10228  sornom  10234  isfin3ds  10286  isf32lem1  10310  isf32lem2  10311  isf32lem5  10314  isf32lem6  10315  isf32lem7  10316  isf32lem8  10317  isf32lem11  10320  fin1a2lem1  10357  ituniiun  10379  axdc2lem  10405  axdc3lem2  10408  axdc3lem3  10409  axdc3lem4  10410  axdc3  10411  axdc4lem  10412  axcclem  10414  axdclem2  10477  wunex2  10696  om2uzsuci  13961  axdc4uzlem  13996  noresle  27761  nosupcbv  27766  nosupno  27767  nosupdm  27768  nosupfv  27770  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  noinfcbv  27781  noinfno  27782  noinfdm  27783  noinffv  27785  noinfres  27786  noinfbnd1lem3  27789  noinfbnd1lem5  27791  bday1  27907  om2noseqlt  28392  bdayn0sf1o  28463  bnj222  35178  bnj966  35239  bnj1112  35278  fineqvnttrclselem3  35419  fineqvnttrclse  35420  fineqvinfep  35421  gonar  35745  goalr  35747  satffun  35759  rankaltopb  36329  ranksng  36517  rankpwg  36519  rankeq1o  36521  ontgsucval  36792  onsucconn  36798  onsucsuccmp  36804  limsucncmp  36806  ordcmp  36807  finxpreclem4  37888  finxp00  37896  brsucmap  38965  mopre  38970  limsuc2  43618  aomclem4  43634  aomclem8  43638  onsucelab  43840  onsucf1olem  43847  onsucrn  43848  onov0suclim  43851  onsucunifi  43947  sucunisn  43948  onsucunipr  43949  onsucunitp  43950  nadd1suc  43969  naddonnn  43972  onsetreclem1  50326