Theorem sumeq2dv 15658

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Σcsu 15642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783  df-fz 13456  df-seq 13958  df-sum 15643

This theorem is referenced by:  2sumeq2dv  15661  sumeq12dv  15662  sumeq12rdv  15663  fsumf1o  15679  fsumss  15681  fsumsplit  15697  isummulc1  15719  isumdivc  15720  isumge0  15722  fsum2dlem  15726  fsumshftm  15737  fsum0diag2  15739  fsummulc1  15741  fsumdivc  15742  fsumneg  15743  fsumsub  15744  fsum2mul  15745  telfsumo2  15760  fsumparts  15763  hashiun  15779  hash2iun  15780  hash2iun1dif1  15781  indsum  15785  ackbijnn  15787  binomlem  15788  binom1p  15790  incexclem  15795  incexc  15796  incexc2  15797  isum1p  15800  arisum  15819  trireciplem  15821  geoserg  15825  pwdif  15827  geo2sum  15832  mertenslem1  15843  mertenslem2  15844  mertens  15845  binomfallfaclem2  15999  binomrisefac  16001  bpolylem  16007  bpolydiflem  16013  fsumkthpow  16015  efaddlem  16052  rpnnen2lem10  16184  rpnnen2lem11  16185  fsumdvds  16271  pwp1fsum  16354  phisum  16755  pcfac  16864  ramcl  16994  lagsubg2  19163  sylow2a  19588  rrxcph  25372  trirn  25380  rrxmval  25385  rrxmet  25388  ovoliunnul  25487  ovolicc2lem4  25500  uniioombllem4  25566  vitalilem5  25592  itg1addlem4  25679  itg1addlem5  25680  itg1mulc  25684  itg10a  25690  itg1climres  25694  itgss  25792  itgeqa  25794  itgsplit  25816  elply2  26174  elplyd  26180  plyeq0lem  26188  plyaddlem1  26191  plymullem1  26192  coeeulem  26202  coeeq2  26220  coemullem  26228  coe1termlem  26236  plycjlem  26254  plyrecj  26259  dvply1  26263  elqaalem3  26301  aareccl  26306  aannenlem1  26308  taylpval  26346  dvtaylp  26350  pserdvlem2  26409  pserdv2  26411  abelthlem8  26420  abelthlem9  26421  abelth  26422  logtayl  26640  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  sgmppw  27177  1sgmprm  27179  chtlepsi  27186  pclogsum  27195  vmasum  27196  logfac2  27197  chpval2  27198  chpchtsum  27199  logexprlim  27205  logfacrlim2  27206  perfectlem2  27210  dchrsum2  27248  sumdchr2  27250  dchrhash  27251  dchr2sum  27253  sum2dchr  27254  pcbcctr  27256  bposlem2  27265  lgsquadlem1  27360  lgsquadlem2  27361  chebbnd1lem1  27449  rplogsumlem1  27464  rplogsumlem2  27465  rpvmasumlem  27467  dchrisumlem1  27469  dchrisumlem2  27470  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2lem  27476  dchrvmasum2if  27477  dchrvmasumiflem1  27481  dchrvmasumiflem2  27482  dchrisum0flblem1  27488  dchrisum0fno1  27491  rpvmasum2  27492  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrisum0lem3  27499  dchrisum0  27500  rplogsum  27507  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem1  27514  mulog2sumlem2  27515  mulog2sumlem3  27516  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  logsqvma  27522  logsqvma2  27523  selberglem1  27525  selberglem2  27526  selberg  27528  selberg2  27531  selberg3lem1  27537  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  selbergr  27548  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntsval2  27556  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntpbnd1  27566  pntlemk  27586  pntlemo  27587  axcgrrflx  29000  axcgrid  29002  axsegconlem1  29003  axsegconlem9  29011  ax5seglem1  29014  ax5seglem2  29015  ax5seglem9  29023  axlowdimlem16  29043  axlowdimlem17  29044  ecgrtg  29069  finsumvtxdg2ssteplem3  29634  rusgrnumwwlks  30063  fusgrhashclwwlkn  30167  fusgreghash2wsp  30426  numclwwlk6  30478  indsumin  32939  elrgspnlem2  33322  vietadeg1  33740  eulerpartlemsv1  34519  eulerpartlemsf  34522  eulerpartlemgs2  34543  eulerpartlemn  34544  plymulx0  34710  signsvfn  34745  fsum2dsub  34770  reprsuc  34778  hashreprin  34783  reprpmtf1o  34789  breprexplema  34793  breprexplemc  34795  breprexp  34796  breprexpnat  34797  vtsprod  34802  circlemeth  34803  circlemethnat  34804  circlevma  34805  circlemethhgt  34806  hgt750lemd  34811  hgt750lemb  34819  hgt750lema  34820  subfaclim  35389  fwddifnp1  36366  knoppndvlem6  36796  rrnmet  38167  3factsumint2  42478  3factsumint3  42479  lcmineqlem1  42485  lcmineqlem3  42487  lcmineqlem6  42490  sticksstones8  42609  sticksstones9  42610  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones12  42614  sticksstones17  42619  sticksstones18  42620  sticksstones19  42621  aks6d1c6lem1  42626  aks6d1c6lem3  42628  aks6d1c7lem3  42638  unitscyglem2  42652  sumcubes  42762  fltnltalem  43112  jm2.22  43444  jm2.23  43445  flcidc  43619  binomcxplemnn0  44797  binomcxplemdvsum  44803  binomcxplemnotnn0  44804  mccllem  46048  isumneg  46053  sumnnodd  46081  dvnmul  46392  dvnprodlem2  46396  dvnprodlem3  46397  stoweidlem37  46486  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  fourierdlem81  46636  fourierdlem83  46638  fourierdlem93  46648  fourierdlem103  46658  fourierdlem104  46659  elaa2lem  46682  etransclem23  46706  etransclem24  46707  etransclem31  46714  etransclem32  46715  etransclem35  46718  etransclem46  46729  rrxtopnfi  46736  rrndistlt  46739  sge0z  46824  sge0fsummpt  46839  sge0sup  46840  sge0resplit  46855  sge0split  46858  sge0ltfirpmpt2  46875  omeiunltfirp  46968  carageniuncllem2  46971  hoidmvlelem2  47045  hoidmvlelem3  47046  ppivalnn  48110  perfectALTVlem2  48213  nnsum3primesprm  48281  nnsum3primesgbe  48283  nnsum4primeseven  48291  altgsumbc  48843  altgsumbcALT  48844  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdig  49114  aacllem  50291  amgmwlem  50292