Theorem suceq 6442

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 4643	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4164	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6382	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6382	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1534   ∪ cun 3945  {csn 4633  suc csuc 6378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-sn 4634  df-suc 6382

This theorem is referenced by:  eqelsuc  6460  suc11  6483  ordunisuc  7841  onsucuni2  7843  onuninsuci  7850  limsuc  7859  tfindes  7873  tfinds2  7874  peano5  7905  findes  7913  onnseq  8374  seqomlem0  8479  seqomlem1  8480  seqomlem4  8483  oasuc  8554  onasuc  8558  oa1suc  8561  oa0r  8568  o2p2e4  8571  oaass  8591  oneo  8611  omeulem1  8612  oeeulem  8631  oeeui  8632  nna0r  8639  nnacom  8647  nnaass  8652  nnmsucr  8655  omabs  8681  nnneo  8685  nneob  8686  omsmolem  8687  omopthlem1  8689  eldifsucnn  8694  limensuc  9192  infensuc  9193  nneneq  9243  nneneqOLD  9255  unblem2  9330  unblem3  9331  suc11reg  9662  inf0  9664  inf3lem1  9671  dfom3  9690  cantnflt  9715  cantnflem1  9732  cnfcom  9743  brttrcl2  9757  ssttrcl  9758  ttrcltr  9759  ttrclss  9763  dmttrcl  9764  rnttrcl  9765  ttrclselem2  9769  r1elwf  9839  rankidb  9843  rankonidlem  9871  ranklim  9887  rankopb  9895  rankelop  9917  rankxpu  9919  rankmapu  9921  rankxplim  9922  cardsucnn  10028  dif1card  10053  infxpenlem  10056  fseqenlem1  10067  dfac12lem1  10186  dfac12lem2  10187  dfac12r  10189  pwsdompw  10247  ackbij1lem14  10276  ackbij1lem18  10280  ackbij1  10281  ackbij2lem3  10284  cfsmolem  10313  cfsmo  10314  sornom  10320  isfin3ds  10372  isf32lem1  10396  isf32lem2  10397  isf32lem5  10400  isf32lem6  10401  isf32lem7  10402  isf32lem8  10403  isf32lem11  10406  fin1a2lem1  10443  ituniiun  10465  axdc2lem  10491  axdc3lem2  10494  axdc3lem3  10495  axdc3lem4  10496  axdc3  10497  axdc4lem  10498  axcclem  10500  axdclem2  10563  wunex2  10781  om2uzsuci  13968  axdc4uzlem  14003  noresle  27727  nosupcbv  27732  nosupno  27733  nosupdm  27734  nosupfv  27736  nosupres  27737  nosupbnd1lem1  27738  nosupbnd1lem3  27740  nosupbnd1lem5  27742  nosupbnd2  27746  noinfcbv  27747  noinfno  27748  noinfdm  27749  noinffv  27751  noinfres  27752  noinfbnd1lem3  27755  noinfbnd1lem5  27757  bday1s  27861  om2noseqlt  28273  bnj222  34728  bnj966  34789  bnj1112  34828  gonar  35223  goalr  35225  satffun  35237  rankaltopb  35803  ranksng  35991  rankpwg  35993  rankeq1o  35995  ontgsucval  36144  onsucconn  36150  onsucsuccmp  36156  limsucncmp  36158  ordcmp  36159  finxpreclem4  37101  finxp00  37109  limsuc2  42702  aomclem4  42718  aomclem8  42722  onsucelab  42929  onsucf1olem  42936  onsucrn  42937  onov0suclim  42940  onsucunifi  43036  sucunisn  43037  onsucunipr  43038  onsucunitp  43039  nadd1suc  43058  naddsuc2  43059  naddonnn  43062  suceqd  43878  onsetreclem1  48451