Theorem sumeq2dv 15668

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

Hypothesis

Ref	Expression
sumeq2dv.1	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
sumeq2dv	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2dv

Step	Hyp	Ref	Expression
1		sumeq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 15667	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Σcsu 15652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530  df-uz 12794  df-fz 13469  df-seq 13967  df-sum 15653

This theorem is referenced by:  2sumeq2dv  15671  sumeq12dv  15672  sumeq12rdv  15673  fsumf1o  15689  fsumss  15691  fsumsplit  15707  isummulc1  15729  isumdivc  15730  isumge0  15732  fsum2dlem  15736  fsumshftm  15747  fsum0diag2  15749  fsummulc1  15751  fsumdivc  15752  fsumneg  15753  fsumsub  15754  fsum2mul  15755  telfsumo2  15769  fsumparts  15772  hashiun  15788  hash2iun  15789  hash2iun1dif1  15790  ackbijnn  15794  binomlem  15795  binom1p  15797  incexclem  15802  incexc  15803  incexc2  15804  isum1p  15807  arisum  15826  trireciplem  15828  geoserg  15832  pwdif  15834  geo2sum  15839  mertenslem1  15850  mertenslem2  15851  mertens  15852  binomfallfaclem2  16006  binomrisefac  16008  bpolylem  16014  bpolydiflem  16020  fsumkthpow  16022  efaddlem  16059  rpnnen2lem10  16191  rpnnen2lem11  16192  fsumdvds  16278  pwp1fsum  16361  phisum  16761  pcfac  16870  ramcl  17000  lagsubg2  19126  sylow2a  19549  rrxcph  25292  trirn  25300  rrxmval  25305  rrxmet  25308  ovoliunnul  25408  ovolicc2lem4  25421  uniioombllem4  25487  vitalilem5  25513  itg1addlem4  25600  itg1addlem5  25601  itg1mulc  25605  itg10a  25611  itg1climres  25615  itgss  25713  itgeqa  25715  itgsplit  25737  elply2  26101  elplyd  26107  plyeq0lem  26115  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeeq2  26147  coemullem  26155  coe1termlem  26163  plycjlem  26182  plyrecj  26187  dvply1  26191  elqaalem3  26229  aareccl  26234  aannenlem1  26236  taylpval  26274  dvtaylp  26278  pserdvlem2  26338  pserdv2  26340  abelthlem8  26349  abelthlem9  26350  abelth  26351  logtayl  26569  leibpi  26852  birthdaylem2  26862  amgmlem  26900  emcllem5  26910  fsumharmonic  26922  lgamcvg2  26965  ftalem5  26987  basellem3  26993  basellem8  26998  sgmval2  27053  fsumdvdscom  27095  dvdsflsumcom  27098  musum  27101  musumsum  27102  muinv  27103  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  sgmppw  27108  1sgmprm  27110  chtlepsi  27117  pclogsum  27126  vmasum  27127  logfac2  27128  chpval2  27129  chpchtsum  27130  logexprlim  27136  logfacrlim2  27137  perfectlem2  27141  dchrsum2  27179  sumdchr2  27181  dchrhash  27182  dchr2sum  27184  sum2dchr  27185  pcbcctr  27187  bposlem2  27196  lgsquadlem1  27291  lgsquadlem2  27292  chebbnd1lem1  27380  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  dchrisum0flblem1  27419  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  rplogsum  27438  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  logsqvma  27453  logsqvma2  27454  selberglem1  27456  selberglem2  27457  selberg  27459  selberg2  27462  selberg3lem1  27468  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  selbergr  27479  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntsval2  27487  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd1  27497  pntlemk  27517  pntlemo  27518  axcgrrflx  28841  axcgrid  28843  axsegconlem1  28844  axsegconlem9  28852  ax5seglem1  28855  ax5seglem2  28856  ax5seglem9  28864  axlowdimlem16  28884  axlowdimlem17  28885  ecgrtg  28910  finsumvtxdg2ssteplem3  29475  rusgrnumwwlks  29904  fusgrhashclwwlkn  30008  fusgreghash2wsp  30267  numclwwlk6  30319  indsum  32784  indsumin  32785  elrgspnlem2  33194  eulerpartlemsv1  34347  eulerpartlemsf  34350  eulerpartlemgs2  34371  eulerpartlemn  34372  plymulx0  34538  signsvfn  34573  fsum2dsub  34598  reprsuc  34606  hashreprin  34611  reprpmtf1o  34617  breprexplema  34621  breprexplemc  34623  breprexp  34624  breprexpnat  34625  vtsprod  34630  circlemeth  34631  circlemethnat  34632  circlevma  34633  circlemethhgt  34634  hgt750lemd  34639  hgt750lemb  34647  hgt750lema  34648  subfaclim  35175  fwddifnp1  36153  knoppndvlem6  36505  rrnmet  37823  3factsumint2  42010  3factsumint3  42011  lcmineqlem1  42017  lcmineqlem3  42019  lcmineqlem6  42022  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  aks6d1c6lem1  42158  aks6d1c6lem3  42160  aks6d1c7lem3  42170  unitscyglem2  42184  sumcubes  42301  fltnltalem  42650  jm2.22  42984  jm2.23  42985  flcidc  43159  binomcxplemnn0  44338  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  mccllem  45595  isumneg  45600  sumnnodd  45628  dvnmul  45941  dvnprodlem2  45945  dvnprodlem3  45946  stoweidlem37  46035  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  fourierdlem81  46185  fourierdlem83  46187  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  elaa2lem  46231  etransclem23  46255  etransclem24  46256  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem46  46278  rrxtopnfi  46285  rrndistlt  46288  sge0z  46373  sge0fsummpt  46388  sge0sup  46389  sge0resplit  46404  sge0split  46407  sge0ltfirpmpt2  46424  omeiunltfirp  46517  carageniuncllem2  46520  hoidmvlelem2  46594  hoidmvlelem3  46595  perfectALTVlem2  47723  nnsum3primesprm  47791  nnsum3primesgbe  47793  nnsum4primeseven  47801  altgsumbc  48340  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdig  48612  aacllem  49790  amgmwlem  49791