Theorem sumeq1d 15422

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

Syntax hints:   → wi 4   = wceq 1539  Σcsu 15406

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-xp 5596  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-iota 6395  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-seq 13731  df-sum 15407

This theorem is referenced by:  sumeq12dv  15427  sumeq12rdv  15428  fsumf1o  15444  sumss  15445  fsumcllem  15453  fsumsplit1  15466  fsum1  15468  fzosump1  15473  fsump1  15477  fsum2d  15492  fsumcom2  15495  fsumshftm  15502  fsumrev2  15503  telfsumo  15523  telfsum  15525  telfsum2  15526  fsumparts  15527  fsumiun  15542  bcxmas  15556  incexclem  15557  incexc2  15559  isumsplit  15561  isum1p  15562  arisum  15581  arisum2  15582  geoser  15588  pwdif  15589  geolim  15591  geo2sum2  15595  mertenslem1  15605  mertenslem2  15606  mertens  15607  bpolydiflem  15773  efcvgfsum  15804  fprodefsum  15813  eftlub  15827  effsumlt  15829  eirrlem  15922  pwp1fsum  16109  bitsinv1  16158  bitsinvp1  16165  pcfac  16609  prmreclem4  16629  prmreclem6  16631  ovoliunlem1  24675  uniioombllem3  24758  itg11  24864  dvfsumlem1  25199  dvfsumlem4  25202  dvfsum2  25207  elplyr  25371  coeeu  25395  coeeq  25397  plyco  25411  0dgrb  25416  dvply2g  25454  vieta1lem2  25480  vieta1  25481  aaliou3lem5  25516  aaliou3lem6  25517  aaliou3lem7  25518  taylpfval  25533  pserdvlem2  25596  abelthlem6  25604  logfac  25765  advlogexp  25819  emcllem2  26155  emcllem3  26156  emcllem7  26160  harmonicbnd  26162  harmonicbnd2  26163  harmonicbnd3  26166  harmonicbnd4  26169  chtval  26268  chpval  26280  chtfl  26307  chpfl  26308  chtprm  26311  chtnprm  26312  chpp1  26313  chtdif  26316  prmorcht  26336  musum  26349  muinv  26351  logfaclbnd  26379  logfacbnd3  26380  logexprlim  26382  chtppilimlem1  26630  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrisumlem3  26648  dchrisum  26649  dchrisum0fval  26662  dchrisum0ff  26664  dchrisum0flblem1  26665  dchrisum0lem2  26675  dchrisum0  26677  mulog2sumlem1  26691  2vmadivsumlem  26697  log2sumbnd  26701  logdivbnd  26713  selberg3lem1  26714  pntrsumbnd  26723  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntrlog2bndlem4  26737  pntpbnd1  26743  pntpbnd2  26744  pntlemf  26762  brcgr  27277  axlowdimlem16  27334  eengv  27356  finsumvtxdg2sstep  27925  eulerpartlemgs2  32356  signsvfn  32570  fsum2dsub  32596  reprval  32599  reprsuc  32604  hashrepr  32614  chpvalz  32617  chtvalz  32618  breprexplema  32619  breprexplemc  32621  breprexp  32622  breprexpnat  32623  vtsval  32626  circlemeth  32629  hgt750lemb  32645  hgt750lema  32646  tgoldbachgtda  32650  tgoldbachgt  32652  subfacval2  33158  subfaclim  33159  bccolsum  33714  knoppndvlem6  34706  mettrifi  35924  rrncmslem  35999  sticksstones6  40114  sticksstones7  40115  sticksstones8  40116  sticksstones9  40117  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones16  40125  fzosumm1  40225  k0004val  41767  binomcxplemnn0  41974  fsumnncl  43120  fsumiunss  43123  fsumsermpt  43127  sumnnodd  43178  dvnmul  43491  dvnprodlem3  43496  itgspltprt  43527  stoweidlem17  43565  stoweidlem20  43568  stirlinglem12  43633  dirkertrigeqlem1  43646  dirkertrigeqlem3  43648  fourierdlem83  43737  fourierdlem112  43766  fourierdlem113  43767  elaa2lem  43781  etransclem32  43814  sge00  43921  sge0iunmptlemre  43960  sge0reuzb  43993  meaiuninclem  44025  carageniuncllem1  44066  hoidmvlelem3  44142  nnsum3primes4  45251  nnsum3primesprm  45253  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  altgsumbcALT  45700  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  nn0sumshdiglem2  45979