Theorem suceq 5790

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 4187	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3768	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 5729	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 5729	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2681	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1483   ∪ cun 3572  {csn 4177  suc csuc 5725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-suc 5729

This theorem is referenced by:  eqelsuc  5806  suc11  5831  ordunisuc  7032  onsucuni2  7034  onuninsuci  7040  limsuc  7049  tfindes  7062  tfinds2  7063  findes  7096  onnseq  7441  seqomlem0  7544  seqomlem1  7545  seqomlem4  7548  oasuc  7604  onasuc  7608  oa1suc  7611  oa0r  7618  o2p2e4  7621  oaass  7641  oneo  7661  omeulem1  7662  oeeulem  7681  oeeui  7682  nna0r  7689  nnacom  7697  nnaass  7702  nnmsucr  7705  omabs  7727  nnneo  7731  nneob  7732  omsmolem  7733  omopthlem1  7735  limensuc  8137  infensuc  8138  nneneq  8143  unblem2  8213  unblem3  8214  suc11reg  8516  inf0  8518  inf3lem1  8525  dfom3  8544  cantnflt  8569  cantnflem1  8586  cnfcom  8597  r1elwf  8659  rankidb  8663  rankonidlem  8691  ranklim  8707  rankopb  8715  rankelop  8737  rankxpu  8739  rankmapu  8741  rankxplim  8742  cardsucnn  8811  dif1card  8833  infxpenlem  8836  fseqenlem1  8847  dfac12lem1  8965  dfac12lem2  8966  dfac12r  8968  pwsdompw  9026  ackbij1lem5  9046  ackbij1lem14  9055  ackbij1lem18  9059  ackbij1  9060  ackbij2lem3  9063  cfsmolem  9092  cfsmo  9093  sornom  9099  isfin3ds  9151  isf32lem1  9175  isf32lem2  9176  isf32lem5  9179  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  isf32lem11  9185  fin1a2lem1  9222  ituniiun  9244  axdc2lem  9270  axdc3lem2  9273  axdc3lem3  9274  axdc3lem4  9275  axdc3  9276  axdc4lem  9277  axcclem  9279  axdclem2  9342  wunex2  9560  om2uzsuci  12747  axdc4uzlem  12782  bnj222  30953  bnj966  31014  bnj1112  31051  noresle  31846  nosupno  31849  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2  31862  noetalem4  31866  noeta  31868  rankaltopb  32086  ranksng  32274  rankpwg  32276  rankeq1o  32278  ontgsucval  32431  onsucconn  32437  onsucsuccmp  32443  limsucncmp  32445  ordcmp  32446  finxpreclem4  33231  finxp00  33239  limsuc2  37611  aomclem4  37627  aomclem8  37631  onsetreclem1  42448