Theorem sumeq1d 15718

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

Syntax hints:   → wi 4   = wceq 1559  Σcsu 15704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-xp 5649  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-iota 6472  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-oprab 7395  df-mpo 7396  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-seq 14009  df-sum 15705

This theorem is referenced by:  sumeq12dv  15724  sumeq12rdv  15725  fsumf1o  15741  sumss  15742  fsumcllem  15750  fsumsplit1  15763  fsum1  15765  fzosump1  15770  fsump1  15774  fsum2d  15789  fsumcom2  15792  fsumshftm  15799  fsumrev2  15800  telfsumo  15821  telfsum  15823  telfsum2  15824  fsumparts  15825  fsumiun  15840  bcxmas  15856  incexclem  15857  incexc2  15859  isumsplit  15861  isum1p  15862  arisum  15881  arisum2  15882  geoser  15888  pwdif  15889  geolim  15891  geo2sum2  15895  mertenslem1  15905  mertenslem2  15906  mertens  15907  bpolydiflem  16075  efcvgfsum  16107  fprodefsum  16116  eftlub  16132  effsumlt  16134  eirrlem  16227  pwp1fsum  16416  bitsinv1  16467  bitsinvp1  16474  pcfac  16926  prmreclem4  16946  prmreclem6  16948  ovoliunlem1  25552  uniioombllem3  25635  itg11  25741  dvfsumlem1  26076  dvfsumlem4  26079  dvfsum2  26084  elplyr  26249  coeeu  26273  coeeq  26275  plyco  26289  0dgrb  26294  dvply2g  26337  vieta1lem2  26363  vieta1  26364  aaliou3lem5  26399  aaliou3lem6  26400  aaliou3lem7  26401  taylpfval  26416  pserdvlem2  26479  abelthlem6  26487  logfac  26654  advlogexp  26708  emcllem2  27049  emcllem3  27050  emcllem7  27054  harmonicbnd  27056  harmonicbnd2  27057  harmonicbnd3  27060  harmonicbnd4  27063  chtval  27162  chpval  27174  chtfl  27201  chpfl  27202  chtprm  27205  chtnprm  27206  chpp1  27207  chtdif  27210  prmorcht  27230  musum  27243  muinv  27245  logfaclbnd  27274  logfacbnd3  27275  logexprlim  27277  chtppilimlem1  27525  rplogsumlem2  27537  rpvmasumlem  27539  dchrisumlem1  27541  dchrisumlem2  27542  dchrisumlem3  27543  dchrisum  27544  dchrisum0fval  27557  dchrisum0ff  27559  dchrisum0flblem1  27560  dchrisum0lem2  27570  dchrisum0  27572  mulog2sumlem1  27586  2vmadivsumlem  27592  log2sumbnd  27596  logdivbnd  27608  selberg3lem1  27609  pntrsumbnd  27618  pntrsumbnd2  27619  pntrlog2bndlem1  27629  pntrlog2bndlem4  27632  pntpbnd1  27638  pntpbnd2  27639  pntlemf  27657  brcgr  29058  axlowdimlem16  29115  eengv  29137  finsumvtxdg2sstep  29707  eulerpartlemgs2  34638  signsvfn  34837  fsum2dsub  34862  reprval  34865  reprsuc  34870  hashrepr  34880  chpvalz  34883  chtvalz  34884  breprexplema  34885  breprexplemc  34887  breprexp  34888  breprexpnat  34889  vtsval  34892  circlemeth  34895  hgt750lemb  34911  hgt750lema  34912  tgoldbachgtda  34916  tgoldbachgt  34918  subfacval2  35498  subfaclim  35499  bccolsum  36050  sumeq12sdv  36538  knoppndvlem6  36916  mettrifi  38217  rrncmslem  38292  sticksstones6  42729  sticksstones7  42730  sticksstones8  42731  sticksstones9  42732  sticksstones10  42733  sticksstones11  42734  sticksstones12a  42735  sticksstones12  42736  sticksstones16  42740  unitscyglem2  42774  unitscyglem4  42776  fzosumm1  42827  fz1sump1  42880  sumcubes  42883  k0004val  44687  binomcxplemnn0  44886  fsumnncl  46109  fsumiunss  46112  fsumsermpt  46116  sumnnodd  46167  dvnmul  46478  dvnprodlem3  46483  itgspltprt  46514  stoweidlem17  46552  stoweidlem20  46555  stirlinglem12  46620  dirkertrigeqlem1  46633  dirkertrigeqlem3  46635  fourierdlem83  46724  fourierdlem112  46753  fourierdlem113  46754  elaa2lem  46768  etransclem32  46801  sge00  46911  sge0iunmptlemre  46950  sge0reuzb  46983  meaiuninclem  47015  carageniuncllem1  47056  hoidmvlelem3  47132  ppivalnn  48202  nnsum3primes4  48371  nnsum3primesprm  48373  nnsum3primesgbe  48375  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  wtgoldbnnsum4prm  48385  bgoldbnnsum3prm  48387  altgsumbcALT  48936  nn0sumshdiglemA  49202  nn0sumshdiglemB  49203  nn0sumshdiglem1  49204  nn0sumshdiglem2  49205