Theorem sumeq1d 15635

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5638  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-seq 13937  df-sum 15622

This theorem is referenced by:  sumeq12dv  15641  sumeq12rdv  15642  fsumf1o  15658  sumss  15659  fsumcllem  15667  fsumsplit1  15680  fsum1  15682  fzosump1  15687  fsump1  15691  fsum2d  15706  fsumcom2  15709  fsumshftm  15716  fsumrev2  15717  telfsumo  15737  telfsum  15739  telfsum2  15740  fsumparts  15741  fsumiun  15756  bcxmas  15770  incexclem  15771  incexc2  15773  isumsplit  15775  isum1p  15776  arisum  15795  arisum2  15796  geoser  15802  pwdif  15803  geolim  15805  geo2sum2  15809  mertenslem1  15819  mertenslem2  15820  mertens  15821  bpolydiflem  15989  efcvgfsum  16021  fprodefsum  16030  eftlub  16046  effsumlt  16048  eirrlem  16141  pwp1fsum  16330  bitsinv1  16381  bitsinvp1  16388  pcfac  16839  prmreclem4  16859  prmreclem6  16861  ovoliunlem1  25471  uniioombllem3  25554  itg11  25660  dvfsumlem1  26000  dvfsumlem4  26004  dvfsum2  26009  elplyr  26174  coeeu  26198  coeeq  26200  plyco  26214  0dgrb  26219  dvply2g  26260  dvply2gOLD  26261  vieta1lem2  26287  vieta1  26288  aaliou3lem5  26323  aaliou3lem6  26324  aaliou3lem7  26325  taylpfval  26340  pserdvlem2  26406  abelthlem6  26414  logfac  26578  advlogexp  26632  emcllem2  26975  emcllem3  26976  emcllem7  26980  harmonicbnd  26982  harmonicbnd2  26983  harmonicbnd3  26986  harmonicbnd4  26989  chtval  27088  chpval  27100  chtfl  27127  chpfl  27128  chtprm  27131  chtnprm  27132  chpp1  27133  chtdif  27136  prmorcht  27156  musum  27169  muinv  27171  logfaclbnd  27201  logfacbnd3  27202  logexprlim  27204  chtppilimlem1  27452  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem2  27469  dchrisumlem3  27470  dchrisum  27471  dchrisum0fval  27484  dchrisum0ff  27486  dchrisum0flblem1  27487  dchrisum0lem2  27497  dchrisum0  27499  mulog2sumlem1  27513  2vmadivsumlem  27519  log2sumbnd  27523  logdivbnd  27535  selberg3lem1  27536  pntrsumbnd  27545  pntrsumbnd2  27546  pntrlog2bndlem1  27556  pntrlog2bndlem4  27559  pntpbnd1  27565  pntpbnd2  27566  pntlemf  27584  brcgr  28985  axlowdimlem16  29042  eengv  29064  finsumvtxdg2sstep  29635  eulerpartlemgs2  34558  signsvfn  34760  fsum2dsub  34785  reprval  34788  reprsuc  34793  hashrepr  34803  chpvalz  34806  chtvalz  34807  breprexplema  34808  breprexplemc  34810  breprexp  34811  breprexpnat  34812  vtsval  34815  circlemeth  34818  hgt750lemb  34834  hgt750lema  34835  tgoldbachgtda  34839  tgoldbachgt  34841  subfacval2  35403  subfaclim  35404  bccolsum  35955  sumeq12sdv  36433  knoppndvlem6  36739  mettrifi  38008  rrncmslem  38083  sticksstones6  42521  sticksstones7  42522  sticksstones8  42523  sticksstones9  42524  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones12  42528  sticksstones16  42532  unitscyglem2  42566  unitscyglem4  42568  fzosumm1  42620  fz1sump1  42680  sumcubes  42683  k0004val  44506  binomcxplemnn0  44705  fsumnncl  45932  fsumiunss  45935  fsumsermpt  45939  sumnnodd  45990  dvnmul  46301  dvnprodlem3  46306  itgspltprt  46337  stoweidlem17  46375  stoweidlem20  46378  stirlinglem12  46443  dirkertrigeqlem1  46456  dirkertrigeqlem3  46458  fourierdlem83  46547  fourierdlem112  46576  fourierdlem113  46577  elaa2lem  46591  etransclem32  46624  sge00  46734  sge0iunmptlemre  46773  sge0reuzb  46806  meaiuninclem  46838  carageniuncllem1  46879  hoidmvlelem3  46955  nnsum3primes4  48148  nnsum3primesprm  48150  nnsum3primesgbe  48152  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  altgsumbcALT  48713  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  nn0sumshdiglem2  48982