Theorem sumeq1d 15602

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

Syntax hints:   → wi 4   = wceq 1541  Σcsu 15588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-xp 5617  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-iota 6432  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-oprab 7345  df-mpo 7346  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-seq 13904  df-sum 15589

This theorem is referenced by:  sumeq12dv  15608  sumeq12rdv  15609  fsumf1o  15625  sumss  15626  fsumcllem  15634  fsumsplit1  15647  fsum1  15649  fzosump1  15654  fsump1  15658  fsum2d  15673  fsumcom2  15676  fsumshftm  15683  fsumrev2  15684  telfsumo  15704  telfsum  15706  telfsum2  15707  fsumparts  15708  fsumiun  15723  bcxmas  15737  incexclem  15738  incexc2  15740  isumsplit  15742  isum1p  15743  arisum  15762  arisum2  15763  geoser  15769  pwdif  15770  geolim  15772  geo2sum2  15776  mertenslem1  15786  mertenslem2  15787  mertens  15788  bpolydiflem  15956  efcvgfsum  15988  fprodefsum  15997  eftlub  16013  effsumlt  16015  eirrlem  16108  pwp1fsum  16297  bitsinv1  16348  bitsinvp1  16355  pcfac  16806  prmreclem4  16826  prmreclem6  16828  ovoliunlem1  25425  uniioombllem3  25508  itg11  25614  dvfsumlem1  25954  dvfsumlem4  25958  dvfsum2  25963  elplyr  26128  coeeu  26152  coeeq  26154  plyco  26168  0dgrb  26173  dvply2g  26214  dvply2gOLD  26215  vieta1lem2  26241  vieta1  26242  aaliou3lem5  26277  aaliou3lem6  26278  aaliou3lem7  26279  taylpfval  26294  pserdvlem2  26360  abelthlem6  26368  logfac  26532  advlogexp  26586  emcllem2  26929  emcllem3  26930  emcllem7  26934  harmonicbnd  26936  harmonicbnd2  26937  harmonicbnd3  26940  harmonicbnd4  26943  chtval  27042  chpval  27054  chtfl  27081  chpfl  27082  chtprm  27085  chtnprm  27086  chpp1  27087  chtdif  27090  prmorcht  27110  musum  27123  muinv  27125  logfaclbnd  27155  logfacbnd3  27156  logexprlim  27158  chtppilimlem1  27406  rplogsumlem2  27418  rpvmasumlem  27420  dchrisumlem1  27422  dchrisumlem2  27423  dchrisumlem3  27424  dchrisum  27425  dchrisum0fval  27438  dchrisum0ff  27440  dchrisum0flblem1  27441  dchrisum0lem2  27451  dchrisum0  27453  mulog2sumlem1  27467  2vmadivsumlem  27473  log2sumbnd  27477  logdivbnd  27489  selberg3lem1  27490  pntrsumbnd  27499  pntrsumbnd2  27500  pntrlog2bndlem1  27510  pntrlog2bndlem4  27513  pntpbnd1  27519  pntpbnd2  27520  pntlemf  27538  brcgr  28873  axlowdimlem16  28930  eengv  28952  finsumvtxdg2sstep  29523  eulerpartlemgs2  34385  signsvfn  34587  fsum2dsub  34612  reprval  34615  reprsuc  34620  hashrepr  34630  chpvalz  34633  chtvalz  34634  breprexplema  34635  breprexplemc  34637  breprexp  34638  breprexpnat  34639  vtsval  34642  circlemeth  34645  hgt750lemb  34661  hgt750lema  34662  tgoldbachgtda  34666  tgoldbachgt  34668  subfacval2  35223  subfaclim  35224  bccolsum  35775  sumeq12sdv  36251  knoppndvlem6  36551  mettrifi  37797  rrncmslem  37872  sticksstones6  42184  sticksstones7  42185  sticksstones8  42186  sticksstones9  42187  sticksstones10  42188  sticksstones11  42189  sticksstones12a  42190  sticksstones12  42191  sticksstones16  42195  unitscyglem2  42229  unitscyglem4  42231  fzosumm1  42283  fz1sump1  42343  sumcubes  42346  k0004val  44183  binomcxplemnn0  44382  fsumnncl  45612  fsumiunss  45615  fsumsermpt  45619  sumnnodd  45670  dvnmul  45981  dvnprodlem3  45986  itgspltprt  46017  stoweidlem17  46055  stoweidlem20  46058  stirlinglem12  46123  dirkertrigeqlem1  46136  dirkertrigeqlem3  46138  fourierdlem83  46227  fourierdlem112  46256  fourierdlem113  46257  elaa2lem  46271  etransclem32  46304  sge00  46414  sge0iunmptlemre  46453  sge0reuzb  46486  meaiuninclem  46518  carageniuncllem1  46559  hoidmvlelem3  46635  nnsum3primes4  47819  nnsum3primesprm  47821  nnsum3primesgbe  47823  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  altgsumbcALT  48384  nn0sumshdiglemA  48651  nn0sumshdiglemB  48652  nn0sumshdiglem1  48653  nn0sumshdiglem2  48654