Theorem sumeq1d 15647

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5683  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-iota 6496  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-seq 13967  df-sum 15633

This theorem is referenced by:  sumeq12dv  15652  sumeq12rdv  15653  fsumf1o  15669  sumss  15670  fsumcllem  15678  fsumsplit1  15691  fsum1  15693  fzosump1  15698  fsump1  15702  fsum2d  15717  fsumcom2  15720  fsumshftm  15727  fsumrev2  15728  telfsumo  15748  telfsum  15750  telfsum2  15751  fsumparts  15752  fsumiun  15767  bcxmas  15781  incexclem  15782  incexc2  15784  isumsplit  15786  isum1p  15787  arisum  15806  arisum2  15807  geoser  15813  pwdif  15814  geolim  15816  geo2sum2  15820  mertenslem1  15830  mertenslem2  15831  mertens  15832  bpolydiflem  15998  efcvgfsum  16029  fprodefsum  16038  eftlub  16052  effsumlt  16054  eirrlem  16147  pwp1fsum  16334  bitsinv1  16383  bitsinvp1  16390  pcfac  16832  prmreclem4  16852  prmreclem6  16854  ovoliunlem1  25019  uniioombllem3  25102  itg11  25208  dvfsumlem1  25543  dvfsumlem4  25546  dvfsum2  25551  elplyr  25715  coeeu  25739  coeeq  25741  plyco  25755  0dgrb  25760  dvply2g  25798  vieta1lem2  25824  vieta1  25825  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  taylpfval  25877  pserdvlem2  25940  abelthlem6  25948  logfac  26109  advlogexp  26163  emcllem2  26501  emcllem3  26502  emcllem7  26506  harmonicbnd  26508  harmonicbnd2  26509  harmonicbnd3  26512  harmonicbnd4  26515  chtval  26614  chpval  26626  chtfl  26653  chpfl  26654  chtprm  26657  chtnprm  26658  chpp1  26659  chtdif  26662  prmorcht  26682  musum  26695  muinv  26697  logfaclbnd  26725  logfacbnd3  26726  logexprlim  26728  chtppilimlem1  26976  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  dchrisum  26995  dchrisum0fval  27008  dchrisum0ff  27010  dchrisum0flblem1  27011  dchrisum0lem2  27021  dchrisum0  27023  mulog2sumlem1  27037  2vmadivsumlem  27043  log2sumbnd  27047  logdivbnd  27059  selberg3lem1  27060  pntrsumbnd  27069  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntrlog2bndlem4  27083  pntpbnd1  27089  pntpbnd2  27090  pntlemf  27108  brcgr  28158  axlowdimlem16  28215  eengv  28237  finsumvtxdg2sstep  28806  eulerpartlemgs2  33379  signsvfn  33593  fsum2dsub  33619  reprval  33622  reprsuc  33627  hashrepr  33637  chpvalz  33640  chtvalz  33641  breprexplema  33642  breprexplemc  33644  breprexp  33645  breprexpnat  33646  vtsval  33649  circlemeth  33652  hgt750lemb  33668  hgt750lema  33669  tgoldbachgtda  33673  tgoldbachgt  33675  subfacval2  34178  subfaclim  34179  bccolsum  34709  knoppndvlem6  35393  mettrifi  36625  rrncmslem  36700  sticksstones6  40967  sticksstones7  40968  sticksstones8  40969  sticksstones9  40970  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones16  40978  fzosumm1  41068  fz1sump1  41208  sumcubes  41211  k0004val  42901  binomcxplemnn0  43108  fsumnncl  44288  fsumiunss  44291  fsumsermpt  44295  sumnnodd  44346  dvnmul  44659  dvnprodlem3  44664  itgspltprt  44695  stoweidlem17  44733  stoweidlem20  44736  stirlinglem12  44801  dirkertrigeqlem1  44814  dirkertrigeqlem3  44816  fourierdlem83  44905  fourierdlem112  44934  fourierdlem113  44935  elaa2lem  44949  etransclem32  44982  sge00  45092  sge0iunmptlemre  45131  sge0reuzb  45164  meaiuninclem  45196  carageniuncllem1  45237  hoidmvlelem3  45313  nnsum3primes4  46456  nnsum3primesprm  46458  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  altgsumbcALT  47029  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  nn0sumshdiglem2  47308