Theorem sumeq1d 15748

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

Syntax hints:   → wi 4   = wceq 1537  Σcsu 15734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-xp 5706  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-seq 14053  df-sum 15735

This theorem is referenced by:  sumeq12dv  15754  sumeq12rdv  15755  fsumf1o  15771  sumss  15772  fsumcllem  15780  fsumsplit1  15793  fsum1  15795  fzosump1  15800  fsump1  15804  fsum2d  15819  fsumcom2  15822  fsumshftm  15829  fsumrev2  15830  telfsumo  15850  telfsum  15852  telfsum2  15853  fsumparts  15854  fsumiun  15869  bcxmas  15883  incexclem  15884  incexc2  15886  isumsplit  15888  isum1p  15889  arisum  15908  arisum2  15909  geoser  15915  pwdif  15916  geolim  15918  geo2sum2  15922  mertenslem1  15932  mertenslem2  15933  mertens  15934  bpolydiflem  16102  efcvgfsum  16134  fprodefsum  16143  eftlub  16157  effsumlt  16159  eirrlem  16252  pwp1fsum  16439  bitsinv1  16488  bitsinvp1  16495  pcfac  16946  prmreclem4  16966  prmreclem6  16968  ovoliunlem1  25556  uniioombllem3  25639  itg11  25745  dvfsumlem1  26086  dvfsumlem4  26090  dvfsum2  26095  elplyr  26260  coeeu  26284  coeeq  26286  plyco  26300  0dgrb  26305  dvply2g  26344  dvply2gOLD  26345  vieta1lem2  26371  vieta1  26372  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  taylpfval  26424  pserdvlem2  26490  abelthlem6  26498  logfac  26661  advlogexp  26715  emcllem2  27058  emcllem3  27059  emcllem7  27063  harmonicbnd  27065  harmonicbnd2  27066  harmonicbnd3  27069  harmonicbnd4  27072  chtval  27171  chpval  27183  chtfl  27210  chpfl  27211  chtprm  27214  chtnprm  27215  chpp1  27216  chtdif  27219  prmorcht  27239  musum  27252  muinv  27254  logfaclbnd  27284  logfacbnd3  27285  logexprlim  27287  chtppilimlem1  27535  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  dchrisum  27554  dchrisum0fval  27567  dchrisum0ff  27569  dchrisum0flblem1  27570  dchrisum0lem2  27580  dchrisum0  27582  mulog2sumlem1  27596  2vmadivsumlem  27602  log2sumbnd  27606  logdivbnd  27618  selberg3lem1  27619  pntrsumbnd  27628  pntrsumbnd2  27629  pntrlog2bndlem1  27639  pntrlog2bndlem4  27642  pntpbnd1  27648  pntpbnd2  27649  pntlemf  27667  brcgr  28933  axlowdimlem16  28990  eengv  29012  finsumvtxdg2sstep  29585  eulerpartlemgs2  34345  signsvfn  34559  fsum2dsub  34584  reprval  34587  reprsuc  34592  hashrepr  34602  chpvalz  34605  chtvalz  34606  breprexplema  34607  breprexplemc  34609  breprexp  34610  breprexpnat  34611  vtsval  34614  circlemeth  34617  hgt750lemb  34633  hgt750lema  34634  tgoldbachgtda  34638  tgoldbachgt  34640  subfacval2  35155  subfaclim  35156  bccolsum  35701  sumeq12sdv  36183  knoppndvlem6  36483  mettrifi  37717  rrncmslem  37792  sticksstones6  42108  sticksstones7  42109  sticksstones8  42110  sticksstones9  42111  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones16  42119  unitscyglem2  42153  unitscyglem4  42155  fzosumm1  42245  fz1sump1  42298  sumcubes  42301  k0004val  44112  binomcxplemnn0  44318  fsumnncl  45493  fsumiunss  45496  fsumsermpt  45500  sumnnodd  45551  dvnmul  45864  dvnprodlem3  45869  itgspltprt  45900  stoweidlem17  45938  stoweidlem20  45941  stirlinglem12  46006  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  fourierdlem83  46110  fourierdlem112  46139  fourierdlem113  46140  elaa2lem  46154  etransclem32  46187  sge00  46297  sge0iunmptlemre  46336  sge0reuzb  46369  meaiuninclem  46401  carageniuncllem1  46442  hoidmvlelem3  46518  nnsum3primes4  47662  nnsum3primesprm  47664  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  altgsumbcALT  48078  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  nn0sumshdiglem2  48356