Theorem suceq 6316

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	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		sneq 4568	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4094	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6257	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6257	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3881  {csn 4558  suc csuc 6253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-suc 6257

This theorem is referenced by:  eqelsuc  6332  suc11  6354  ordunisuc  7654  onsucuni2  7656  onuninsuci  7662  limsuc  7671  tfindes  7684  tfinds2  7685  peano5  7714  findes  7723  onnseq  8146  seqomlem0  8250  seqomlem1  8251  seqomlem4  8254  oasuc  8316  onasuc  8320  oa1suc  8323  oa0r  8330  o2p2e4  8333  o2p2e4OLD  8334  oaass  8354  oneo  8374  omeulem1  8375  oeeulem  8394  oeeui  8395  nna0r  8402  nnacom  8410  nnaass  8415  nnmsucr  8418  omabs  8441  nnneo  8445  nneob  8446  omsmolem  8447  omopthlem1  8449  limensuc  8890  infensuc  8891  nneneq  8896  unblem2  8997  unblem3  8998  suc11reg  9307  inf0  9309  inf3lem1  9316  dfom3  9335  cantnflt  9360  cantnflem1  9377  cnfcom  9388  r1elwf  9485  rankidb  9489  rankonidlem  9517  ranklim  9533  rankopb  9541  rankelop  9563  rankxpu  9565  rankmapu  9567  rankxplim  9568  cardsucnn  9674  dif1card  9697  infxpenlem  9700  fseqenlem1  9711  dfac12lem1  9830  dfac12lem2  9831  dfac12r  9833  pwsdompw  9891  ackbij1lem14  9920  ackbij1lem18  9924  ackbij1  9925  ackbij2lem3  9928  cfsmolem  9957  cfsmo  9958  sornom  9964  isfin3ds  10016  isf32lem1  10040  isf32lem2  10041  isf32lem5  10044  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  isf32lem11  10050  fin1a2lem1  10087  ituniiun  10109  axdc2lem  10135  axdc3lem2  10138  axdc3lem3  10139  axdc3lem4  10140  axdc3  10141  axdc4lem  10142  axcclem  10144  axdclem2  10207  wunex2  10425  om2uzsuci  13596  axdc4uzlem  13631  bnj222  32763  bnj966  32824  bnj1112  32863  gonar  33257  goalr  33259  satffun  33271  eldifsucnn  33597  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  dmttrcl  33707  rnttrcl  33708  ttrclselem2  33712  noresle  33827  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2  33846  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  bday1s  33952  rankaltopb  34208  ranksng  34396  rankpwg  34398  rankeq1o  34400  ontgsucval  34548  onsucconn  34554  onsucsuccmp  34560  limsucncmp  34562  ordcmp  34563  finxpreclem4  35492  finxp00  35500  limsuc2  40782  aomclem4  40798  aomclem8  40802  suceqd  41711  onsetreclem1  46296