Theorem sumeq1d 15341

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Allowed substitution hints:   𝜑(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq1d

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

Syntax hints:   → wi 4   = wceq 1539  Σcsu 15325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-xp 5586  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-iota 6376  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-seq 13650  df-sum 15326

This theorem is referenced by:  sumeq12dv  15346  sumeq12rdv  15347  fsumf1o  15363  sumss  15364  fsumcllem  15372  fsumsplit1  15385  fsum1  15387  fzosump1  15392  fsump1  15396  fsum2d  15411  fsumcom2  15414  fsumshftm  15421  fsumrev2  15422  telfsumo  15442  telfsum  15444  telfsum2  15445  fsumparts  15446  fsumiun  15461  bcxmas  15475  incexclem  15476  incexc2  15478  isumsplit  15480  isum1p  15481  arisum  15500  arisum2  15501  geoser  15507  pwdif  15508  geolim  15510  geo2sum2  15514  mertenslem1  15524  mertenslem2  15525  mertens  15526  bpolydiflem  15692  efcvgfsum  15723  fprodefsum  15732  eftlub  15746  effsumlt  15748  eirrlem  15841  pwp1fsum  16028  bitsinv1  16077  bitsinvp1  16084  pcfac  16528  prmreclem4  16548  prmreclem6  16550  ovoliunlem1  24571  uniioombllem3  24654  itg11  24760  dvfsumlem1  25095  dvfsumlem4  25098  dvfsum2  25103  elplyr  25267  coeeu  25291  coeeq  25293  plyco  25307  0dgrb  25312  dvply2g  25350  vieta1lem2  25376  vieta1  25377  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  taylpfval  25429  pserdvlem2  25492  abelthlem6  25500  logfac  25661  advlogexp  25715  emcllem2  26051  emcllem3  26052  emcllem7  26056  harmonicbnd  26058  harmonicbnd2  26059  harmonicbnd3  26062  harmonicbnd4  26065  chtval  26164  chpval  26176  chtfl  26203  chpfl  26204  chtprm  26207  chtnprm  26208  chpp1  26209  chtdif  26212  prmorcht  26232  musum  26245  muinv  26247  logfaclbnd  26275  logfacbnd3  26276  logexprlim  26278  chtppilimlem1  26526  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrisumlem3  26544  dchrisum  26545  dchrisum0fval  26558  dchrisum0ff  26560  dchrisum0flblem1  26561  dchrisum0lem2  26571  dchrisum0  26573  mulog2sumlem1  26587  2vmadivsumlem  26593  log2sumbnd  26597  logdivbnd  26609  selberg3lem1  26610  pntrsumbnd  26619  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntrlog2bndlem4  26633  pntpbnd1  26639  pntpbnd2  26640  pntlemf  26658  brcgr  27171  axlowdimlem16  27228  eengv  27250  finsumvtxdg2sstep  27819  eulerpartlemgs2  32247  signsvfn  32461  fsum2dsub  32487  reprval  32490  reprsuc  32495  hashrepr  32505  chpvalz  32508  chtvalz  32509  breprexplema  32510  breprexplemc  32512  breprexp  32513  breprexpnat  32514  vtsval  32517  circlemeth  32520  hgt750lemb  32536  hgt750lema  32537  tgoldbachgtda  32541  tgoldbachgt  32543  subfacval2  33049  subfaclim  33050  bccolsum  33611  knoppndvlem6  34624  mettrifi  35842  rrncmslem  35917  sticksstones6  40035  sticksstones7  40036  sticksstones8  40037  sticksstones9  40038  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones16  40046  fzosumm1  40144  k0004val  41649  binomcxplemnn0  41856  fsumnncl  43003  fsumiunss  43006  fsumsermpt  43010  sumnnodd  43061  dvnmul  43374  dvnprodlem3  43379  itgspltprt  43410  stoweidlem17  43448  stoweidlem20  43451  stirlinglem12  43516  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  fourierdlem83  43620  fourierdlem112  43649  fourierdlem113  43650  elaa2lem  43664  etransclem32  43697  sge00  43804  sge0iunmptlemre  43843  sge0reuzb  43876  meaiuninclem  43908  carageniuncllem1  43949  hoidmvlelem3  44025  nnsum3primes4  45128  nnsum3primesprm  45130  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  altgsumbcALT  45577  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  nn0sumshdiglem2  45856