Theorem sumeq1d 15732

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

Syntax hints:   → wi 4   = wceq 1536  Σcsu 15718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5694  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-iota 6515  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-seq 14039  df-sum 15719

This theorem is referenced by:  sumeq12dv  15738  sumeq12rdv  15739  fsumf1o  15755  sumss  15756  fsumcllem  15764  fsumsplit1  15777  fsum1  15779  fzosump1  15784  fsump1  15788  fsum2d  15803  fsumcom2  15806  fsumshftm  15813  fsumrev2  15814  telfsumo  15834  telfsum  15836  telfsum2  15837  fsumparts  15838  fsumiun  15853  bcxmas  15867  incexclem  15868  incexc2  15870  isumsplit  15872  isum1p  15873  arisum  15892  arisum2  15893  geoser  15899  pwdif  15900  geolim  15902  geo2sum2  15906  mertenslem1  15916  mertenslem2  15917  mertens  15918  bpolydiflem  16086  efcvgfsum  16118  fprodefsum  16127  eftlub  16141  effsumlt  16143  eirrlem  16236  pwp1fsum  16424  bitsinv1  16475  bitsinvp1  16482  pcfac  16932  prmreclem4  16952  prmreclem6  16954  ovoliunlem1  25550  uniioombllem3  25633  itg11  25739  dvfsumlem1  26080  dvfsumlem4  26084  dvfsum2  26089  elplyr  26254  coeeu  26278  coeeq  26280  plyco  26294  0dgrb  26299  dvply2g  26340  dvply2gOLD  26341  vieta1lem2  26367  vieta1  26368  aaliou3lem5  26403  aaliou3lem6  26404  aaliou3lem7  26405  taylpfval  26420  pserdvlem2  26486  abelthlem6  26494  logfac  26657  advlogexp  26711  emcllem2  27054  emcllem3  27055  emcllem7  27059  harmonicbnd  27061  harmonicbnd2  27062  harmonicbnd3  27065  harmonicbnd4  27068  chtval  27167  chpval  27179  chtfl  27206  chpfl  27207  chtprm  27210  chtnprm  27211  chpp1  27212  chtdif  27215  prmorcht  27235  musum  27248  muinv  27250  logfaclbnd  27280  logfacbnd3  27281  logexprlim  27283  chtppilimlem1  27531  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  dchrisum  27550  dchrisum0fval  27563  dchrisum0ff  27565  dchrisum0flblem1  27566  dchrisum0lem2  27576  dchrisum0  27578  mulog2sumlem1  27592  2vmadivsumlem  27598  log2sumbnd  27602  logdivbnd  27614  selberg3lem1  27615  pntrsumbnd  27624  pntrsumbnd2  27625  pntrlog2bndlem1  27635  pntrlog2bndlem4  27638  pntpbnd1  27644  pntpbnd2  27645  pntlemf  27663  brcgr  28929  axlowdimlem16  28986  eengv  29008  finsumvtxdg2sstep  29581  eulerpartlemgs2  34361  signsvfn  34575  fsum2dsub  34600  reprval  34603  reprsuc  34608  hashrepr  34618  chpvalz  34621  chtvalz  34622  breprexplema  34623  breprexplemc  34625  breprexp  34626  breprexpnat  34627  vtsval  34630  circlemeth  34633  hgt750lemb  34649  hgt750lema  34650  tgoldbachgtda  34654  tgoldbachgt  34656  subfacval2  35171  subfaclim  35172  bccolsum  35718  sumeq12sdv  36199  knoppndvlem6  36499  mettrifi  37743  rrncmslem  37818  sticksstones6  42132  sticksstones7  42133  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones16  42143  unitscyglem2  42177  unitscyglem4  42179  fzosumm1  42269  fz1sump1  42322  sumcubes  42325  k0004val  44139  binomcxplemnn0  44344  fsumnncl  45527  fsumiunss  45530  fsumsermpt  45534  sumnnodd  45585  dvnmul  45898  dvnprodlem3  45903  itgspltprt  45934  stoweidlem17  45972  stoweidlem20  45975  stirlinglem12  46040  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  fourierdlem83  46144  fourierdlem112  46173  fourierdlem113  46174  elaa2lem  46188  etransclem32  46221  sge00  46331  sge0iunmptlemre  46370  sge0reuzb  46403  meaiuninclem  46435  carageniuncllem1  46476  hoidmvlelem3  46552  nnsum3primes4  47712  nnsum3primesprm  47714  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  altgsumbcALT  48197  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdiglem2  48471