Theorem suceq 6386

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-suc 6324

This theorem is referenced by:  eqelsuc  6404  suc11  6427  ordunisuc  7777  onsucuni2  7779  onuninsuci  7785  limsuc  7794  tfindes  7808  tfinds2  7809  peano5  7838  findes  7845  onnseq  8278  seqomlem0  8382  seqomlem1  8383  seqomlem4  8386  oasuc  8453  onasuc  8457  oa1suc  8460  oa0r  8467  o2p2e4  8470  oaass  8490  oneo  8510  omeulem1  8511  oeeulem  8531  oeeui  8532  nna0r  8539  nnacom  8547  nnaass  8552  nnmsucr  8555  omabs  8581  nnneo  8585  nneob  8586  omsmolem  8587  omopthlem1  8589  eldifsucnn  8594  naddsuc2  8631  naddoa  8632  limensuc  9086  infensuc  9087  nneneq  9134  unblem2  9197  unblem3  9198  suc11reg  9534  inf0  9536  inf3lem1  9543  dfom3  9562  cantnflt  9587  cantnflem1  9604  cnfcom  9615  brttrcl2  9629  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  r1elwf  9714  rankidb  9718  rankonidlem  9746  ranklim  9762  rankopb  9770  rankelop  9792  rankxpu  9794  rankmapu  9796  rankxplim  9797  cardsucnn  9903  dif1card  9926  infxpenlem  9929  fseqenlem1  9940  dfac12lem1  10060  dfac12lem2  10061  dfac12r  10063  pwsdompw  10119  ackbij1lem14  10148  ackbij1lem18  10152  ackbij1  10153  ackbij2lem3  10156  cfsmolem  10186  cfsmo  10187  sornom  10193  isfin3ds  10245  isf32lem1  10269  isf32lem2  10270  isf32lem5  10273  isf32lem6  10274  isf32lem7  10275  isf32lem8  10276  isf32lem11  10279  fin1a2lem1  10316  ituniiun  10338  axdc2lem  10364  axdc3lem2  10367  axdc3lem3  10368  axdc3lem4  10369  axdc3  10370  axdc4lem  10371  axcclem  10373  axdclem2  10436  wunex2  10655  om2uzsuci  13904  axdc4uzlem  13939  noresle  27678  nosupcbv  27683  nosupno  27684  nosupdm  27685  nosupfv  27687  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1lem3  27691  nosupbnd1lem5  27693  noinfcbv  27698  noinfno  27699  noinfdm  27700  noinffv  27702  noinfres  27703  noinfbnd1lem3  27706  noinfbnd1lem5  27708  bday1  27823  om2noseqlt  28308  bdayn0sf1o  28379  bnj222  35044  bnj966  35105  bnj1112  35144  fineqvnttrclselem3  35286  fineqvnttrclse  35287  fineqvinfep  35288  gonar  35596  goalr  35598  satffun  35610  rankaltopb  36180  ranksng  36368  rankpwg  36370  rankeq1o  36372  ontgsucval  36633  onsucconn  36639  onsucsuccmp  36645  limsucncmp  36647  ordcmp  36648  finxpreclem4  37727  finxp00  37735  brsucmap  38804  mopre  38809  limsuc2  43490  aomclem4  43506  aomclem8  43510  onsucelab  43712  onsucf1olem  43719  onsucrn  43720  onov0suclim  43723  onsucunifi  43819  sucunisn  43820  onsucunipr  43821  onsucunitp  43822  nadd1suc  43841  naddonnn  43844  onsetreclem1  50195