Theorem sumeq1d 15653

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

Syntax hints:   → wi 4   = wceq 1547  Σcsu 15639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-xp 5624  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-iota 6441  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seq 13955  df-sum 15640

This theorem is referenced by:  sumeq12dv  15659  sumeq12rdv  15660  fsumf1o  15676  sumss  15677  fsumcllem  15685  fsumsplit1  15698  fsum1  15700  fzosump1  15705  fsump1  15709  fsum2d  15724  fsumcom2  15727  fsumshftm  15734  fsumrev2  15735  telfsumo  15756  telfsum  15758  telfsum2  15759  fsumparts  15760  fsumiun  15775  bcxmas  15791  incexclem  15792  incexc2  15794  isumsplit  15796  isum1p  15797  arisum  15816  arisum2  15817  geoser  15823  pwdif  15824  geolim  15826  geo2sum2  15830  mertenslem1  15840  mertenslem2  15841  mertens  15842  bpolydiflem  16010  efcvgfsum  16042  fprodefsum  16051  eftlub  16067  effsumlt  16069  eirrlem  16162  pwp1fsum  16351  bitsinv1  16402  bitsinvp1  16409  pcfac  16861  prmreclem4  16881  prmreclem6  16883  ovoliunlem1  25487  uniioombllem3  25570  itg11  25676  dvfsumlem1  26011  dvfsumlem4  26014  dvfsum2  26019  elplyr  26184  coeeu  26208  coeeq  26210  plyco  26224  0dgrb  26229  dvply2g  26269  vieta1lem2  26295  vieta1  26296  aaliou3lem5  26331  aaliou3lem6  26332  aaliou3lem7  26333  taylpfval  26348  pserdvlem2  26411  abelthlem6  26419  logfac  26583  advlogexp  26637  emcllem2  26978  emcllem3  26979  emcllem7  26983  harmonicbnd  26985  harmonicbnd2  26986  harmonicbnd3  26989  harmonicbnd4  26992  chtval  27091  chpval  27103  chtfl  27130  chpfl  27131  chtprm  27134  chtnprm  27135  chpp1  27136  chtdif  27139  prmorcht  27159  musum  27172  muinv  27174  logfaclbnd  27203  logfacbnd3  27204  logexprlim  27206  chtppilimlem1  27454  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrisumlem3  27472  dchrisum  27473  dchrisum0fval  27486  dchrisum0ff  27488  dchrisum0flblem1  27489  dchrisum0lem2  27499  dchrisum0  27501  mulog2sumlem1  27515  2vmadivsumlem  27521  log2sumbnd  27525  logdivbnd  27537  selberg3lem1  27538  pntrsumbnd  27547  pntrsumbnd2  27548  pntrlog2bndlem1  27558  pntrlog2bndlem4  27561  pntpbnd1  27567  pntpbnd2  27568  pntlemf  27586  brcgr  28987  axlowdimlem16  29044  eengv  29066  finsumvtxdg2sstep  29636  eulerpartlemgs2  34564  signsvfn  34766  fsum2dsub  34791  reprval  34794  reprsuc  34799  hashrepr  34809  chpvalz  34812  chtvalz  34813  breprexplema  34814  breprexplemc  34816  breprexp  34817  breprexpnat  34818  vtsval  34821  circlemeth  34824  hgt750lemb  34840  hgt750lema  34841  tgoldbachgtda  34845  tgoldbachgt  34847  subfacval2  35415  subfaclim  35416  bccolsum  35967  sumeq12sdv  36445  knoppndvlem6  36823  mettrifi  38124  rrncmslem  38199  sticksstones6  42636  sticksstones7  42637  sticksstones8  42638  sticksstones9  42639  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones16  42647  unitscyglem2  42681  unitscyglem4  42683  fzosumm1  42734  fz1sump1  42787  sumcubes  42790  k0004val  44594  binomcxplemnn0  44793  fsumnncl  46017  fsumiunss  46020  fsumsermpt  46024  sumnnodd  46075  dvnmul  46386  dvnprodlem3  46391  itgspltprt  46422  stoweidlem17  46460  stoweidlem20  46463  stirlinglem12  46528  dirkertrigeqlem1  46541  dirkertrigeqlem3  46543  fourierdlem83  46632  fourierdlem112  46661  fourierdlem113  46662  elaa2lem  46676  etransclem32  46709  sge00  46819  sge0iunmptlemre  46858  sge0reuzb  46891  meaiuninclem  46923  carageniuncllem1  46964  hoidmvlelem3  47040  ppivalnn  48110  nnsum3primes4  48279  nnsum3primesprm  48281  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  altgsumbcALT  48844  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  nn0sumshdiglem2  49113