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  28189  axlowdimlem16  28246  eengv  28268  finsumvtxdg2sstep  28837  eulerpartlemgs2  33410  signsvfn  33624  fsum2dsub  33650  reprval  33653  reprsuc  33658  hashrepr  33668  chpvalz  33671  chtvalz  33672  breprexplema  33673  breprexplemc  33675  breprexp  33676  breprexpnat  33677  vtsval  33680  circlemeth  33683  hgt750lemb  33699  hgt750lema  33700  tgoldbachgtda  33704  tgoldbachgt  33706  subfacval2  34209  subfaclim  34210  bccolsum  34740  knoppndvlem6  35441  mettrifi  36673  rrncmslem  36748  sticksstones6  41015  sticksstones7  41016  sticksstones8  41017  sticksstones9  41018  sticksstones10  41019  sticksstones11  41020  sticksstones12a  41021  sticksstones12  41022  sticksstones16  41026  fzosumm1  41116  fz1sump1  41256  sumcubes  41259  k0004val  42949  binomcxplemnn0  43156  fsumnncl  44336  fsumiunss  44339  fsumsermpt  44343  sumnnodd  44394  dvnmul  44707  dvnprodlem3  44712  itgspltprt  44743  stoweidlem17  44781  stoweidlem20  44784  stirlinglem12  44849  dirkertrigeqlem1  44862  dirkertrigeqlem3  44864  fourierdlem83  44953  fourierdlem112  44982  fourierdlem113  44983  elaa2lem  44997  etransclem32  45030  sge00  45140  sge0iunmptlemre  45179  sge0reuzb  45212  meaiuninclem  45244  carageniuncllem1  45285  hoidmvlelem3  45361  nnsum3primes4  46504  nnsum3primesprm  46506  nnsum3primesgbe  46508  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  wtgoldbnnsum4prm  46518  bgoldbnnsum3prm  46520  altgsumbcALT  47077  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  nn0sumshdiglem1  47355  nn0sumshdiglem2  47356