Theorem sumeq2dv 14433

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-seq 12802  df-sum 14417

This theorem is referenced by:  sumeq2sdv  14435  2sumeq2dv  14436  sumeq12dv  14437  sumeq12rdv  14438  fsumf1o  14454  fsumss  14456  fsumsplit  14471  isummulc1  14494  isumdivc  14495  isumge0  14497  fsum2dlem  14501  fsumshftm  14513  fsum0diag2  14515  fsummulc1  14517  fsumdivc  14518  fsumneg  14519  fsumsub  14520  fsum2mul  14521  telfsumo2  14535  fsumparts  14538  hashiun  14554  hash2iun  14555  hash2iun1dif1  14556  ackbijnn  14560  binomlem  14561  binom1p  14563  incexclem  14568  incexc  14569  incexc2  14570  isum1p  14573  arisum  14592  trireciplem  14594  geoserg  14598  geo2sum  14604  mertenslem1  14616  mertenslem2  14617  mertens  14618  binomfallfaclem2  14771  binomrisefac  14773  bpolylem  14779  bpolydiflem  14785  fsumkthpow  14787  efaddlem  14823  rpnnen2lem10  14952  rpnnen2lem11  14953  fsumdvds  15030  pwp1fsum  15114  phisum  15495  pcfac  15603  ramcl  15733  lagsubg2  17655  sylow2a  18034  rrxcph  23180  trirn  23183  rrxmval  23188  rrxmet  23191  ovoliunnul  23275  ovolicc2lem4  23288  uniioombllem4  23354  vitalilem5  23381  itg1addlem4  23466  itg1addlem5  23467  itg1mulc  23471  itg10a  23477  itg1climres  23481  itgss  23578  itgeqa  23580  itgsplit  23602  elply2  23952  elplyd  23958  plyeq0lem  23966  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeeq2  23998  coemullem  24006  coe1termlem  24014  plycjlem  24032  plyrecj  24035  dvply1  24039  elqaalem3  24076  aareccl  24081  aannenlem1  24083  taylpval  24121  dvtaylp  24124  pserdvlem2  24182  pserdv2  24184  abelthlem8  24193  abelthlem9  24194  abelth  24195  logtayl  24406  leibpi  24669  birthdaylem2  24679  amgmlem  24716  emcllem5  24726  fsumharmonic  24738  lgamcvg2  24781  ftalem5  24803  basellem3  24809  basellem8  24814  sgmval2  24869  fsumdvdscom  24911  dvdsflsumcom  24914  musum  24917  musumsum  24918  muinv  24919  fsumdvdsmul  24921  sgmppw  24922  1sgmprm  24924  chtlepsi  24931  pclogsum  24940  vmasum  24941  logfac2  24942  chpval2  24943  chpchtsum  24944  logexprlim  24950  logfacrlim2  24951  perfectlem2  24955  dchrsum2  24993  sumdchr2  24995  dchrhash  24996  dchr2sum  24998  sum2dchr  24999  pcbcctr  25001  bposlem2  25010  lgsquadlem1  25105  lgsquadlem2  25106  chebbnd1lem1  25158  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma  25231  logsqvma2  25232  selberglem1  25234  selberglem2  25235  selberg  25237  selberg2  25240  selberg3lem1  25246  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selbergr  25257  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsval2  25265  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd1  25275  pntlemk  25295  pntlemo  25296  axcgrrflx  25794  axcgrid  25796  axsegconlem1  25797  axsegconlem9  25805  ax5seglem1  25808  ax5seglem2  25809  ax5seglem9  25817  axlowdimlem16  25837  axlowdimlem17  25838  ecgrtg  25863  finsumvtxdg2ssteplem3  26443  rusgrnumwwlks  26869  fusgrhashclwwlkn  26956  fusgreghash2wsp  27202  numclwwlk4  27244  numclwwlk6  27248  indsum  30083  indsumin  30084  eulerpartlemsv1  30418  eulerpartlemsf  30421  eulerpartlemgs2  30442  eulerpartlemn  30443  plymulx0  30624  signsvfn  30659  fsum2dsub  30685  reprsuc  30693  hashreprin  30698  reprpmtf1o  30704  breprexplema  30708  breprexplemc  30710  breprexp  30711  breprexpnat  30712  vtsprod  30717  circlemeth  30718  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  hgt750lemd  30726  hgt750lemb  30734  hgt750lema  30735  subfaclim  31170  fwddifnp1  32272  knoppndvlem6  32508  rrnmet  33628  fsumshftdOLD  34238  jm2.22  37562  jm2.23  37563  flcidc  37744  binomcxplemnn0  38548  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  mccllem  39829  isumneg  39834  sumnnodd  39862  dvnmul  40158  dvnprodlem2  40162  dvnprodlem3  40163  stoweidlem37  40254  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  fourierdlem81  40404  fourierdlem83  40406  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  elaa2lem  40450  etransclem23  40474  etransclem24  40475  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem46  40497  rrxtopnfi  40506  rrndistlt  40510  sge0z  40592  sge0fsummpt  40607  sge0sup  40608  sge0resplit  40623  sge0split  40626  sge0ltfirpmpt2  40643  omeiunltfirp  40733  carageniuncllem2  40736  hoidmvlelem2  40810  hoidmvlelem3  40811  pwdif  41501  perfectALTVlem2  41631  nnsum3primesprm  41678  nnsum3primesgbe  41680  nnsum4primeseven  41688  altgsumbc  42130  altgsumbcALT  42131  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdig  42417  aacllem  42547  amgmwlem  42548