Theorem sumeq1d 15911

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-xp 5664  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-iota 6520  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-seq 14185  df-sum 15898

This theorem is used by:  sumeq12dv  15916  sumeq12rdv  15917  fsumf1o  15933  sumss  15934  fsumcllem  15942  fsumsplit1  15955  fsum1  15957  fzosump1  15962  fsump1  15966  fsum2d  15981  fsumcom2  15984  fsumshftm  15991  fsumrev2  15992  telfsumo  16013  telfsum  16015  telfsum2  16016  fsumparts  16017  fsumiun  16032  bcxmas  16048  incexclem  16049  incexc2  16051  isumsplit  16053  isum1p  16054  arisum  16073  arisum2  16074  geoser  16080  pwdif  16081  geolim  16083  geo2sum2  16087  mertenslem1  16097  mertenslem2  16098  mertens  16099  bpolydiflem  16264  efcvgfsum  16296  fprodefsum  16305  eftlub  16321  effsumlt  16323  eirrlem  16416  pwp1fsum  16605  bitsinv1  16656  bitsinvp1  16663  pcfac  17121  prmreclem4  17141  prmreclem6  17143  ovoliunlem1  25878  uniioombllem3  25961  itg11  26067  dvfsumlem1  26401  dvfsumlem4  26404  dvfsum2  26409  elplyr  26574  coeeu  26599  coeeq  26601  plyco  26615  0dgrb  26620  dvply2g  26661  vieta1lem2  26689  vieta1  26690  aaliou3lem5  26731  aaliou3lem6  26732  aaliou3lem7  26733  taylpfval  26749  pserdvlem2  26812  abelthlem6  26820  logfac  26986  advlogexp  27040  emcllem2  27381  emcllem3  27382  emcllem7  27386  harmonicbnd  27388  harmonicbnd2  27389  harmonicbnd3  27392  harmonicbnd4  27395  chtval  27494  chpval  27506  chtfl  27533  chpfl  27534  chtprm  27537  chtnprm  27538  chpp1  27539  chtdif  27542  prmorcht  27562  musum  27575  muinv  27577  logfaclbnd  27606  logfacbnd3  27607  logexprlim  27609  chtppilimlem1  27857  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlem1  27873  dchrisumlem2  27874  dchrisumlem3  27875  dchrisum  27876  dchrisum0fval  27889  dchrisum0ff  27891  dchrisum0flblem1  27892  dchrisum0lem2  27902  dchrisum0  27904  mulog2sumlem1  27918  2vmadivsumlem  27924  log2sumbnd  27928  logdivbnd  27940  selberg3lem1  27941  pntrsumbnd  27950  pntrsumbnd2  27951  pntrlog2bndlem1  27961  pntrlog2bndlem4  27964  pntpbnd1  27970  pntpbnd2  27971  pntlemf  27989  brcgr  29535  axlowdimlem16  29592  eengv  29614  finsumvtxdg2sstep  30187  eulerpartlemgs2  35123  signsvfn  35322  fsum2dsub  35347  reprval  35350  reprsuc  35355  hashrepr  35365  chpvalz  35368  chtvalz  35369  breprexplema  35370  breprexplemc  35372  breprexp  35373  breprexpnat  35374  vtsval  35377  circlemeth  35380  hgt750lemb  35396  hgt750lema  35397  tgoldbachgtda  35401  tgoldbachgt  35403  subfacval2  36160  subfaclim  36161  bccolsum  36719  sumeq12sdv  37221  knoppndvlem6  37598  mettrifi  38957  rrncmslem  39032  sticksstones6  43467  sticksstones7  43468  sticksstones8  43469  sticksstones9  43470  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones12  43474  sticksstones16  43478  unitscyglem2  43512  unitscyglem4  43514  fzosumm1  43567  fz1sump1  43633  sumcubes  43636  k0004val  45411  binomcxplemnn0  45594  fsumnncl  46857  fsumiunss  46860  fsumsermpt  46864  sumnnodd  46915  dvnmul  47226  dvnprodlem3  47231  itgspltprt  47262  stoweidlem17  47300  stoweidlem20  47303  stirlinglem12  47368  dirkertrigeqlem1  47381  dirkertrigeqlem3  47383  fourierdlem83  47472  fourierdlem112  47501  fourierdlem113  47502  elaa2lem  47516  etransclem32  47549  sge00  47659  sge0iunmptlemre  47698  sge0reuzb  47731  meaiuninclem  47763  carageniuncllem1  47804  hoidmvlelem3  47880  ppivalnn  48990  nnsum3primes4  49159  nnsum3primesprm  49161  nnsum3primesgbe  49163  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  linply  49713  altgsumbcALT  49796  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdiglem1  50064  nn0sumshdiglem2  50065