Theorem sumeq1d 15662

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

Syntax hints:   → wi 4   = wceq 1542  Σcsu 15648

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-iota 6454  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-seq 13964  df-sum 15649

This theorem is referenced by:  sumeq12dv  15668  sumeq12rdv  15669  fsumf1o  15685  sumss  15686  fsumcllem  15694  fsumsplit1  15707  fsum1  15709  fzosump1  15714  fsump1  15718  fsum2d  15733  fsumcom2  15736  fsumshftm  15743  fsumrev2  15744  telfsumo  15765  telfsum  15767  telfsum2  15768  fsumparts  15769  fsumiun  15784  bcxmas  15800  incexclem  15801  incexc2  15803  isumsplit  15805  isum1p  15806  arisum  15825  arisum2  15826  geoser  15832  pwdif  15833  geolim  15835  geo2sum2  15839  mertenslem1  15849  mertenslem2  15850  mertens  15851  bpolydiflem  16019  efcvgfsum  16051  fprodefsum  16060  eftlub  16076  effsumlt  16078  eirrlem  16171  pwp1fsum  16360  bitsinv1  16411  bitsinvp1  16418  pcfac  16870  prmreclem4  16890  prmreclem6  16892  ovoliunlem1  25469  uniioombllem3  25552  itg11  25658  dvfsumlem1  25993  dvfsumlem4  25996  dvfsum2  26001  elplyr  26166  coeeu  26190  coeeq  26192  plyco  26206  0dgrb  26211  dvply2g  26251  vieta1lem2  26277  vieta1  26278  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  taylpfval  26330  pserdvlem2  26393  abelthlem6  26401  logfac  26565  advlogexp  26619  emcllem2  26960  emcllem3  26961  emcllem7  26965  harmonicbnd  26967  harmonicbnd2  26968  harmonicbnd3  26971  harmonicbnd4  26974  chtval  27073  chpval  27085  chtfl  27112  chpfl  27113  chtprm  27116  chtnprm  27117  chpp1  27118  chtdif  27121  prmorcht  27141  musum  27154  muinv  27156  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  chtppilimlem1  27436  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum  27455  dchrisum0fval  27468  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0lem2  27481  dchrisum0  27483  mulog2sumlem1  27497  2vmadivsumlem  27503  log2sumbnd  27507  logdivbnd  27519  selberg3lem1  27520  pntrsumbnd  27529  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem4  27543  pntpbnd1  27549  pntpbnd2  27550  pntlemf  27568  brcgr  28969  axlowdimlem16  29026  eengv  29048  finsumvtxdg2sstep  29618  eulerpartlemgs2  34524  signsvfn  34726  fsum2dsub  34751  reprval  34754  reprsuc  34759  hashrepr  34769  chpvalz  34772  chtvalz  34773  breprexplema  34774  breprexplemc  34776  breprexp  34777  breprexpnat  34778  vtsval  34781  circlemeth  34784  hgt750lemb  34800  hgt750lema  34801  tgoldbachgtda  34805  tgoldbachgt  34807  subfacval2  35369  subfaclim  35370  bccolsum  35921  sumeq12sdv  36399  knoppndvlem6  36777  mettrifi  38078  rrncmslem  38153  sticksstones6  42590  sticksstones7  42591  sticksstones8  42592  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones16  42601  unitscyglem2  42635  unitscyglem4  42637  fzosumm1  42689  fz1sump1  42742  sumcubes  42745  k0004val  44577  binomcxplemnn0  44776  fsumnncl  46002  fsumiunss  46005  fsumsermpt  46009  sumnnodd  46060  dvnmul  46371  dvnprodlem3  46376  itgspltprt  46407  stoweidlem17  46445  stoweidlem20  46448  stirlinglem12  46513  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  fourierdlem83  46617  fourierdlem112  46646  fourierdlem113  46647  elaa2lem  46661  etransclem32  46694  sge00  46804  sge0iunmptlemre  46843  sge0reuzb  46876  meaiuninclem  46908  carageniuncllem1  46949  hoidmvlelem3  47025  ppivalnn  48095  nnsum3primes4  48264  nnsum3primesprm  48266  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  altgsumbcALT  48829  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  nn0sumshdiglem2  49098