Theorem suceq 6258

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 4579	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4142	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6199	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6199	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2883	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3936  {csn 4569  suc csuc 6195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-suc 6199

This theorem is referenced by:  eqelsuc  6274  suc11  6296  ordunisuc  7549  onsucuni2  7551  onuninsuci  7557  limsuc  7566  tfindes  7579  tfinds2  7580  findes  7614  onnseq  7983  seqomlem0  8087  seqomlem1  8088  seqomlem4  8091  oasuc  8151  onasuc  8155  oa1suc  8158  oa0r  8165  o2p2e4  8168  o2p2e4OLD  8169  oaass  8189  oneo  8209  omeulem1  8210  oeeulem  8229  oeeui  8230  nna0r  8237  nnacom  8245  nnaass  8250  nnmsucr  8253  omabs  8276  nnneo  8280  nneob  8281  omsmolem  8282  omopthlem1  8284  limensuc  8696  infensuc  8697  nneneq  8702  unblem2  8773  unblem3  8774  suc11reg  9084  inf0  9086  inf3lem1  9093  dfom3  9112  cantnflt  9137  cantnflem1  9154  cnfcom  9165  r1elwf  9227  rankidb  9231  rankonidlem  9259  ranklim  9275  rankopb  9283  rankelop  9305  rankxpu  9307  rankmapu  9309  rankxplim  9310  cardsucnn  9416  dif1card  9438  infxpenlem  9441  fseqenlem1  9452  dfac12lem1  9571  dfac12lem2  9572  dfac12r  9574  pwsdompw  9628  ackbij1lem14  9657  ackbij1lem18  9661  ackbij1  9662  ackbij2lem3  9665  cfsmolem  9694  cfsmo  9695  sornom  9701  isfin3ds  9753  isf32lem1  9777  isf32lem2  9778  isf32lem5  9781  isf32lem6  9782  isf32lem7  9783  isf32lem8  9784  isf32lem11  9787  fin1a2lem1  9824  ituniiun  9846  axdc2lem  9872  axdc3lem2  9875  axdc3lem3  9876  axdc3lem4  9877  axdc3  9878  axdc4lem  9879  axcclem  9881  axdclem2  9944  wunex2  10162  om2uzsuci  13319  axdc4uzlem  13354  bnj222  32157  bnj966  32218  bnj1112  32257  gonar  32644  goalr  32646  satffun  32658  noresle  33202  nosupno  33205  nosupdm  33206  nosupfv  33208  nosupres  33209  nosupbnd1lem1  33210  nosupbnd1lem3  33212  nosupbnd1lem5  33214  nosupbnd2  33218  noetalem4  33222  noeta  33224  rankaltopb  33442  ranksng  33630  rankpwg  33632  rankeq1o  33634  ontgsucval  33782  onsucconn  33788  onsucsuccmp  33794  limsucncmp  33796  ordcmp  33797  finxpreclem4  34677  finxp00  34685  limsuc2  39648  aomclem4  39664  aomclem8  39668  suceqd  40570  onsetreclem1  44814