Theorem sumeq1d 15747

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

Syntax hints:   → wi 4   = wceq 1567  Σcsu 15733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-iota 6490  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-oprab 7412  df-mpo 7413  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-seq 14034  df-sum 15734

This theorem is referenced by:  sumeq12dv  15753  sumeq12rdv  15754  fsumf1o  15770  sumss  15771  fsumcllem  15779  fsumsplit1  15792  fsum1  15794  fzosump1  15799  fsump1  15803  fsum2d  15818  fsumcom2  15821  fsumshftm  15828  fsumrev2  15829  telfsumo  15850  telfsum  15852  telfsum2  15853  fsumparts  15854  fsumiun  15869  bcxmas  15885  incexclem  15886  incexc2  15888  isumsplit  15890  isum1p  15891  arisum  15910  arisum2  15911  geoser  15917  pwdif  15918  geolim  15920  geo2sum2  15924  mertenslem1  15934  mertenslem2  15935  mertens  15936  bpolydiflem  16104  efcvgfsum  16136  fprodefsum  16145  eftlub  16161  effsumlt  16163  eirrlem  16256  pwp1fsum  16445  bitsinv1  16496  bitsinvp1  16503  pcfac  16955  prmreclem4  16975  prmreclem6  16977  ovoliunlem1  25626  uniioombllem3  25709  itg11  25815  dvfsumlem1  26150  dvfsumlem4  26153  dvfsum2  26158  elplyr  26323  coeeu  26347  coeeq  26349  plyco  26363  0dgrb  26368  dvply2g  26411  vieta1lem2  26437  vieta1  26438  aaliou3lem5  26473  aaliou3lem6  26474  aaliou3lem7  26475  taylpfval  26490  pserdvlem2  26553  abelthlem6  26561  logfac  26728  advlogexp  26782  emcllem2  27123  emcllem3  27124  emcllem7  27128  harmonicbnd  27130  harmonicbnd2  27131  harmonicbnd3  27134  harmonicbnd4  27137  chtval  27236  chpval  27248  chtfl  27275  chpfl  27276  chtprm  27279  chtnprm  27280  chpp1  27281  chtdif  27284  prmorcht  27304  musum  27317  muinv  27319  logfaclbnd  27348  logfacbnd3  27349  logexprlim  27351  chtppilimlem1  27599  rplogsumlem2  27611  rpvmasumlem  27613  dchrisumlem1  27615  dchrisumlem2  27616  dchrisumlem3  27617  dchrisum  27618  dchrisum0fval  27631  dchrisum0ff  27633  dchrisum0flblem1  27634  dchrisum0lem2  27644  dchrisum0  27646  mulog2sumlem1  27660  2vmadivsumlem  27666  log2sumbnd  27670  logdivbnd  27682  selberg3lem1  27683  pntrsumbnd  27692  pntrsumbnd2  27693  pntrlog2bndlem1  27703  pntrlog2bndlem4  27706  pntpbnd1  27712  pntpbnd2  27713  pntlemf  27731  brcgr  29187  axlowdimlem16  29244  eengv  29266  finsumvtxdg2sstep  29836  eulerpartlemgs2  34711  signsvfn  34910  fsum2dsub  34935  reprval  34938  reprsuc  34943  hashrepr  34953  chpvalz  34956  chtvalz  34957  breprexplema  34958  breprexplemc  34960  breprexp  34961  breprexpnat  34962  vtsval  34965  circlemeth  34968  hgt750lemb  34984  hgt750lema  34985  tgoldbachgtda  34989  tgoldbachgt  34991  subfacval2  35574  subfaclim  35575  bccolsum  36126  sumeq12sdv  36614  knoppndvlem6  36991  mettrifi  38291  rrncmslem  38366  sticksstones6  42803  sticksstones7  42804  sticksstones8  42805  sticksstones9  42806  sticksstones10  42807  sticksstones11  42808  sticksstones12a  42809  sticksstones12  42810  sticksstones16  42814  unitscyglem2  42848  unitscyglem4  42850  fzosumm1  42903  fz1sump1  42956  sumcubes  42959  k0004val  44763  binomcxplemnn0  44946  fsumnncl  46175  fsumiunss  46178  fsumsermpt  46182  sumnnodd  46233  dvnmul  46544  dvnprodlem3  46549  itgspltprt  46580  stoweidlem17  46618  stoweidlem20  46621  stirlinglem12  46686  dirkertrigeqlem1  46699  dirkertrigeqlem3  46701  fourierdlem83  46790  fourierdlem112  46819  fourierdlem113  46820  elaa2lem  46834  etransclem32  46867  sge00  46977  sge0iunmptlemre  47016  sge0reuzb  47049  meaiuninclem  47081  carageniuncllem1  47122  hoidmvlelem3  47198  ppivalnn  48268  nnsum3primes4  48437  nnsum3primesprm  48439  nnsum3primesgbe  48441  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  wtgoldbnnsum4prm  48451  bgoldbnnsum3prm  48453  altgsumbcALT  49013  nn0sumshdiglemA  49279  nn0sumshdiglemB  49280  nn0sumshdiglem1  49281  nn0sumshdiglem2  49282