Theorem suceq 6450

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 4636	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4169	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6390	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6390	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3949  {csn 4626  suc csuc 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-suc 6390

This theorem is referenced by:  eqelsuc  6468  suc11  6491  ordunisuc  7852  onsucuni2  7854  onuninsuci  7861  limsuc  7870  tfindes  7884  tfinds2  7885  peano5  7915  findes  7922  onnseq  8384  seqomlem0  8489  seqomlem1  8490  seqomlem4  8493  oasuc  8562  onasuc  8566  oa1suc  8569  oa0r  8576  o2p2e4  8579  oaass  8599  oneo  8619  omeulem1  8620  oeeulem  8639  oeeui  8640  nna0r  8647  nnacom  8655  nnaass  8660  nnmsucr  8663  omabs  8689  nnneo  8693  nneob  8694  omsmolem  8695  omopthlem1  8697  eldifsucnn  8702  naddsuc2  8739  naddoa  8740  limensuc  9194  infensuc  9195  nneneq  9246  nneneqOLD  9258  unblem2  9329  unblem3  9330  suc11reg  9659  inf0  9661  inf3lem1  9668  dfom3  9687  cantnflt  9712  cantnflem1  9729  cnfcom  9740  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  dmttrcl  9761  rnttrcl  9762  ttrclselem2  9766  r1elwf  9836  rankidb  9840  rankonidlem  9868  ranklim  9884  rankopb  9892  rankelop  9914  rankxpu  9916  rankmapu  9918  rankxplim  9919  cardsucnn  10025  dif1card  10050  infxpenlem  10053  fseqenlem1  10064  dfac12lem1  10184  dfac12lem2  10185  dfac12r  10187  pwsdompw  10243  ackbij1lem14  10272  ackbij1lem18  10276  ackbij1  10277  ackbij2lem3  10280  cfsmolem  10310  cfsmo  10311  sornom  10317  isfin3ds  10369  isf32lem1  10393  isf32lem2  10394  isf32lem5  10397  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  isf32lem11  10403  fin1a2lem1  10440  ituniiun  10462  axdc2lem  10488  axdc3lem2  10491  axdc3lem3  10492  axdc3lem4  10493  axdc3  10494  axdc4lem  10495  axcclem  10497  axdclem2  10560  wunex2  10778  om2uzsuci  13989  axdc4uzlem  14024  noresle  27742  nosupcbv  27747  nosupno  27748  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2  27761  noinfcbv  27762  noinfno  27763  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem5  27772  bday1s  27876  om2noseqlt  28305  bnj222  34897  bnj966  34958  bnj1112  34997  gonar  35400  goalr  35402  satffun  35414  rankaltopb  35980  ranksng  36168  rankpwg  36170  rankeq1o  36172  ontgsucval  36433  onsucconn  36439  onsucsuccmp  36445  limsucncmp  36447  ordcmp  36448  finxpreclem4  37395  finxp00  37403  limsuc2  43053  aomclem4  43069  aomclem8  43073  onsucelab  43276  onsucf1olem  43283  onsucrn  43284  onov0suclim  43287  onsucunifi  43383  sucunisn  43384  onsucunipr  43385  onsucunitp  43386  nadd1suc  43405  naddonnn  43408  suceqd  44223  onsetreclem1  49224