Theorem sumeq2dv 13817

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)

Hypothesis

Ref	Expression
sumeq2dv.1	|- ( ( ph /\ k e. A ) -> B = C )

Assertion

Ref	Expression
sumeq2dv	|- ( ph -> sum_ k e. A B = sum_ k e. A C )

Distinct variable groups:   A, k   ph, k

Allowed substitution hints:   B( k)   C( k)

Proof of Theorem sumeq2dv

Step	Hyp	Ref	Expression
1		sumeq2dv.1	. . 3 |- ( ( ph /\ k e. A ) -> B = C )
2	1	ralrimiva 2813	. 2 |- ( ph -> A. k e. A B = C )
3	2	sumeq2d 13816	1 |- ( ph -> sum_ k e. A B = sum_ k e. A C )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897   sum_csu 13800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-n0 10898  df-z 10966  df-uz 11188  df-fz 11813  df-seq 12245  df-sum 13801

This theorem is referenced by:  sumeq2sdv  13818  2sumeq2dv  13819  sumeq12dv  13820  sumeq12rdv  13821  fsumf1o  13837  fsumss  13839  fsumsplit  13854  isummulc1  13872  isumdivc  13873  isumge0  13875  fsum2dlem  13879  fsumshftm  13890  fsum0diag2  13892  fsummulc1  13894  fsumdivc  13895  fsumneg  13896  fsumsub  13897  fsum2mul  13898  telfsumo2  13911  fsumparts  13914  hashiun  13930  ackbijnn  13934  binomlem  13935  binom1p  13937  incexclem  13942  incexc  13943  incexc2  13944  isum1p  13947  arisum  13966  trireciplem  13968  geoserg  13972  geo2sum  13977  mertenslem1  13988  mertenslem2  13989  mertens  13990  binomfallfaclem2  14141  binomrisefac  14143  bpolylem  14149  bpolydiflem  14155  fsumkthpow  14157  efaddlem  14195  rpnnen2lem10  14324  rpnnen2lem11  14325  fsumdvds  14396  pcfac  14892  ramcl  15035  lagsubg2  16926  sylow2a  17319  rrxcph  22399  trirn  22402  rrxmval  22407  rrxmet  22410  ovoliunnul  22508  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  uniioombllem4  22592  vitalilem5  22618  itg1addlem4  22705  itg1addlem5  22706  itg1mulc  22710  itg10a  22716  itg1climres  22720  itgss  22817  itgeqa  22819  itgsplit  22841  elply2  23198  elplyd  23204  plyeq0lem  23212  plyaddlem1  23215  plymullem1  23216  coeeulem  23226  coeeq2  23244  coemullem  23252  coe1termlem  23260  plycjlem  23278  plyrecj  23281  dvply1  23285  elqaalem3  23322  elqaalem3OLD  23325  aareccl  23330  aannenlem1  23332  taylpval  23370  dvtaylp  23373  pserdvlem2  23431  pserdv2  23433  abelthlem8  23442  abelthlem9  23443  abelth  23444  logtayl  23653  leibpi  23916  birthdaylem2  23926  amgmlem  23963  emcllem5  23973  fsumharmonic  23985  lgamcvg2  24028  ftalem5  24049  ftalem5OLD  24051  basellem3  24057  basellem8  24062  sgmval2  24118  fsumdvdscom  24162  dvdsflsumcom  24165  musum  24168  musumsum  24169  muinv  24170  fsumdvdsmul  24172  sgmppw  24173  1sgmprm  24175  chtlepsi  24182  pclogsum  24191  vmasum  24192  logfac2  24193  chpval2  24194  chpchtsum  24195  logexprlim  24201  logfacrlim2  24202  perfectlem2  24206  dchrsum2  24244  sumdchr2  24246  dchrhash  24247  dchr2sum  24249  sum2dchr  24250  pcbcctr  24252  bposlem2  24261  lgsquadlem1  24330  lgsquadlem2  24331  chebbnd1lem1  24355  rplogsumlem1  24370  rplogsumlem2  24371  rpvmasumlem  24373  dchrisumlem1  24375  dchrisumlem2  24376  dchrmusum2  24380  dchrvmasumlem1  24381  dchrvmasum2lem  24382  dchrvmasum2if  24383  dchrvmasumiflem1  24387  dchrvmasumiflem2  24388  dchrisum0flblem1  24394  dchrisum0fno1  24397  rpvmasum2  24398  dchrisum0lem2a  24403  dchrisum0lem2  24404  dchrisum0lem3  24405  dchrisum0  24406  rplogsum  24413  mudivsum  24416  mulogsumlem  24417  mulogsum  24418  mulog2sumlem1  24420  mulog2sumlem2  24421  mulog2sumlem3  24422  vmalogdivsum2  24424  vmalogdivsum  24425  2vmadivsumlem  24426  logsqvma  24428  logsqvma2  24429  selberglem1  24431  selberglem2  24432  selberg  24434  selberg2  24437  selberg3lem1  24443  selberg4lem1  24446  selberg4  24447  pntrsumo1  24451  selbergr  24454  selberg3r  24455  selberg4r  24456  selberg34r  24457  pntsval2  24462  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  pntpbnd1  24472  pntlemk  24492  pntlemo  24493  axcgrrflx  24992  axcgrid  24994  axsegconlem1  24995  axsegconlem9  25003  ax5seglem1  25006  ax5seglem2  25007  ax5seglem9  25015  axlowdimlem16  25035  axlowdimlem17  25036  ecgrtg  25061  hashclwwlkn  25612  rusgranumwlks  25732  frghash2spot  25839  usgreghash2spotv  25842  usgreghash2spot  25845  numclwwlk4  25886  numclwwlk6  25889  sspival  26425  indsum  28892  eulerpartlemsv1  29237  eulerpartlemsf  29240  eulerpartlemgs2  29261  eulerpartlemn  29262  plymulx0  29484  signsvfn  29519  subfaclim  29959  fwddifnp1  30980  rrnmet  32205  fsumshftdOLD  32568  jm2.22  35894  jm2.23  35895  flcidc  36084  phisum  36120  binomcxplemnn0  36741  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  mccllem  37714  isumneg  37717  sumnnodd  37747  dvnmul  37855  dvnprodlem2  37859  dvnprodlem3  37860  stoweidlem37  37935  dirkertrigeqlem2  37998  dirkertrigeqlem3  37999  fourierdlem81  38088  fourierdlem83  38090  fourierdlem93  38100  fourierdlem103  38110  fourierdlem104  38111  elaa2lem  38134  elaa2lemOLD  38135  etransclem23  38159  etransclem24  38160  etransclem31  38167  etransclem32  38168  etransclem35  38171  etransclem46  38182  rrxtopnfi  38192  rrndistlt  38196  sge0z  38254  sge0fsummpt  38269  sge0sup  38270  sge0resplit  38285  sge0split  38288  sge0ltfirpmpt2  38305  omeiunltfirp  38377  carageniuncllem2  38380  hoidmvlelem2  38455  hoidmvlelem3  38456  perfectALTVlem2  38881  nnsum3primesprm  38922  nnsum3primesgbe  38924  nnsum4primeseven  38932  altgsumbc  40405  altgsumbcALT  40406  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703  nn0sumshdig  40706  aacllem  40812