Theorem sumeq1d 15874

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Σcsu 15860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-xp 5656  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6306  df-iota 6496  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7425  df-oprab 7426  df-mpo 7427  df-frecs 8304  df-wrecs 8335  df-recs 8384  df-rdg 8423  df-seq 14150  df-sum 15861

This theorem is used by:  sumeq12dv  15879  sumeq12rdv  15880  fsumf1o  15896  sumss  15897  fsumcllem  15905  fsumsplit1  15918  fsum1  15920  fzosump1  15925  fsump1  15929  fsum2d  15944  fsumcom2  15947  fsumshftm  15954  fsumrev2  15955  telfsumo  15976  telfsum  15978  telfsum2  15979  fsumparts  15980  fsumiun  15995  bcxmas  16011  incexclem  16012  incexc2  16014  isumsplit  16016  isum1p  16017  arisum  16036  arisum2  16037  geoser  16043  pwdif  16044  geolim  16046  geo2sum2  16050  mertenslem1  16060  mertenslem2  16061  mertens  16062  bpolydiflem  16227  efcvgfsum  16259  fprodefsum  16268  eftlub  16284  effsumlt  16286  eirrlem  16379  pwp1fsum  16568  bitsinv1  16619  bitsinvp1  16626  pcfac  17084  prmreclem4  17104  prmreclem6  17106  ovoliunlem1  25830  uniioombllem3  25913  itg11  26019  dvfsumlem1  26353  dvfsumlem4  26356  dvfsum2  26361  elplyr  26526  coeeu  26551  coeeq  26553  plyco  26567  0dgrb  26572  dvply2g  26613  vieta1lem2  26641  vieta1  26642  aaliou3lem5  26681  aaliou3lem6  26682  aaliou3lem7  26683  taylpfval  26699  pserdvlem2  26762  abelthlem6  26770  logfac  26936  advlogexp  26990  emcllem2  27331  emcllem3  27332  emcllem7  27336  harmonicbnd  27338  harmonicbnd2  27339  harmonicbnd3  27342  harmonicbnd4  27345  chtval  27444  chpval  27456  chtfl  27483  chpfl  27484  chtprm  27487  chtnprm  27488  chpp1  27489  chtdif  27492  prmorcht  27512  musum  27525  muinv  27527  logfaclbnd  27556  logfacbnd3  27557  logexprlim  27559  chtppilimlem1  27807  rplogsumlem2  27819  rpvmasumlem  27821  dchrisumlem1  27823  dchrisumlem2  27824  dchrisumlem3  27825  dchrisum  27826  dchrisum0fval  27839  dchrisum0ff  27841  dchrisum0flblem1  27842  dchrisum0lem2  27852  dchrisum0  27854  mulog2sumlem1  27868  2vmadivsumlem  27874  log2sumbnd  27878  logdivbnd  27890  selberg3lem1  27891  pntrsumbnd  27900  pntrsumbnd2  27901  pntrlog2bndlem1  27911  pntrlog2bndlem4  27914  pntpbnd1  27920  pntpbnd2  27921  pntlemf  27939  brcgr  29485  axlowdimlem16  29542  eengv  29564  finsumvtxdg2sstep  30137  eulerpartlemgs2  35060  signsvfn  35259  fsum2dsub  35284  reprval  35287  reprsuc  35292  hashrepr  35302  chpvalz  35305  chtvalz  35306  breprexplema  35307  breprexplemc  35309  breprexp  35310  breprexpnat  35311  vtsval  35314  circlemeth  35317  hgt750lemb  35333  hgt750lema  35334  tgoldbachgtda  35338  tgoldbachgt  35340  subfacval2  36040  subfaclim  36041  bccolsum  36598  sumeq12sdv  37100  knoppndvlem6  37477  mettrifi  38798  rrncmslem  38873  sticksstones6  43308  sticksstones7  43309  sticksstones8  43310  sticksstones9  43311  sticksstones10  43312  sticksstones11  43313  sticksstones12a  43314  sticksstones12  43315  sticksstones16  43319  unitscyglem2  43353  unitscyglem4  43355  fzosumm1  43408  fz1sump1  43474  sumcubes  43477  k0004val  45257  binomcxplemnn0  45440  fsumnncl  46691  fsumiunss  46694  fsumsermpt  46698  sumnnodd  46749  dvnmul  47060  dvnprodlem3  47065  itgspltprt  47096  stoweidlem17  47134  stoweidlem20  47137  stirlinglem12  47202  dirkertrigeqlem1  47215  dirkertrigeqlem3  47217  fourierdlem83  47306  fourierdlem112  47335  fourierdlem113  47336  elaa2lem  47350  etransclem32  47383  sge00  47493  sge0iunmptlemre  47532  sge0reuzb  47565  meaiuninclem  47597  carageniuncllem1  47638  hoidmvlelem3  47714  ppivalnn  48824  nnsum3primes4  48993  nnsum3primesprm  48995  nnsum3primesgbe  48997  nnsum4primesodd  49001  nnsum4primesoddALTV  49002  wtgoldbnnsum4prm  49007  bgoldbnnsum3prm  49009  altgsumbcALT  49572  nn0sumshdiglemA  49838  nn0sumshdiglemB  49839  nn0sumshdiglem1  49840  nn0sumshdiglem2  49841