Theorem sumeq1d 15614

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

Syntax hints:   → wi 4   = wceq 1541  Σcsu 15600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-xp 5627  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-iota 6445  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-seq 13916  df-sum 15601

This theorem is referenced by:  sumeq12dv  15620  sumeq12rdv  15621  fsumf1o  15637  sumss  15638  fsumcllem  15646  fsumsplit1  15659  fsum1  15661  fzosump1  15666  fsump1  15670  fsum2d  15685  fsumcom2  15688  fsumshftm  15695  fsumrev2  15696  telfsumo  15716  telfsum  15718  telfsum2  15719  fsumparts  15720  fsumiun  15735  bcxmas  15749  incexclem  15750  incexc2  15752  isumsplit  15754  isum1p  15755  arisum  15774  arisum2  15775  geoser  15781  pwdif  15782  geolim  15784  geo2sum2  15788  mertenslem1  15798  mertenslem2  15799  mertens  15800  bpolydiflem  15968  efcvgfsum  16000  fprodefsum  16009  eftlub  16025  effsumlt  16027  eirrlem  16120  pwp1fsum  16309  bitsinv1  16360  bitsinvp1  16367  pcfac  16818  prmreclem4  16838  prmreclem6  16840  ovoliunlem1  25450  uniioombllem3  25533  itg11  25639  dvfsumlem1  25979  dvfsumlem4  25983  dvfsum2  25988  elplyr  26153  coeeu  26177  coeeq  26179  plyco  26193  0dgrb  26198  dvply2g  26239  dvply2gOLD  26240  vieta1lem2  26266  vieta1  26267  aaliou3lem5  26302  aaliou3lem6  26303  aaliou3lem7  26304  taylpfval  26319  pserdvlem2  26385  abelthlem6  26393  logfac  26557  advlogexp  26611  emcllem2  26954  emcllem3  26955  emcllem7  26959  harmonicbnd  26961  harmonicbnd2  26962  harmonicbnd3  26965  harmonicbnd4  26968  chtval  27067  chpval  27079  chtfl  27106  chpfl  27107  chtprm  27110  chtnprm  27111  chpp1  27112  chtdif  27115  prmorcht  27135  musum  27148  muinv  27150  logfaclbnd  27180  logfacbnd3  27181  logexprlim  27183  chtppilimlem1  27431  rplogsumlem2  27443  rpvmasumlem  27445  dchrisumlem1  27447  dchrisumlem2  27448  dchrisumlem3  27449  dchrisum  27450  dchrisum0fval  27463  dchrisum0ff  27465  dchrisum0flblem1  27466  dchrisum0lem2  27476  dchrisum0  27478  mulog2sumlem1  27492  2vmadivsumlem  27498  log2sumbnd  27502  logdivbnd  27514  selberg3lem1  27515  pntrsumbnd  27524  pntrsumbnd2  27525  pntrlog2bndlem1  27535  pntrlog2bndlem4  27538  pntpbnd1  27544  pntpbnd2  27545  pntlemf  27563  brcgr  28899  axlowdimlem16  28956  eengv  28978  finsumvtxdg2sstep  29549  eulerpartlemgs2  34465  signsvfn  34667  fsum2dsub  34692  reprval  34695  reprsuc  34700  hashrepr  34710  chpvalz  34713  chtvalz  34714  breprexplema  34715  breprexplemc  34717  breprexp  34718  breprexpnat  34719  vtsval  34722  circlemeth  34725  hgt750lemb  34741  hgt750lema  34742  tgoldbachgtda  34746  tgoldbachgt  34748  subfacval2  35303  subfaclim  35304  bccolsum  35855  sumeq12sdv  36333  knoppndvlem6  36633  mettrifi  37870  rrncmslem  37945  sticksstones6  42317  sticksstones7  42318  sticksstones8  42319  sticksstones9  42320  sticksstones10  42321  sticksstones11  42322  sticksstones12a  42323  sticksstones12  42324  sticksstones16  42328  unitscyglem2  42362  unitscyglem4  42364  fzosumm1  42420  fz1sump1  42480  sumcubes  42483  k0004val  44307  binomcxplemnn0  44506  fsumnncl  45734  fsumiunss  45737  fsumsermpt  45741  sumnnodd  45792  dvnmul  46103  dvnprodlem3  46108  itgspltprt  46139  stoweidlem17  46177  stoweidlem20  46180  stirlinglem12  46245  dirkertrigeqlem1  46258  dirkertrigeqlem3  46260  fourierdlem83  46349  fourierdlem112  46378  fourierdlem113  46379  elaa2lem  46393  etransclem32  46426  sge00  46536  sge0iunmptlemre  46575  sge0reuzb  46608  meaiuninclem  46640  carageniuncllem1  46681  hoidmvlelem3  46757  nnsum3primes4  47950  nnsum3primesprm  47952  nnsum3primesgbe  47954  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  altgsumbcALT  48515  nn0sumshdiglemA  48781  nn0sumshdiglemB  48782  nn0sumshdiglem1  48783  nn0sumshdiglem2  48784