Theorem sumeq2dv 13762

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

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1438   e. wcel 1869   sum_csu 13745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-nn 10612  df-n0 10872  df-z 10940  df-uz 11162  df-fz 11787  df-seq 12215  df-sum 13746

This theorem is referenced by:  sumeq2sdv  13763  2sumeq2dv  13764  sumeq12dv  13765  sumeq12rdv  13766  fsumf1o  13782  fsumss  13784  fsumsplit  13799  isummulc1  13817  isumdivc  13818  isumge0  13820  fsum2dlem  13824  fsumshftm  13835  fsum0diag2  13837  fsummulc1  13839  fsumdivc  13840  fsumneg  13841  fsumsub  13842  fsum2mul  13843  telfsumo2  13856  fsumparts  13859  hashiun  13875  ackbijnn  13879  binomlem  13880  binom1p  13882  incexclem  13887  incexc  13888  incexc2  13889  isum1p  13892  arisum  13911  trireciplem  13913  geoserg  13917  geo2sum  13922  mertenslem1  13933  mertenslem2  13934  mertens  13935  binomfallfaclem2  14086  binomrisefac  14088  bpolylem  14094  bpolydiflem  14100  fsumkthpow  14102  efaddlem  14140  rpnnen2lem10  14269  rpnnen2lem11  14270  fsumdvds  14341  pcfac  14837  ramcl  14980  lagsubg2  16871  sylow2a  17264  rrxcph  22343  trirn  22346  rrxmval  22351  rrxmet  22354  ovoliunnul  22452  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  uniioombllem4  22536  vitalilem5  22562  itg1addlem4  22649  itg1addlem5  22650  itg1mulc  22654  itg10a  22660  itg1climres  22664  itgss  22761  itgeqa  22763  itgsplit  22785  elply2  23142  elplyd  23148  plyeq0lem  23156  plyaddlem1  23159  plymullem1  23160  coeeulem  23170  coeeq2  23188  coemullem  23196  coe1termlem  23204  plycjlem  23222  plyrecj  23225  dvply1  23229  elqaalem3  23266  elqaalem3OLD  23269  aareccl  23274  aannenlem1  23276  taylpval  23314  dvtaylp  23317  pserdvlem2  23375  pserdv2  23377  abelthlem8  23386  abelthlem9  23387  abelth  23388  logtayl  23597  leibpi  23860  birthdaylem2  23870  amgmlem  23907  emcllem5  23917  fsumharmonic  23929  lgamcvg2  23972  ftalem5  23993  ftalem5OLD  23995  basellem3  24001  basellem8  24006  sgmval2  24062  fsumdvdscom  24106  dvdsflsumcom  24109  musum  24112  musumsum  24113  muinv  24114  fsumdvdsmul  24116  sgmppw  24117  1sgmprm  24119  chtlepsi  24126  pclogsum  24135  vmasum  24136  logfac2  24137  chpval2  24138  chpchtsum  24139  logexprlim  24145  logfacrlim2  24146  perfectlem2  24150  dchrsum2  24188  sumdchr2  24190  dchrhash  24191  dchr2sum  24193  sum2dchr  24194  pcbcctr  24196  bposlem2  24205  lgsquadlem1  24274  lgsquadlem2  24275  chebbnd1lem1  24299  rplogsumlem1  24314  rplogsumlem2  24315  rpvmasumlem  24317  dchrisumlem1  24319  dchrisumlem2  24320  dchrmusum2  24324  dchrvmasumlem1  24325  dchrvmasum2lem  24326  dchrvmasum2if  24327  dchrvmasumiflem1  24331  dchrvmasumiflem2  24332  dchrisum0flblem1  24338  dchrisum0fno1  24341  rpvmasum2  24342  dchrisum0lem2a  24347  dchrisum0lem2  24348  dchrisum0lem3  24349  dchrisum0  24350  rplogsum  24357  mudivsum  24360  mulogsumlem  24361  mulogsum  24362  mulog2sumlem1  24364  mulog2sumlem2  24365  mulog2sumlem3  24366  vmalogdivsum2  24368  vmalogdivsum  24369  2vmadivsumlem  24370  logsqvma  24372  logsqvma2  24373  selberglem1  24375  selberglem2  24376  selberg  24378  selberg2  24381  selberg3lem1  24387  selberg4lem1  24390  selberg4  24391  pntrsumo1  24395  selbergr  24398  selberg3r  24399  selberg4r  24400  selberg34r  24401  pntsval2  24406  pntrlog2bndlem4  24410  pntrlog2bndlem5  24411  pntpbnd1  24416  pntlemk  24436  pntlemo  24437  axcgrrflx  24936  axcgrid  24938  axsegconlem1  24939  axsegconlem9  24947  ax5seglem1  24950  ax5seglem2  24951  ax5seglem9  24959  axlowdimlem16  24979  axlowdimlem17  24980  ecgrtg  25005  hashclwwlkn  25556  rusgranumwlks  25676  frghash2spot  25783  usgreghash2spotv  25786  usgreghash2spot  25789  numclwwlk4  25830  numclwwlk6  25833  sspival  26369  indsum  28846  eulerpartlemsv1  29191  eulerpartlemsf  29194  eulerpartlemgs2  29215  eulerpartlemn  29216  plymulx0  29438  signsvfn  29473  subfaclim  29913  fwddifnp1  30931  rrnmet  32119  fsumshftdOLD  32487  jm2.22  35814  jm2.23  35815  flcidc  36004  phisum  36040  binomcxplemnn0  36600  binomcxplemdvsum  36606  binomcxplemnotnn0  36607  mccllem  37541  isumneg  37544  sumnnodd  37574  dvnmul  37682  dvnprodlem2  37686  dvnprodlem3  37687  stoweidlem37  37762  dirkertrigeqlem2  37825  dirkertrigeqlem3  37826  fourierdlem81  37915  fourierdlem83  37917  fourierdlem93  37927  fourierdlem103  37937  fourierdlem104  37938  elaa2lem  37961  elaa2lemOLD  37962  etransclem23  37986  etransclem24  37987  etransclem31  37994  etransclem32  37995  etransclem35  37998  etransclem46  38009  sge0z  38049  sge0fsummpt  38064  sge0sup  38065  sge0resplit  38080  sge0split  38083  sge0ltfirpmpt2  38100  omeiunltfirp  38163  carageniuncllem2  38166  perfectALTVlem2  38600  nnsum3primesprm  38641  nnsum3primesgbe  38643  nnsum4primeseven  38651  altgsumbc  39477  altgsumbcALT  39478  nn0sumshdiglemA  39774  nn0sumshdiglemB  39775  nn0sumshdig  39778  aacllem  39884