Theorem sumeq1d 15653

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

Syntax hints:   → wi 4   = wceq 1542  Σcsu 15639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-xp 5630  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-iota 6448  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-seq 13955  df-sum 15640

This theorem is referenced by:  sumeq12dv  15659  sumeq12rdv  15660  fsumf1o  15676  sumss  15677  fsumcllem  15685  fsumsplit1  15698  fsum1  15700  fzosump1  15705  fsump1  15709  fsum2d  15724  fsumcom2  15727  fsumshftm  15734  fsumrev2  15735  telfsumo  15756  telfsum  15758  telfsum2  15759  fsumparts  15760  fsumiun  15775  bcxmas  15791  incexclem  15792  incexc2  15794  isumsplit  15796  isum1p  15797  arisum  15816  arisum2  15817  geoser  15823  pwdif  15824  geolim  15826  geo2sum2  15830  mertenslem1  15840  mertenslem2  15841  mertens  15842  bpolydiflem  16010  efcvgfsum  16042  fprodefsum  16051  eftlub  16067  effsumlt  16069  eirrlem  16162  pwp1fsum  16351  bitsinv1  16402  bitsinvp1  16409  pcfac  16861  prmreclem4  16881  prmreclem6  16883  ovoliunlem1  25479  uniioombllem3  25562  itg11  25668  dvfsumlem1  26003  dvfsumlem4  26006  dvfsum2  26011  elplyr  26176  coeeu  26200  coeeq  26202  plyco  26216  0dgrb  26221  dvply2g  26261  dvply2gOLD  26262  vieta1lem2  26288  vieta1  26289  aaliou3lem5  26324  aaliou3lem6  26325  aaliou3lem7  26326  taylpfval  26341  pserdvlem2  26406  abelthlem6  26414  logfac  26578  advlogexp  26632  emcllem2  26974  emcllem3  26975  emcllem7  26979  harmonicbnd  26981  harmonicbnd2  26982  harmonicbnd3  26985  harmonicbnd4  26988  chtval  27087  chpval  27099  chtfl  27126  chpfl  27127  chtprm  27130  chtnprm  27131  chpp1  27132  chtdif  27135  prmorcht  27155  musum  27168  muinv  27170  logfaclbnd  27199  logfacbnd3  27200  logexprlim  27202  chtppilimlem1  27450  rplogsumlem2  27462  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem2  27467  dchrisumlem3  27468  dchrisum  27469  dchrisum0fval  27482  dchrisum0ff  27484  dchrisum0flblem1  27485  dchrisum0lem2  27495  dchrisum0  27497  mulog2sumlem1  27511  2vmadivsumlem  27517  log2sumbnd  27521  logdivbnd  27533  selberg3lem1  27534  pntrsumbnd  27543  pntrsumbnd2  27544  pntrlog2bndlem1  27554  pntrlog2bndlem4  27557  pntpbnd1  27563  pntpbnd2  27564  pntlemf  27582  brcgr  28983  axlowdimlem16  29040  eengv  29062  finsumvtxdg2sstep  29633  eulerpartlemgs2  34540  signsvfn  34742  fsum2dsub  34767  reprval  34770  reprsuc  34775  hashrepr  34785  chpvalz  34788  chtvalz  34789  breprexplema  34790  breprexplemc  34792  breprexp  34793  breprexpnat  34794  vtsval  34797  circlemeth  34800  hgt750lemb  34816  hgt750lema  34817  tgoldbachgtda  34821  tgoldbachgt  34823  subfacval2  35385  subfaclim  35386  bccolsum  35937  sumeq12sdv  36415  knoppndvlem6  36793  mettrifi  38092  rrncmslem  38167  sticksstones6  42604  sticksstones7  42605  sticksstones8  42606  sticksstones9  42607  sticksstones10  42608  sticksstones11  42609  sticksstones12a  42610  sticksstones12  42611  sticksstones16  42615  unitscyglem2  42649  unitscyglem4  42651  fzosumm1  42703  fz1sump1  42756  sumcubes  42759  k0004val  44595  binomcxplemnn0  44794  fsumnncl  46020  fsumiunss  46023  fsumsermpt  46027  sumnnodd  46078  dvnmul  46389  dvnprodlem3  46394  itgspltprt  46425  stoweidlem17  46463  stoweidlem20  46466  stirlinglem12  46531  dirkertrigeqlem1  46544  dirkertrigeqlem3  46546  fourierdlem83  46635  fourierdlem112  46664  fourierdlem113  46665  elaa2lem  46679  etransclem32  46712  sge00  46822  sge0iunmptlemre  46861  sge0reuzb  46894  meaiuninclem  46926  carageniuncllem1  46967  hoidmvlelem3  47043  ppivalnn  48107  nnsum3primes4  48276  nnsum3primesprm  48278  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  altgsumbcALT  48841  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109  nn0sumshdiglem2  49110