Theorem suceq 6451

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 4640	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4178	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6391	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6391	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3960  {csn 4630  suc csuc 6387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-suc 6391

This theorem is referenced by:  eqelsuc  6469  suc11  6492  ordunisuc  7851  onsucuni2  7853  onuninsuci  7860  limsuc  7869  tfindes  7883  tfinds2  7884  peano5  7915  findes  7922  onnseq  8382  seqomlem0  8487  seqomlem1  8488  seqomlem4  8491  oasuc  8560  onasuc  8564  oa1suc  8567  oa0r  8574  o2p2e4  8577  oaass  8597  oneo  8617  omeulem1  8618  oeeulem  8637  oeeui  8638  nna0r  8645  nnacom  8653  nnaass  8658  nnmsucr  8661  omabs  8687  nnneo  8691  nneob  8692  omsmolem  8693  omopthlem1  8695  eldifsucnn  8700  naddsuc2  8737  naddoa  8738  limensuc  9192  infensuc  9193  nneneq  9243  nneneqOLD  9255  unblem2  9326  unblem3  9327  suc11reg  9656  inf0  9658  inf3lem1  9665  dfom3  9684  cantnflt  9709  cantnflem1  9726  cnfcom  9737  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  dmttrcl  9758  rnttrcl  9759  ttrclselem2  9763  r1elwf  9833  rankidb  9837  rankonidlem  9865  ranklim  9881  rankopb  9889  rankelop  9911  rankxpu  9913  rankmapu  9915  rankxplim  9916  cardsucnn  10022  dif1card  10047  infxpenlem  10050  fseqenlem1  10061  dfac12lem1  10181  dfac12lem2  10182  dfac12r  10184  pwsdompw  10240  ackbij1lem14  10269  ackbij1lem18  10273  ackbij1  10274  ackbij2lem3  10277  cfsmolem  10307  cfsmo  10308  sornom  10314  isfin3ds  10366  isf32lem1  10390  isf32lem2  10391  isf32lem5  10394  isf32lem6  10395  isf32lem7  10396  isf32lem8  10397  isf32lem11  10400  fin1a2lem1  10437  ituniiun  10459  axdc2lem  10485  axdc3lem2  10488  axdc3lem3  10489  axdc3lem4  10490  axdc3  10491  axdc4lem  10492  axcclem  10494  axdclem2  10557  wunex2  10775  om2uzsuci  13985  axdc4uzlem  14020  noresle  27756  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2  27775  noinfcbv  27776  noinfno  27777  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  bday1s  27890  om2noseqlt  28319  bnj222  34875  bnj966  34936  bnj1112  34975  gonar  35379  goalr  35381  satffun  35393  rankaltopb  35960  ranksng  36148  rankpwg  36150  rankeq1o  36152  ontgsucval  36414  onsucconn  36420  onsucsuccmp  36426  limsucncmp  36428  ordcmp  36429  finxpreclem4  37376  finxp00  37384  limsuc2  43029  aomclem4  43045  aomclem8  43049  onsucelab  43252  onsucf1olem  43259  onsucrn  43260  onov0suclim  43263  onsucunifi  43359  sucunisn  43360  onsucunipr  43361  onsucunitp  43362  nadd1suc  43381  naddonnn  43384  suceqd  44199  onsetreclem1  48935