Theorem sumeq1d 15629

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 15617	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   = wceq 1541  Σcsu 15614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-xp 5675  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-iota 6484  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-oprab 7397  df-mpo 7398  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-seq 13949  df-sum 15615

This theorem is referenced by:  sumeq12dv  15634  sumeq12rdv  15635  fsumf1o  15651  sumss  15652  fsumcllem  15660  fsumsplit1  15673  fsum1  15675  fzosump1  15680  fsump1  15684  fsum2d  15699  fsumcom2  15702  fsumshftm  15709  fsumrev2  15710  telfsumo  15730  telfsum  15732  telfsum2  15733  fsumparts  15734  fsumiun  15749  bcxmas  15763  incexclem  15764  incexc2  15766  isumsplit  15768  isum1p  15769  arisum  15788  arisum2  15789  geoser  15795  pwdif  15796  geolim  15798  geo2sum2  15802  mertenslem1  15812  mertenslem2  15813  mertens  15814  bpolydiflem  15980  efcvgfsum  16011  fprodefsum  16020  eftlub  16034  effsumlt  16036  eirrlem  16129  pwp1fsum  16316  bitsinv1  16365  bitsinvp1  16372  pcfac  16814  prmreclem4  16834  prmreclem6  16836  ovoliunlem1  24948  uniioombllem3  25031  itg11  25137  dvfsumlem1  25472  dvfsumlem4  25475  dvfsum2  25480  elplyr  25644  coeeu  25668  coeeq  25670  plyco  25684  0dgrb  25689  dvply2g  25727  vieta1lem2  25753  vieta1  25754  aaliou3lem5  25789  aaliou3lem6  25790  aaliou3lem7  25791  taylpfval  25806  pserdvlem2  25869  abelthlem6  25877  logfac  26038  advlogexp  26092  emcllem2  26428  emcllem3  26429  emcllem7  26433  harmonicbnd  26435  harmonicbnd2  26436  harmonicbnd3  26439  harmonicbnd4  26442  chtval  26541  chpval  26553  chtfl  26580  chpfl  26581  chtprm  26584  chtnprm  26585  chpp1  26586  chtdif  26589  prmorcht  26609  musum  26622  muinv  26624  logfaclbnd  26652  logfacbnd3  26653  logexprlim  26655  chtppilimlem1  26903  rplogsumlem2  26915  rpvmasumlem  26917  dchrisumlem1  26919  dchrisumlem2  26920  dchrisumlem3  26921  dchrisum  26922  dchrisum0fval  26935  dchrisum0ff  26937  dchrisum0flblem1  26938  dchrisum0lem2  26948  dchrisum0  26950  mulog2sumlem1  26964  2vmadivsumlem  26970  log2sumbnd  26974  logdivbnd  26986  selberg3lem1  26987  pntrsumbnd  26996  pntrsumbnd2  26997  pntrlog2bndlem1  27007  pntrlog2bndlem4  27010  pntpbnd1  27016  pntpbnd2  27017  pntlemf  27035  brcgr  28023  axlowdimlem16  28080  eengv  28102  finsumvtxdg2sstep  28671  eulerpartlemgs2  33210  signsvfn  33424  fsum2dsub  33450  reprval  33453  reprsuc  33458  hashrepr  33468  chpvalz  33471  chtvalz  33472  breprexplema  33473  breprexplemc  33475  breprexp  33476  breprexpnat  33477  vtsval  33480  circlemeth  33483  hgt750lemb  33499  hgt750lema  33500  tgoldbachgtda  33504  tgoldbachgt  33506  subfacval2  34009  subfaclim  34010  bccolsum  34539  knoppndvlem6  35197  mettrifi  36430  rrncmslem  36505  sticksstones6  40772  sticksstones7  40773  sticksstones8  40774  sticksstones9  40775  sticksstones10  40776  sticksstones11  40777  sticksstones12a  40778  sticksstones12  40779  sticksstones16  40783  fzosumm1  40875  k0004val  42672  binomcxplemnn0  42879  fsumnncl  44061  fsumiunss  44064  fsumsermpt  44068  sumnnodd  44119  dvnmul  44432  dvnprodlem3  44437  itgspltprt  44468  stoweidlem17  44506  stoweidlem20  44509  stirlinglem12  44574  dirkertrigeqlem1  44587  dirkertrigeqlem3  44589  fourierdlem83  44678  fourierdlem112  44707  fourierdlem113  44708  elaa2lem  44722  etransclem32  44755  sge00  44865  sge0iunmptlemre  44904  sge0reuzb  44937  meaiuninclem  44969  carageniuncllem1  45010  hoidmvlelem3  45086  nnsum3primes4  46228  nnsum3primesprm  46230  nnsum3primesgbe  46232  nnsum4primesodd  46236  nnsum4primesoddALTV  46237  wtgoldbnnsum4prm  46242  bgoldbnnsum3prm  46244  altgsumbcALT  46677  nn0sumshdiglemA  46953  nn0sumshdiglemB  46954  nn0sumshdiglem1  46955  nn0sumshdiglem2  46956