Theorem sumeq1d 15626

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

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

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-xp 5629  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-iota 6442  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seq 13928  df-sum 15613

This theorem is referenced by:  sumeq12dv  15632  sumeq12rdv  15633  fsumf1o  15649  sumss  15650  fsumcllem  15658  fsumsplit1  15671  fsum1  15673  fzosump1  15678  fsump1  15682  fsum2d  15697  fsumcom2  15700  fsumshftm  15707  fsumrev2  15708  telfsumo  15728  telfsum  15730  telfsum2  15731  fsumparts  15732  fsumiun  15747  bcxmas  15761  incexclem  15762  incexc2  15764  isumsplit  15766  isum1p  15767  arisum  15786  arisum2  15787  geoser  15793  pwdif  15794  geolim  15796  geo2sum2  15800  mertenslem1  15810  mertenslem2  15811  mertens  15812  bpolydiflem  15980  efcvgfsum  16012  fprodefsum  16021  eftlub  16037  effsumlt  16039  eirrlem  16132  pwp1fsum  16321  bitsinv1  16372  bitsinvp1  16379  pcfac  16830  prmreclem4  16850  prmreclem6  16852  ovoliunlem1  25420  uniioombllem3  25503  itg11  25609  dvfsumlem1  25949  dvfsumlem4  25953  dvfsum2  25958  elplyr  26123  coeeu  26147  coeeq  26149  plyco  26163  0dgrb  26168  dvply2g  26209  dvply2gOLD  26210  vieta1lem2  26236  vieta1  26237  aaliou3lem5  26272  aaliou3lem6  26273  aaliou3lem7  26274  taylpfval  26289  pserdvlem2  26355  abelthlem6  26363  logfac  26527  advlogexp  26581  emcllem2  26924  emcllem3  26925  emcllem7  26929  harmonicbnd  26931  harmonicbnd2  26932  harmonicbnd3  26935  harmonicbnd4  26938  chtval  27037  chpval  27049  chtfl  27076  chpfl  27077  chtprm  27080  chtnprm  27081  chpp1  27082  chtdif  27085  prmorcht  27105  musum  27118  muinv  27120  logfaclbnd  27150  logfacbnd3  27151  logexprlim  27153  chtppilimlem1  27401  rplogsumlem2  27413  rpvmasumlem  27415  dchrisumlem1  27417  dchrisumlem2  27418  dchrisumlem3  27419  dchrisum  27420  dchrisum0fval  27433  dchrisum0ff  27435  dchrisum0flblem1  27436  dchrisum0lem2  27446  dchrisum0  27448  mulog2sumlem1  27462  2vmadivsumlem  27468  log2sumbnd  27472  logdivbnd  27484  selberg3lem1  27485  pntrsumbnd  27494  pntrsumbnd2  27495  pntrlog2bndlem1  27505  pntrlog2bndlem4  27508  pntpbnd1  27514  pntpbnd2  27515  pntlemf  27533  brcgr  28864  axlowdimlem16  28921  eengv  28943  finsumvtxdg2sstep  29514  eulerpartlemgs2  34367  signsvfn  34569  fsum2dsub  34594  reprval  34597  reprsuc  34602  hashrepr  34612  chpvalz  34615  chtvalz  34616  breprexplema  34617  breprexplemc  34619  breprexp  34620  breprexpnat  34621  vtsval  34624  circlemeth  34627  hgt750lemb  34643  hgt750lema  34644  tgoldbachgtda  34648  tgoldbachgt  34650  subfacval2  35179  subfaclim  35180  bccolsum  35731  sumeq12sdv  36210  knoppndvlem6  36510  mettrifi  37756  rrncmslem  37831  sticksstones6  42144  sticksstones7  42145  sticksstones8  42146  sticksstones9  42147  sticksstones10  42148  sticksstones11  42149  sticksstones12a  42150  sticksstones12  42151  sticksstones16  42155  unitscyglem2  42189  unitscyglem4  42191  fzosumm1  42243  fz1sump1  42303  sumcubes  42306  k0004val  44143  binomcxplemnn0  44342  fsumnncl  45573  fsumiunss  45576  fsumsermpt  45580  sumnnodd  45631  dvnmul  45944  dvnprodlem3  45949  itgspltprt  45980  stoweidlem17  46018  stoweidlem20  46021  stirlinglem12  46086  dirkertrigeqlem1  46099  dirkertrigeqlem3  46101  fourierdlem83  46190  fourierdlem112  46219  fourierdlem113  46220  elaa2lem  46234  etransclem32  46267  sge00  46377  sge0iunmptlemre  46416  sge0reuzb  46449  meaiuninclem  46481  carageniuncllem1  46522  hoidmvlelem3  46598  nnsum3primes4  47792  nnsum3primesprm  47794  nnsum3primesgbe  47796  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  altgsumbcALT  48357  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625  nn0sumshdiglem1  48626  nn0sumshdiglem2  48627