Theorem suceq 6461

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 4658	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4192	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6401	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6401	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974  {csn 4648  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-suc 6401

This theorem is referenced by:  eqelsuc  6479  suc11  6502  ordunisuc  7868  onsucuni2  7870  onuninsuci  7877  limsuc  7886  tfindes  7900  tfinds2  7901  peano5  7932  findes  7940  onnseq  8400  seqomlem0  8505  seqomlem1  8506  seqomlem4  8509  oasuc  8580  onasuc  8584  oa1suc  8587  oa0r  8594  o2p2e4  8597  oaass  8617  oneo  8637  omeulem1  8638  oeeulem  8657  oeeui  8658  nna0r  8665  nnacom  8673  nnaass  8678  nnmsucr  8681  omabs  8707  nnneo  8711  nneob  8712  omsmolem  8713  omopthlem1  8715  eldifsucnn  8720  naddsuc2  8757  naddoa  8758  limensuc  9220  infensuc  9221  nneneq  9272  nneneqOLD  9284  unblem2  9357  unblem3  9358  suc11reg  9688  inf0  9690  inf3lem1  9697  dfom3  9716  cantnflt  9741  cantnflem1  9758  cnfcom  9769  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  r1elwf  9865  rankidb  9869  rankonidlem  9897  ranklim  9913  rankopb  9921  rankelop  9943  rankxpu  9945  rankmapu  9947  rankxplim  9948  cardsucnn  10054  dif1card  10079  infxpenlem  10082  fseqenlem1  10093  dfac12lem1  10213  dfac12lem2  10214  dfac12r  10216  pwsdompw  10272  ackbij1lem14  10301  ackbij1lem18  10305  ackbij1  10306  ackbij2lem3  10309  cfsmolem  10339  cfsmo  10340  sornom  10346  isfin3ds  10398  isf32lem1  10422  isf32lem2  10423  isf32lem5  10426  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  isf32lem11  10432  fin1a2lem1  10469  ituniiun  10491  axdc2lem  10517  axdc3lem2  10520  axdc3lem3  10521  axdc3lem4  10522  axdc3  10523  axdc4lem  10524  axcclem  10526  axdclem2  10589  wunex2  10807  om2uzsuci  13999  axdc4uzlem  14034  noresle  27760  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2  27779  noinfcbv  27780  noinfno  27781  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  bday1s  27894  om2noseqlt  28323  bnj222  34859  bnj966  34920  bnj1112  34959  gonar  35363  goalr  35365  satffun  35377  rankaltopb  35943  ranksng  36131  rankpwg  36133  rankeq1o  36135  ontgsucval  36398  onsucconn  36404  onsucsuccmp  36410  limsucncmp  36412  ordcmp  36413  finxpreclem4  37360  finxp00  37368  limsuc2  42998  aomclem4  43014  aomclem8  43018  onsucelab  43225  onsucf1olem  43232  onsucrn  43233  onov0suclim  43236  onsucunifi  43332  sucunisn  43333  onsucunipr  43334  onsucunitp  43335  nadd1suc  43354  naddonnn  43357  suceqd  44173  onsetreclem1  48797