Theorem sumeq1d 15775

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Σcsu 15761

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-xp 5669  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-iota 6496  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14056  df-sum 15762

This theorem is used by:  sumeq12dv  15780  sumeq12rdv  15781  fsumf1o  15797  sumss  15798  fsumcllem  15806  fsumsplit1  15819  fsum1  15821  fzosump1  15826  fsump1  15830  fsum2d  15845  fsumcom2  15848  fsumshftm  15855  fsumrev2  15856  telfsumo  15877  telfsum  15879  telfsum2  15880  fsumparts  15881  fsumiun  15896  bcxmas  15912  incexclem  15913  incexc2  15915  isumsplit  15917  isum1p  15918  arisum  15937  arisum2  15938  geoser  15944  pwdif  15945  geolim  15947  geo2sum2  15951  mertenslem1  15961  mertenslem2  15962  mertens  15963  bpolydiflem  16130  efcvgfsum  16162  fprodefsum  16171  eftlub  16187  effsumlt  16189  eirrlem  16282  pwp1fsum  16471  bitsinv1  16522  bitsinvp1  16529  pcfac  16981  prmreclem4  17001  prmreclem6  17003  ovoliunlem1  25712  uniioombllem3  25795  itg11  25901  dvfsumlem1  26236  dvfsumlem4  26239  dvfsum2  26244  elplyr  26409  coeeu  26433  coeeq  26435  plyco  26449  0dgrb  26454  dvply2g  26497  vieta1lem2  26523  vieta1  26524  aaliou3lem5  26561  aaliou3lem6  26562  aaliou3lem7  26563  taylpfval  26579  pserdvlem2  26642  abelthlem6  26650  logfac  26817  advlogexp  26871  emcllem2  27212  emcllem3  27213  emcllem7  27217  harmonicbnd  27219  harmonicbnd2  27220  harmonicbnd3  27223  harmonicbnd4  27226  chtval  27325  chpval  27337  chtfl  27364  chpfl  27365  chtprm  27368  chtnprm  27369  chpp1  27370  chtdif  27373  prmorcht  27393  musum  27406  muinv  27408  logfaclbnd  27437  logfacbnd3  27438  logexprlim  27440  chtppilimlem1  27688  rplogsumlem2  27700  rpvmasumlem  27702  dchrisumlem1  27704  dchrisumlem2  27705  dchrisumlem3  27706  dchrisum  27707  dchrisum0fval  27720  dchrisum0ff  27722  dchrisum0flblem1  27723  dchrisum0lem2  27733  dchrisum0  27735  mulog2sumlem1  27749  2vmadivsumlem  27755  log2sumbnd  27759  logdivbnd  27771  selberg3lem1  27772  pntrsumbnd  27781  pntrsumbnd2  27782  pntrlog2bndlem1  27792  pntrlog2bndlem4  27795  pntpbnd1  27801  pntpbnd2  27802  pntlemf  27820  brcgr  29305  axlowdimlem16  29362  eengv  29384  finsumvtxdg2sstep  29957  eulerpartlemgs2  34835  signsvfn  35034  fsum2dsub  35059  reprval  35062  reprsuc  35067  hashrepr  35077  chpvalz  35080  chtvalz  35081  breprexplema  35082  breprexplemc  35084  breprexp  35085  breprexpnat  35086  vtsval  35089  circlemeth  35092  hgt750lemb  35108  hgt750lema  35109  tgoldbachgtda  35113  tgoldbachgt  35115  subfacval2  35716  subfaclim  35717  bccolsum  36268  sumeq12sdv  36786  knoppndvlem6  37163  mettrifi  38466  rrncmslem  38541  sticksstones6  42976  sticksstones7  42977  sticksstones8  42978  sticksstones9  42979  sticksstones10  42980  sticksstones11  42981  sticksstones12a  42982  sticksstones12  42983  sticksstones16  42987  unitscyglem2  43021  unitscyglem4  43023  fzosumm1  43076  fz1sump1  43129  sumcubes  43132  k0004val  44934  binomcxplemnn0  45117  fsumnncl  46346  fsumiunss  46349  fsumsermpt  46353  sumnnodd  46404  dvnmul  46715  dvnprodlem3  46720  itgspltprt  46751  stoweidlem17  46789  stoweidlem20  46792  stirlinglem12  46857  dirkertrigeqlem1  46870  dirkertrigeqlem3  46872  fourierdlem83  46961  fourierdlem112  46990  fourierdlem113  46991  elaa2lem  47005  etransclem32  47038  sge00  47148  sge0iunmptlemre  47187  sge0reuzb  47220  meaiuninclem  47252  carageniuncllem1  47293  hoidmvlelem3  47369  ppivalnn  48442  nnsum3primes4  48611  nnsum3primesprm  48613  nnsum3primesgbe  48615  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  altgsumbcALT  49190  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  nn0sumshdiglem1  49458  nn0sumshdiglem2  49459