Theorem sumeq1d 15642

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

Syntax hints:   → wi 4   = wceq 1540  Σcsu 15628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-xp 5637  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-iota 6452  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-seq 13943  df-sum 15629

This theorem is referenced by:  sumeq12dv  15648  sumeq12rdv  15649  fsumf1o  15665  sumss  15666  fsumcllem  15674  fsumsplit1  15687  fsum1  15689  fzosump1  15694  fsump1  15698  fsum2d  15713  fsumcom2  15716  fsumshftm  15723  fsumrev2  15724  telfsumo  15744  telfsum  15746  telfsum2  15747  fsumparts  15748  fsumiun  15763  bcxmas  15777  incexclem  15778  incexc2  15780  isumsplit  15782  isum1p  15783  arisum  15802  arisum2  15803  geoser  15809  pwdif  15810  geolim  15812  geo2sum2  15816  mertenslem1  15826  mertenslem2  15827  mertens  15828  bpolydiflem  15996  efcvgfsum  16028  fprodefsum  16037  eftlub  16053  effsumlt  16055  eirrlem  16148  pwp1fsum  16337  bitsinv1  16388  bitsinvp1  16395  pcfac  16846  prmreclem4  16866  prmreclem6  16868  ovoliunlem1  25379  uniioombllem3  25462  itg11  25568  dvfsumlem1  25908  dvfsumlem4  25912  dvfsum2  25917  elplyr  26082  coeeu  26106  coeeq  26108  plyco  26122  0dgrb  26127  dvply2g  26168  dvply2gOLD  26169  vieta1lem2  26195  vieta1  26196  aaliou3lem5  26231  aaliou3lem6  26232  aaliou3lem7  26233  taylpfval  26248  pserdvlem2  26314  abelthlem6  26322  logfac  26486  advlogexp  26540  emcllem2  26883  emcllem3  26884  emcllem7  26888  harmonicbnd  26890  harmonicbnd2  26891  harmonicbnd3  26894  harmonicbnd4  26897  chtval  26996  chpval  27008  chtfl  27035  chpfl  27036  chtprm  27039  chtnprm  27040  chpp1  27041  chtdif  27044  prmorcht  27064  musum  27077  muinv  27079  logfaclbnd  27109  logfacbnd3  27110  logexprlim  27112  chtppilimlem1  27360  rplogsumlem2  27372  rpvmasumlem  27374  dchrisumlem1  27376  dchrisumlem2  27377  dchrisumlem3  27378  dchrisum  27379  dchrisum0fval  27392  dchrisum0ff  27394  dchrisum0flblem1  27395  dchrisum0lem2  27405  dchrisum0  27407  mulog2sumlem1  27421  2vmadivsumlem  27427  log2sumbnd  27431  logdivbnd  27443  selberg3lem1  27444  pntrsumbnd  27453  pntrsumbnd2  27454  pntrlog2bndlem1  27464  pntrlog2bndlem4  27467  pntpbnd1  27473  pntpbnd2  27474  pntlemf  27492  brcgr  28803  axlowdimlem16  28860  eengv  28882  finsumvtxdg2sstep  29453  eulerpartlemgs2  34344  signsvfn  34546  fsum2dsub  34571  reprval  34574  reprsuc  34579  hashrepr  34589  chpvalz  34592  chtvalz  34593  breprexplema  34594  breprexplemc  34596  breprexp  34597  breprexpnat  34598  vtsval  34601  circlemeth  34604  hgt750lemb  34620  hgt750lema  34621  tgoldbachgtda  34625  tgoldbachgt  34627  subfacval2  35147  subfaclim  35148  bccolsum  35699  sumeq12sdv  36178  knoppndvlem6  36478  mettrifi  37724  rrncmslem  37799  sticksstones6  42112  sticksstones7  42113  sticksstones8  42114  sticksstones9  42115  sticksstones10  42116  sticksstones11  42117  sticksstones12a  42118  sticksstones12  42119  sticksstones16  42123  unitscyglem2  42157  unitscyglem4  42159  fzosumm1  42211  fz1sump1  42271  sumcubes  42274  k0004val  44112  binomcxplemnn0  44311  fsumnncl  45543  fsumiunss  45546  fsumsermpt  45550  sumnnodd  45601  dvnmul  45914  dvnprodlem3  45919  itgspltprt  45950  stoweidlem17  45988  stoweidlem20  45991  stirlinglem12  46056  dirkertrigeqlem1  46069  dirkertrigeqlem3  46071  fourierdlem83  46160  fourierdlem112  46189  fourierdlem113  46190  elaa2lem  46204  etransclem32  46237  sge00  46347  sge0iunmptlemre  46386  sge0reuzb  46419  meaiuninclem  46451  carageniuncllem1  46492  hoidmvlelem3  46568  nnsum3primes4  47762  nnsum3primesprm  47764  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  altgsumbcALT  48314  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0sumshdiglem1  48583  nn0sumshdiglem2  48584