Theorem sumeq2dv 13282

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 2822	. 2 |- ( ph -> A. k e. A B = C )
3	2	sumeq2d 13281	1 |- ( ph -> sum_ k e. A B = sum_ k e. A C )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   sum_csu 13265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-nn 10424  df-n0 10681  df-z 10748  df-uz 10963  df-fz 11539  df-seq 11908  df-sum 13266

This theorem is referenced by:  sumeq2sdv  13283  2sumeq2dv  13284  sumeq12dv  13285  sumeq12rdv  13286  fsumf1o  13302  fsumss  13304  fsumsplit  13318  isummulc1  13332  isumdivc  13333  isumge0  13335  fsum2dlem  13339  fsumshftm  13350  fsum0diag2  13352  fsummulc1  13354  fsumdivc  13355  fsumneg  13356  fsumsub  13357  fsum2mul  13358  fsumtscopo2  13368  fsumparts  13371  hashiun  13387  ackbijnn  13393  binomlem  13394  binom1p  13396  incexclem  13401  incexc  13402  incexc2  13403  isum1p  13406  arisum  13424  trireciplem  13426  geoserg  13430  geo2sum  13435  mertenslem1  13446  mertenslem2  13447  mertens  13448  efaddlem  13480  rpnnen2lem10  13608  rpnnen2lem11  13609  fsumdvds  13678  pcfac  14063  ramcl  14192  lagsubg2  15844  sylow2a  16222  rrxcph  21012  trirn  21015  rrxmval  21020  rrxmet  21023  ovoliunnul  21106  ovolicc2lem4  21119  uniioombllem4  21182  vitalilem5  21208  itg1addlem4  21293  itg1addlem5  21294  itg1mulc  21298  itg10a  21304  itg1climres  21308  itgss  21405  itgeqa  21407  itgsplit  21429  elply2  21780  elplyd  21786  plyeq0lem  21794  plyaddlem1  21797  plymullem1  21798  coeeulem  21808  coeeq2  21826  coemullem  21833  coe1termlem  21841  plycjlem  21859  plyrecj  21862  dvply1  21866  elqaalem3  21903  aareccl  21908  aannenlem1  21910  taylpval  21948  dvtaylp  21951  pserdvlem2  22009  pserdv2  22011  abelthlem8  22020  abelthlem9  22021  abelth  22022  logtayl  22221  leibpi  22453  birthdaylem2  22462  amgmlem  22499  emcllem5  22509  fsumharmonic  22521  ftalem5  22530  basellem3  22536  basellem8  22541  sgmval2  22597  fsumdvdscom  22641  dvdsflsumcom  22644  musum  22647  musumsum  22648  muinv  22649  fsumdvdsmul  22651  sgmppw  22652  1sgmprm  22654  chtlepsi  22661  pclogsum  22670  vmasum  22671  logfac2  22672  chpval2  22673  chpchtsum  22674  logexprlim  22680  logfacrlim2  22681  perfectlem2  22685  dchrsum2  22723  sumdchr2  22725  dchrhash  22726  dchr2sum  22728  sum2dchr  22729  pcbcctr  22731  bposlem2  22740  lgsquadlem1  22809  lgsquadlem2  22810  chebbnd1lem1  22834  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  dchrvmasum2if  22862  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  dchrisum0flblem1  22873  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrisum0  22885  rplogsum  22892  mudivsum  22895  mulogsumlem  22896  mulogsum  22897  mulog2sumlem1  22899  mulog2sumlem2  22900  mulog2sumlem3  22901  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  logsqvma  22907  logsqvma2  22908  selberglem1  22910  selberglem2  22911  selberg  22913  selberg2  22916  selberg3lem1  22922  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  selbergr  22933  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntsval2  22941  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntpbnd1  22951  pntlemk  22971  pntlemo  22972  axcgrrflx  23295  axcgrid  23297  axsegconlem1  23298  axsegconlem9  23306  ax5seglem1  23309  ax5seglem2  23310  ax5seglem9  23318  axlowdimlem16  23338  axlowdimlem17  23339  ecgrtg  23364  sspival  24271  indsum  26613  eulerpartlemsv1  26873  eulerpartlemsf  26876  eulerpartlemgs2  26897  eulerpartlemn  26898  plymulx0  27082  signsvfn  27117  lgamcvg2  27175  subfaclim  27210  binomfallfaclem2  27677  binomrisefac  27679  bpolylem  28325  bpolydiflem  28331  fsumkthpow  28333  rrnmet  28866  jm2.22  29482  jm2.23  29483  flcidc  29669  phisum  29705  isumneg  29913  stoweidlem37  29970  hashclwwlkn  30648  frghash2spot  30794  usgreghash2spotv  30797  usgreghash2spot  30800  numclwwlk4  30841  numclwwlk6  30844  altgsumbc  30887  altgsumbcALT  30888  fsumshftdOLD  32909