Theorem sumeq1d 15747

Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)

Hypothesis

Ref	Expression
sumeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sumeq1d	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Proof of Theorem sumeq1d

Step	Hyp	Ref	Expression
1		sumeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sumeq1 15736	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	syl 18	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1570  Σcsu 15733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-xp 5667  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-iota 6492  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-seq 14034  df-sum 15734

This theorem is referenced by:  sumeq12dv  15753  sumeq12rdv  15754  fsumf1o  15770  sumss  15771  fsumcllem  15779  fsumsplit1  15792  fsum1  15794  fzosump1  15799  fsump1  15803  fsum2d  15818  fsumcom2  15821  fsumshftm  15828  fsumrev2  15829  telfsumo  15850  telfsum  15852  telfsum2  15853  fsumparts  15854  fsumiun  15869  bcxmas  15885  incexclem  15886  incexc2  15888  isumsplit  15890  isum1p  15891  arisum  15910  arisum2  15911  geoser  15917  pwdif  15918  geolim  15920  geo2sum2  15924  mertenslem1  15934  mertenslem2  15935  mertens  15936  bpolydiflem  16103  efcvgfsum  16135  fprodefsum  16144  eftlub  16160  effsumlt  16162  eirrlem  16255  pwp1fsum  16444  bitsinv1  16495  bitsinvp1  16502  pcfac  16954  prmreclem4  16974  prmreclem6  16976  ovoliunlem1  25661  uniioombllem3  25744  itg11  25850  dvfsumlem1  26185  dvfsumlem4  26188  dvfsum2  26193  elplyr  26358  coeeu  26382  coeeq  26384  plyco  26398  0dgrb  26403  dvply2g  26446  vieta1lem2  26472  vieta1  26473  aaliou3lem5  26510  aaliou3lem6  26511  aaliou3lem7  26512  taylpfval  26528  pserdvlem2  26591  abelthlem6  26599  logfac  26766  advlogexp  26820  emcllem2  27161  emcllem3  27162  emcllem7  27166  harmonicbnd  27168  harmonicbnd2  27169  harmonicbnd3  27172  harmonicbnd4  27175  chtval  27274  chpval  27286  chtfl  27313  chpfl  27314  chtprm  27317  chtnprm  27318  chpp1  27319  chtdif  27322  prmorcht  27342  musum  27355  muinv  27357  logfaclbnd  27386  logfacbnd3  27387  logexprlim  27389  chtppilimlem1  27637  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrisumlem3  27655  dchrisum  27656  dchrisum0fval  27669  dchrisum0ff  27671  dchrisum0flblem1  27672  dchrisum0lem2  27682  dchrisum0  27684  mulog2sumlem1  27698  2vmadivsumlem  27704  log2sumbnd  27708  logdivbnd  27720  selberg3lem1  27721  pntrsumbnd  27730  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntrlog2bndlem4  27744  pntpbnd1  27750  pntpbnd2  27751  pntlemf  27769  brcgr  29250  axlowdimlem16  29307  eengv  29329  finsumvtxdg2sstep  29899  eulerpartlemgs2  34770  signsvfn  34969  fsum2dsub  34994  reprval  34997  reprsuc  35002  hashrepr  35012  chpvalz  35015  chtvalz  35016  breprexplema  35017  breprexplemc  35019  breprexp  35020  breprexpnat  35021  vtsval  35024  circlemeth  35027  hgt750lemb  35043  hgt750lema  35044  tgoldbachgtda  35048  tgoldbachgt  35050  subfacval2  35679  subfaclim  35680  bccolsum  36231  sumeq12sdv  36729  knoppndvlem6  37106  mettrifi  38408  rrncmslem  38483  sticksstones6  42918  sticksstones7  42919  sticksstones8  42920  sticksstones9  42921  sticksstones10  42922  sticksstones11  42923  sticksstones12a  42924  sticksstones12  42925  sticksstones16  42929  unitscyglem2  42963  unitscyglem4  42965  fzosumm1  43018  fz1sump1  43071  sumcubes  43074  k0004val  44876  binomcxplemnn0  45059  fsumnncl  46288  fsumiunss  46291  fsumsermpt  46295  sumnnodd  46346  dvnmul  46657  dvnprodlem3  46662  itgspltprt  46693  stoweidlem17  46731  stoweidlem20  46734  stirlinglem12  46799  dirkertrigeqlem1  46812  dirkertrigeqlem3  46814  fourierdlem83  46903  fourierdlem112  46932  fourierdlem113  46933  elaa2lem  46947  etransclem32  46980  sge00  47090  sge0iunmptlemre  47129  sge0reuzb  47162  meaiuninclem  47194  carageniuncllem1  47235  hoidmvlelem3  47311  ppivalnn  48384  nnsum3primes4  48553  nnsum3primesprm  48555  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  altgsumbcALT  49133  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  nn0sumshdiglem1  49401  nn0sumshdiglem2  49402