Theorem suceq 6391

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

Syntax hints:   → wi 4   = wceq 1542  suc csuc 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-suc 6329

This theorem is referenced by:  eqelsuc  6409  suc11  6432  ordunisuc  7783  onsucuni2  7785  onuninsuci  7791  limsuc  7800  tfindes  7814  tfinds2  7815  peano5  7844  findes  7851  onnseq  8284  seqomlem0  8388  seqomlem1  8389  seqomlem4  8392  oasuc  8459  onasuc  8463  oa1suc  8466  oa0r  8473  o2p2e4  8476  oaass  8496  oneo  8516  omeulem1  8517  oeeulem  8537  oeeui  8538  nna0r  8545  nnacom  8553  nnaass  8558  nnmsucr  8561  omabs  8587  nnneo  8591  nneob  8592  omsmolem  8593  omopthlem1  8595  eldifsucnn  8600  naddsuc2  8637  naddoa  8638  limensuc  9092  infensuc  9093  nneneq  9140  unblem2  9203  unblem3  9204  suc11reg  9540  inf0  9542  inf3lem1  9549  dfom3  9568  cantnflt  9593  cantnflem1  9610  cnfcom  9621  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  r1elwf  9720  rankidb  9724  rankonidlem  9752  ranklim  9768  rankopb  9776  rankelop  9798  rankxpu  9800  rankmapu  9802  rankxplim  9803  cardsucnn  9909  dif1card  9932  infxpenlem  9935  fseqenlem1  9946  dfac12lem1  10066  dfac12lem2  10067  dfac12r  10069  pwsdompw  10125  ackbij1lem14  10154  ackbij1lem18  10158  ackbij1  10159  ackbij2lem3  10162  cfsmolem  10192  cfsmo  10193  sornom  10199  isfin3ds  10251  isf32lem1  10275  isf32lem2  10276  isf32lem5  10279  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  isf32lem11  10285  fin1a2lem1  10322  ituniiun  10344  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3lem4  10375  axdc3  10376  axdc4lem  10377  axcclem  10379  axdclem2  10442  wunex2  10661  om2uzsuci  13910  axdc4uzlem  13945  noresle  27661  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  noinfcbv  27681  noinfno  27682  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  bday1  27806  om2noseqlt  28291  bdayn0sf1o  28362  bnj222  35025  bnj966  35086  bnj1112  35125  fineqvnttrclselem3  35267  fineqvnttrclse  35268  fineqvinfep  35269  gonar  35577  goalr  35579  satffun  35591  rankaltopb  36161  ranksng  36349  rankpwg  36351  rankeq1o  36353  ontgsucval  36614  onsucconn  36620  onsucsuccmp  36626  limsucncmp  36628  ordcmp  36629  finxpreclem4  37710  finxp00  37718  brsucmap  38787  mopre  38792  limsuc2  43469  aomclem4  43485  aomclem8  43489  onsucelab  43691  onsucf1olem  43698  onsucrn  43699  onov0suclim  43702  onsucunifi  43798  sucunisn  43799  onsucunipr  43800  onsucunitp  43801  nadd1suc  43820  naddonnn  43823  onsetreclem1  50180