Theorem sumeq2dv 15721

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Σcsu 15705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-1st 7996  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-n0 12510  df-z 12597  df-uz 12861  df-fz 13530  df-seq 14025  df-sum 15706

This theorem is referenced by:  2sumeq2dv  15724  sumeq12dv  15725  sumeq12rdv  15726  fsumf1o  15742  fsumss  15744  fsumsplit  15760  isummulc1  15782  isumdivc  15783  isumge0  15785  fsum2dlem  15789  fsumshftm  15800  fsum0diag2  15802  fsummulc1  15804  fsumdivc  15805  fsumneg  15806  fsumsub  15807  fsum2mul  15808  telfsumo2  15822  fsumparts  15825  hashiun  15841  hash2iun  15842  hash2iun1dif1  15843  ackbijnn  15847  binomlem  15848  binom1p  15850  incexclem  15855  incexc  15856  incexc2  15857  isum1p  15860  arisum  15879  trireciplem  15881  geoserg  15885  pwdif  15887  geo2sum  15892  mertenslem1  15903  mertenslem2  15904  mertens  15905  binomfallfaclem2  16059  binomrisefac  16061  bpolylem  16067  bpolydiflem  16073  fsumkthpow  16075  efaddlem  16112  rpnnen2lem10  16242  rpnnen2lem11  16243  fsumdvds  16328  pwp1fsum  16411  phisum  16811  pcfac  16920  ramcl  17050  lagsubg2  19182  sylow2a  19606  rrxcph  25363  trirn  25371  rrxmval  25376  rrxmet  25379  ovoliunnul  25479  ovolicc2lem4  25492  uniioombllem4  25558  vitalilem5  25584  itg1addlem4  25671  itg1addlem5  25672  itg1mulc  25676  itg10a  25682  itg1climres  25686  itgss  25784  itgeqa  25786  itgsplit  25808  elply2  26172  elplyd  26178  plyeq0lem  26186  plyaddlem1  26189  plymullem1  26190  coeeulem  26200  coeeq2  26218  coemullem  26226  coe1termlem  26234  plycjlem  26253  plyrecj  26258  dvply1  26262  elqaalem3  26300  aareccl  26305  aannenlem1  26307  taylpval  26345  dvtaylp  26349  pserdvlem2  26409  pserdv2  26411  abelthlem8  26420  abelthlem9  26421  abelth  26422  logtayl  26639  leibpi  26922  birthdaylem2  26932  amgmlem  26970  emcllem5  26980  fsumharmonic  26992  lgamcvg2  27035  ftalem5  27057  basellem3  27063  basellem8  27068  sgmval2  27123  fsumdvdscom  27165  dvdsflsumcom  27168  musum  27171  musumsum  27172  muinv  27173  fsumdvdsmul  27175  fsumdvdsmulOLD  27177  sgmppw  27178  1sgmprm  27180  chtlepsi  27187  pclogsum  27196  vmasum  27197  logfac2  27198  chpval2  27199  chpchtsum  27200  logexprlim  27206  logfacrlim2  27207  perfectlem2  27211  dchrsum2  27249  sumdchr2  27251  dchrhash  27252  dchr2sum  27254  sum2dchr  27255  pcbcctr  27257  bposlem2  27266  lgsquadlem1  27361  lgsquadlem2  27362  chebbnd1lem1  27450  rplogsumlem1  27465  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrvmasum2if  27478  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  dchrisum0flblem1  27489  dchrisum0fno1  27492  rpvmasum2  27493  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  dchrisum0  27501  rplogsum  27508  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem1  27515  mulog2sumlem2  27516  mulog2sumlem3  27517  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  logsqvma  27523  logsqvma2  27524  selberglem1  27526  selberglem2  27527  selberg  27529  selberg2  27532  selberg3lem1  27538  selberg4lem1  27541  selberg4  27542  pntrsumo1  27546  selbergr  27549  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntsval2  27557  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntpbnd1  27567  pntlemk  27587  pntlemo  27588  axcgrrflx  28860  axcgrid  28862  axsegconlem1  28863  axsegconlem9  28871  ax5seglem1  28874  ax5seglem2  28875  ax5seglem9  28883  axlowdimlem16  28903  axlowdimlem17  28904  ecgrtg  28929  finsumvtxdg2ssteplem3  29494  rusgrnumwwlks  29923  fusgrhashclwwlkn  30027  fusgreghash2wsp  30286  numclwwlk6  30338  indsum  32791  indsumin  32792  elrgspnlem2  33191  eulerpartlemsv1  34333  eulerpartlemsf  34336  eulerpartlemgs2  34357  eulerpartlemn  34358  plymulx0  34537  signsvfn  34572  fsum2dsub  34597  reprsuc  34605  hashreprin  34610  reprpmtf1o  34616  breprexplema  34620  breprexplemc  34622  breprexp  34623  breprexpnat  34624  vtsprod  34629  circlemeth  34630  circlemethnat  34631  circlevma  34632  circlemethhgt  34633  hgt750lemd  34638  hgt750lemb  34646  hgt750lema  34647  subfaclim  35168  fwddifnp1  36141  knoppndvlem6  36493  rrnmet  37811  3factsumint2  41998  3factsumint3  41999  lcmineqlem1  42005  lcmineqlem3  42007  lcmineqlem6  42010  sticksstones8  42129  sticksstones9  42130  sticksstones10  42131  sticksstones11  42132  sticksstones12a  42133  sticksstones12  42134  sticksstones17  42139  sticksstones18  42140  sticksstones19  42141  aks6d1c6lem1  42146  aks6d1c6lem3  42148  aks6d1c7lem3  42158  unitscyglem2  42172  sumcubes  42326  fltnltalem  42651  jm2.22  42985  jm2.23  42986  flcidc  43160  binomcxplemnn0  44340  binomcxplemdvsum  44346  binomcxplemnotnn0  44347  mccllem  45584  isumneg  45589  sumnnodd  45617  dvnmul  45930  dvnprodlem2  45934  dvnprodlem3  45935  stoweidlem37  46024  dirkertrigeqlem2  46086  dirkertrigeqlem3  46087  fourierdlem81  46174  fourierdlem83  46176  fourierdlem93  46186  fourierdlem103  46196  fourierdlem104  46197  elaa2lem  46220  etransclem23  46244  etransclem24  46245  etransclem31  46252  etransclem32  46253  etransclem35  46256  etransclem46  46267  rrxtopnfi  46274  rrndistlt  46277  sge0z  46362  sge0fsummpt  46377  sge0sup  46378  sge0resplit  46393  sge0split  46396  sge0ltfirpmpt2  46413  omeiunltfirp  46506  carageniuncllem2  46509  hoidmvlelem2  46583  hoidmvlelem3  46584  perfectALTVlem2  47682  nnsum3primesprm  47750  nnsum3primesgbe  47752  nnsum4primeseven  47760  altgsumbc  48241  altgsumbcALT  48242  nn0sumshdiglemA  48513  nn0sumshdiglemB  48514  nn0sumshdig  48517  aacllem  49415  amgmwlem  49416