Theorem sumeq2dv 15655

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Σcsu 15639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453  df-seq 13955  df-sum 15640

This theorem is referenced by:  2sumeq2dv  15658  sumeq12dv  15659  sumeq12rdv  15660  fsumf1o  15676  fsumss  15678  fsumsplit  15694  isummulc1  15716  isumdivc  15717  isumge0  15719  fsum2dlem  15723  fsumshftm  15734  fsum0diag2  15736  fsummulc1  15738  fsumdivc  15739  fsumneg  15740  fsumsub  15741  fsum2mul  15742  telfsumo2  15757  fsumparts  15760  hashiun  15776  hash2iun  15777  hash2iun1dif1  15778  indsum  15782  ackbijnn  15784  binomlem  15785  binom1p  15787  incexclem  15792  incexc  15793  incexc2  15794  isum1p  15797  arisum  15816  trireciplem  15818  geoserg  15822  pwdif  15824  geo2sum  15829  mertenslem1  15840  mertenslem2  15841  mertens  15842  binomfallfaclem2  15996  binomrisefac  15998  bpolylem  16004  bpolydiflem  16010  fsumkthpow  16012  efaddlem  16049  rpnnen2lem10  16181  rpnnen2lem11  16182  fsumdvds  16268  pwp1fsum  16351  phisum  16752  pcfac  16861  ramcl  16991  lagsubg2  19160  sylow2a  19585  rrxcph  25377  trirn  25385  rrxmval  25390  rrxmet  25393  ovoliunnul  25492  ovolicc2lem4  25505  uniioombllem4  25571  vitalilem5  25597  itg1addlem4  25684  itg1addlem5  25685  itg1mulc  25689  itg10a  25695  itg1climres  25699  itgss  25797  itgeqa  25799  itgsplit  25821  elply2  26179  elplyd  26185  plyeq0lem  26193  plyaddlem1  26196  plymullem1  26197  coeeulem  26207  coeeq2  26225  coemullem  26233  coe1termlem  26241  plycjlem  26259  plyrecj  26264  dvply1  26268  elqaalem3  26305  aareccl  26310  aannenlem1  26312  taylpval  26350  dvtaylp  26353  pserdvlem2  26411  pserdv2  26413  abelthlem8  26422  abelthlem9  26423  abelth  26424  logtayl  26642  leibpi  26924  birthdaylem2  26934  amgmlem  26971  emcllem5  26981  fsumharmonic  26993  lgamcvg2  27036  ftalem5  27058  basellem3  27064  basellem8  27069  sgmval2  27124  fsumdvdscom  27166  dvdsflsumcom  27169  musum  27172  musumsum  27173  muinv  27174  fsumdvdsmul  27176  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  29001  axcgrid  29003  axsegconlem1  29004  axsegconlem9  29012  ax5seglem1  29015  ax5seglem2  29016  ax5seglem9  29024  axlowdimlem16  29044  axlowdimlem17  29045  ecgrtg  29070  finsumvtxdg2ssteplem3  29634  rusgrnumwwlks  30063  fusgrhashclwwlkn  30167  fusgreghash2wsp  30426  numclwwlk6  30478  indsumin  32940  elrgspnlem2  33324  vietadeg1  33762  eulerpartlemsv1  34540  eulerpartlemsf  34543  eulerpartlemgs2  34564  eulerpartlemn  34565  plymulx0  34731  signsvfn  34766  fsum2dsub  34791  reprsuc  34799  hashreprin  34804  reprpmtf1o  34810  breprexplema  34814  breprexplemc  34816  breprexp  34817  breprexpnat  34818  vtsprod  34823  circlemeth  34824  circlemethnat  34825  circlevma  34826  circlemethhgt  34827  hgt750lemd  34832  hgt750lemb  34840  hgt750lema  34841  subfaclim  35416  fwddifnp1  36393  knoppndvlem6  36823  rrnmet  38196  3factsumint2  42507  3factsumint3  42508  lcmineqlem1  42514  lcmineqlem3  42516  lcmineqlem6  42519  sticksstones8  42638  sticksstones9  42639  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones17  42648  sticksstones18  42649  sticksstones19  42650  aks6d1c6lem1  42655  aks6d1c6lem3  42657  aks6d1c7lem3  42667  unitscyglem2  42681  sumcubes  42790  fltnltalem  43112  jm2.22  43440  jm2.23  43441  flcidc  43615  binomcxplemnn0  44793  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  mccllem  46042  isumneg  46047  sumnnodd  46075  dvnmul  46386  dvnprodlem2  46390  dvnprodlem3  46391  stoweidlem37  46480  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  fourierdlem81  46630  fourierdlem83  46632  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  elaa2lem  46676  etransclem23  46700  etransclem24  46701  etransclem31  46708  etransclem32  46709  etransclem35  46712  etransclem46  46723  rrxtopnfi  46730  rrndistlt  46733  sge0z  46818  sge0fsummpt  46833  sge0sup  46834  sge0resplit  46849  sge0split  46852  sge0ltfirpmpt2  46869  omeiunltfirp  46962  carageniuncllem2  46965  hoidmvlelem2  47039  hoidmvlelem3  47040  ppivalnn  48110  perfectALTVlem2  48213  nnsum3primesprm  48281  nnsum3primesgbe  48283  nnsum4primeseven  48291  altgsumbc  48843  altgsumbcALT  48844  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdig  49114  aacllem  50291  amgmwlem  50292