Theorem sumeq1d 15791

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

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

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-iota 6493  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14070  df-sum 15778

This theorem is used by:  sumeq12dv  15796  sumeq12rdv  15797  fsumf1o  15813  sumss  15814  fsumcllem  15822  fsumsplit1  15835  fsum1  15837  fzosump1  15842  fsump1  15846  fsum2d  15861  fsumcom2  15864  fsumshftm  15871  fsumrev2  15872  telfsumo  15893  telfsum  15895  telfsum2  15896  fsumparts  15897  fsumiun  15912  bcxmas  15928  incexclem  15929  incexc2  15931  isumsplit  15933  isum1p  15934  arisum  15953  arisum2  15954  geoser  15960  pwdif  15961  geolim  15963  geo2sum2  15967  mertenslem1  15977  mertenslem2  15978  mertens  15979  bpolydiflem  16146  efcvgfsum  16178  fprodefsum  16187  eftlub  16203  effsumlt  16205  eirrlem  16298  pwp1fsum  16487  bitsinv1  16538  bitsinvp1  16545  pcfac  16997  prmreclem4  17017  prmreclem6  17019  ovoliunlem1  25736  uniioombllem3  25819  itg11  25925  dvfsumlem1  26260  dvfsumlem4  26263  dvfsum2  26268  elplyr  26433  coeeu  26458  coeeq  26460  plyco  26474  0dgrb  26479  dvply2g  26522  vieta1lem2  26550  vieta1  26551  aaliou3lem5  26590  aaliou3lem6  26591  aaliou3lem7  26592  taylpfval  26608  pserdvlem2  26671  abelthlem6  26679  logfac  26846  advlogexp  26900  emcllem2  27241  emcllem3  27242  emcllem7  27246  harmonicbnd  27248  harmonicbnd2  27249  harmonicbnd3  27252  harmonicbnd4  27255  chtval  27354  chpval  27366  chtfl  27393  chpfl  27394  chtprm  27397  chtnprm  27398  chpp1  27399  chtdif  27402  prmorcht  27422  musum  27435  muinv  27437  logfaclbnd  27466  logfacbnd3  27467  logexprlim  27469  chtppilimlem1  27717  rplogsumlem2  27729  rpvmasumlem  27731  dchrisumlem1  27733  dchrisumlem2  27734  dchrisumlem3  27735  dchrisum  27736  dchrisum0fval  27749  dchrisum0ff  27751  dchrisum0flblem1  27752  dchrisum0lem2  27762  dchrisum0  27764  mulog2sumlem1  27778  2vmadivsumlem  27784  log2sumbnd  27788  logdivbnd  27800  selberg3lem1  27801  pntrsumbnd  27810  pntrsumbnd2  27811  pntrlog2bndlem1  27821  pntrlog2bndlem4  27824  pntpbnd1  27830  pntpbnd2  27831  pntlemf  27849  brcgr  29365  axlowdimlem16  29422  eengv  29444  finsumvtxdg2sstep  30017  eulerpartlemgs2  34899  signsvfn  35098  fsum2dsub  35123  reprval  35126  reprsuc  35131  hashrepr  35141  chpvalz  35144  chtvalz  35145  breprexplema  35146  breprexplemc  35148  breprexp  35149  breprexpnat  35150  vtsval  35153  circlemeth  35156  hgt750lemb  35172  hgt750lema  35173  tgoldbachgtda  35177  tgoldbachgt  35179  subfacval2  35774  subfaclim  35775  bccolsum  36326  sumeq12sdv  36845  knoppndvlem6  37222  mettrifi  38515  rrncmslem  38590  sticksstones6  43025  sticksstones7  43026  sticksstones8  43027  sticksstones9  43028  sticksstones10  43029  sticksstones11  43030  sticksstones12a  43031  sticksstones12  43032  sticksstones16  43036  unitscyglem2  43070  unitscyglem4  43072  fzosumm1  43125  fz1sump1  43193  sumcubes  43196  k0004val  44998  binomcxplemnn0  45181  fsumnncl  46410  fsumiunss  46413  fsumsermpt  46417  sumnnodd  46468  dvnmul  46779  dvnprodlem3  46784  itgspltprt  46815  stoweidlem17  46853  stoweidlem20  46856  stirlinglem12  46921  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  fourierdlem83  47025  fourierdlem112  47054  fourierdlem113  47055  elaa2lem  47069  etransclem32  47102  sge00  47212  sge0iunmptlemre  47251  sge0reuzb  47284  meaiuninclem  47316  carageniuncllem1  47357  hoidmvlelem3  47433  ppivalnn  48543  nnsum3primes4  48712  nnsum3primesprm  48714  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  altgsumbcALT  49291  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559  nn0sumshdiglem2  49560