Theorem suceq 6400

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

Syntax hints:   → wi 4   = wceq 1540  suc csuc 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-suc 6338

This theorem is referenced by:  eqelsuc  6418  suc11  6441  ordunisuc  7807  onsucuni2  7809  onuninsuci  7816  limsuc  7825  tfindes  7839  tfinds2  7840  peano5  7869  findes  7876  onnseq  8313  seqomlem0  8417  seqomlem1  8418  seqomlem4  8421  oasuc  8488  onasuc  8492  oa1suc  8495  oa0r  8502  o2p2e4  8505  oaass  8525  oneo  8545  omeulem1  8546  oeeulem  8565  oeeui  8566  nna0r  8573  nnacom  8581  nnaass  8586  nnmsucr  8589  omabs  8615  nnneo  8619  nneob  8620  omsmolem  8621  omopthlem1  8623  eldifsucnn  8628  naddsuc2  8665  naddoa  8666  limensuc  9118  infensuc  9119  nneneq  9170  unblem2  9240  unblem3  9241  suc11reg  9572  inf0  9574  inf3lem1  9581  dfom3  9600  cantnflt  9625  cantnflem1  9642  cnfcom  9653  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  r1elwf  9749  rankidb  9753  rankonidlem  9781  ranklim  9797  rankopb  9805  rankelop  9827  rankxpu  9829  rankmapu  9831  rankxplim  9832  cardsucnn  9938  dif1card  9963  infxpenlem  9966  fseqenlem1  9977  dfac12lem1  10097  dfac12lem2  10098  dfac12r  10100  pwsdompw  10156  ackbij1lem14  10185  ackbij1lem18  10189  ackbij1  10190  ackbij2lem3  10193  cfsmolem  10223  cfsmo  10224  sornom  10230  isfin3ds  10282  isf32lem1  10306  isf32lem2  10307  isf32lem5  10310  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  isf32lem11  10316  fin1a2lem1  10353  ituniiun  10375  axdc2lem  10401  axdc3lem2  10404  axdc3lem3  10405  axdc3lem4  10406  axdc3  10407  axdc4lem  10408  axcclem  10410  axdclem2  10473  wunex2  10691  om2uzsuci  13913  axdc4uzlem  13948  noresle  27609  nosupcbv  27614  nosupno  27615  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  noinfcbv  27629  noinfno  27630  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  bday1s  27743  om2noseqlt  28193  bdayn0sf1o  28259  bnj222  34873  bnj966  34934  bnj1112  34973  gonar  35382  goalr  35384  satffun  35396  rankaltopb  35967  ranksng  36155  rankpwg  36157  rankeq1o  36159  ontgsucval  36420  onsucconn  36426  onsucsuccmp  36432  limsucncmp  36434  ordcmp  36435  finxpreclem4  37382  finxp00  37390  limsuc2  43030  aomclem4  43046  aomclem8  43050  onsucelab  43252  onsucf1olem  43259  onsucrn  43260  onov0suclim  43263  onsucunifi  43359  sucunisn  43360  onsucunipr  43361  onsucunitp  43362  nadd1suc  43381  naddonnn  43384  onsetreclem1  49694