Theorem sumeq2dv 15396

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 3109	. 2 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
3	2	sumeq2d 15395	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-cnex 10911  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931  ax-pre-mulgt0 10932

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-1st 7817  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999  df-sub 11190  df-neg 11191  df-nn 11957  df-n0 12217  df-z 12303  df-uz 12565  df-fz 13222  df-seq 13703  df-sum 15379

This theorem is referenced by:  2sumeq2dv  15398  sumeq12dv  15399  sumeq12rdv  15400  fsumf1o  15416  fsumss  15418  fsumsplit  15434  isummulc1  15456  isumdivc  15457  isumge0  15459  fsum2dlem  15463  fsumshftm  15474  fsum0diag2  15476  fsummulc1  15478  fsumdivc  15479  fsumneg  15480  fsumsub  15481  fsum2mul  15482  telfsumo2  15496  fsumparts  15499  hashiun  15515  hash2iun  15516  hash2iun1dif1  15517  ackbijnn  15521  binomlem  15522  binom1p  15524  incexclem  15529  incexc  15530  incexc2  15531  isum1p  15534  arisum  15553  trireciplem  15555  geoserg  15559  pwdif  15561  geo2sum  15566  mertenslem1  15577  mertenslem2  15578  mertens  15579  binomfallfaclem2  15731  binomrisefac  15733  bpolylem  15739  bpolydiflem  15745  fsumkthpow  15747  efaddlem  15783  rpnnen2lem10  15913  rpnnen2lem11  15914  fsumdvds  15998  pwp1fsum  16081  phisum  16472  pcfac  16581  ramcl  16711  lagsubg2  18798  sylow2a  19205  rrxcph  24537  trirn  24545  rrxmval  24550  rrxmet  24553  ovoliunnul  24652  ovolicc2lem4  24665  uniioombllem4  24731  vitalilem5  24757  itg1addlem4  24844  itg1addlem4OLD  24845  itg1addlem5  24846  itg1mulc  24850  itg10a  24856  itg1climres  24860  itgss  24957  itgeqa  24959  itgsplit  24981  elply2  25338  elplyd  25344  plyeq0lem  25352  plyaddlem1  25355  plymullem1  25356  coeeulem  25366  coeeq2  25384  coemullem  25392  coe1termlem  25400  plycjlem  25418  plyrecj  25421  dvply1  25425  elqaalem3  25462  aareccl  25467  aannenlem1  25469  taylpval  25507  dvtaylp  25510  pserdvlem2  25568  pserdv2  25570  abelthlem8  25579  abelthlem9  25580  abelth  25581  logtayl  25796  leibpi  26073  birthdaylem2  26083  amgmlem  26120  emcllem5  26130  fsumharmonic  26142  lgamcvg2  26185  ftalem5  26207  basellem3  26213  basellem8  26218  sgmval2  26273  fsumdvdscom  26315  dvdsflsumcom  26318  musum  26321  musumsum  26322  muinv  26323  fsumdvdsmul  26325  sgmppw  26326  1sgmprm  26328  chtlepsi  26335  pclogsum  26344  vmasum  26345  logfac2  26346  chpval2  26347  chpchtsum  26348  logexprlim  26354  logfacrlim2  26355  perfectlem2  26359  dchrsum2  26397  sumdchr2  26399  dchrhash  26400  dchr2sum  26402  sum2dchr  26403  pcbcctr  26405  bposlem2  26414  lgsquadlem1  26509  lgsquadlem2  26510  chebbnd1lem1  26598  rplogsumlem1  26613  rplogsumlem2  26614  rpvmasumlem  26616  dchrisumlem1  26618  dchrisumlem2  26619  dchrmusum2  26623  dchrvmasumlem1  26624  dchrvmasum2lem  26625  dchrvmasum2if  26626  dchrvmasumiflem1  26630  dchrvmasumiflem2  26631  dchrisum0flblem1  26637  dchrisum0fno1  26640  rpvmasum2  26641  dchrisum0lem2a  26646  dchrisum0lem2  26647  dchrisum0lem3  26648  dchrisum0  26649  rplogsum  26656  mudivsum  26659  mulogsumlem  26660  mulogsum  26661  mulog2sumlem1  26663  mulog2sumlem2  26664  mulog2sumlem3  26665  vmalogdivsum2  26667  vmalogdivsum  26668  2vmadivsumlem  26669  logsqvma  26671  logsqvma2  26672  selberglem1  26674  selberglem2  26675  selberg  26677  selberg2  26680  selberg3lem1  26686  selberg4lem1  26689  selberg4  26690  pntrsumo1  26694  selbergr  26697  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntsval2  26705  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntpbnd1  26715  pntlemk  26735  pntlemo  26736  axcgrrflx  27263  axcgrid  27265  axsegconlem1  27266  axsegconlem9  27274  ax5seglem1  27277  ax5seglem2  27278  ax5seglem9  27286  axlowdimlem16  27306  axlowdimlem17  27307  ecgrtg  27332  finsumvtxdg2ssteplem3  27895  rusgrnumwwlks  28318  fusgrhashclwwlkn  28422  fusgreghash2wsp  28681  numclwwlk6  28733  indsum  31968  indsumin  31969  eulerpartlemsv1  32302  eulerpartlemsf  32305  eulerpartlemgs2  32326  eulerpartlemn  32327  plymulx0  32505  signsvfn  32540  fsum2dsub  32566  reprsuc  32574  hashreprin  32579  reprpmtf1o  32585  breprexplema  32589  breprexplemc  32591  breprexp  32592  breprexpnat  32593  vtsprod  32598  circlemeth  32599  circlemethnat  32600  circlevma  32601  circlemethhgt  32602  hgt750lemd  32607  hgt750lemb  32615  hgt750lema  32616  subfaclim  33129  fwddifnp1  34446  knoppndvlem6  34676  rrnmet  35966  3factsumint2  40010  3factsumint3  40011  lcmineqlem1  40017  lcmineqlem3  40019  lcmineqlem6  40022  sticksstones8  40089  sticksstones9  40090  sticksstones10  40091  sticksstones11  40092  sticksstones12a  40093  sticksstones12  40094  sticksstones17  40099  sticksstones18  40100  sticksstones19  40101  fltnltalem  40479  jm2.22  40797  jm2.23  40798  flcidc  40979  binomcxplemnn0  41920  binomcxplemdvsum  41926  binomcxplemnotnn0  41927  mccllem  43092  isumneg  43097  sumnnodd  43125  dvnmul  43438  dvnprodlem2  43442  dvnprodlem3  43443  stoweidlem37  43532  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  fourierdlem81  43682  fourierdlem83  43684  fourierdlem93  43694  fourierdlem103  43704  fourierdlem104  43705  elaa2lem  43728  etransclem23  43752  etransclem24  43753  etransclem31  43760  etransclem32  43761  etransclem35  43764  etransclem46  43775  rrxtopnfi  43782  rrndistlt  43785  sge0z  43867  sge0fsummpt  43882  sge0sup  43883  sge0resplit  43898  sge0split  43901  sge0ltfirpmpt2  43918  omeiunltfirp  44011  carageniuncllem2  44014  hoidmvlelem2  44088  hoidmvlelem3  44089  perfectALTVlem2  45126  nnsum3primesprm  45194  nnsum3primesgbe  45196  nnsum4primeseven  45204  altgsumbc  45640  altgsumbcALT  45641  nn0sumshdiglemA  45917  nn0sumshdiglemB  45918  nn0sumshdig  45921  aacllem  46457  amgmwlem  46458