Theorem sumeq2dv 15646

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Σcsu 15629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-n0 12470  df-z 12556  df-uz 12820  df-fz 13482  df-seq 13964  df-sum 15630

This theorem is referenced by:  2sumeq2dv  15648  sumeq12dv  15649  sumeq12rdv  15650  fsumf1o  15666  fsumss  15668  fsumsplit  15684  isummulc1  15706  isumdivc  15707  isumge0  15709  fsum2dlem  15713  fsumshftm  15724  fsum0diag2  15726  fsummulc1  15728  fsumdivc  15729  fsumneg  15730  fsumsub  15731  fsum2mul  15732  telfsumo2  15746  fsumparts  15749  hashiun  15765  hash2iun  15766  hash2iun1dif1  15767  ackbijnn  15771  binomlem  15772  binom1p  15774  incexclem  15779  incexc  15780  incexc2  15781  isum1p  15784  arisum  15803  trireciplem  15805  geoserg  15809  pwdif  15811  geo2sum  15816  mertenslem1  15827  mertenslem2  15828  mertens  15829  binomfallfaclem2  15981  binomrisefac  15983  bpolylem  15989  bpolydiflem  15995  fsumkthpow  15997  efaddlem  16033  rpnnen2lem10  16163  rpnnen2lem11  16164  fsumdvds  16248  pwp1fsum  16331  phisum  16720  pcfac  16829  ramcl  16959  lagsubg2  19066  sylow2a  19482  rrxcph  24901  trirn  24909  rrxmval  24914  rrxmet  24917  ovoliunnul  25016  ovolicc2lem4  25029  uniioombllem4  25095  vitalilem5  25121  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  itg1mulc  25214  itg10a  25220  itg1climres  25224  itgss  25321  itgeqa  25323  itgsplit  25345  elply2  25702  elplyd  25708  plyeq0lem  25716  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  coeeq2  25748  coemullem  25756  coe1termlem  25764  plycjlem  25782  plyrecj  25785  dvply1  25789  elqaalem3  25826  aareccl  25831  aannenlem1  25833  taylpval  25871  dvtaylp  25874  pserdvlem2  25932  pserdv2  25934  abelthlem8  25943  abelthlem9  25944  abelth  25945  logtayl  26160  leibpi  26437  birthdaylem2  26447  amgmlem  26484  emcllem5  26494  fsumharmonic  26506  lgamcvg2  26549  ftalem5  26571  basellem3  26577  basellem8  26582  sgmval2  26637  fsumdvdscom  26679  dvdsflsumcom  26682  musum  26685  musumsum  26686  muinv  26687  fsumdvdsmul  26689  sgmppw  26690  1sgmprm  26692  chtlepsi  26699  pclogsum  26708  vmasum  26709  logfac2  26710  chpval2  26711  chpchtsum  26712  logexprlim  26718  logfacrlim2  26719  perfectlem2  26723  dchrsum2  26761  sumdchr2  26763  dchrhash  26764  dchr2sum  26766  sum2dchr  26767  pcbcctr  26769  bposlem2  26778  lgsquadlem1  26873  lgsquadlem2  26874  chebbnd1lem1  26962  rplogsumlem1  26977  rplogsumlem2  26978  rpvmasumlem  26980  dchrisumlem1  26982  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasum2lem  26989  dchrvmasum2if  26990  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrisum0flblem1  27001  dchrisum0fno1  27004  rpvmasum2  27005  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  dchrisum0  27013  rplogsum  27020  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  mulog2sumlem1  27027  mulog2sumlem2  27028  mulog2sumlem3  27029  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  logsqvma  27035  logsqvma2  27036  selberglem1  27038  selberglem2  27039  selberg  27041  selberg2  27044  selberg3lem1  27050  selberg4lem1  27053  selberg4  27054  pntrsumo1  27058  selbergr  27061  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntsval2  27069  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntpbnd1  27079  pntlemk  27099  pntlemo  27100  axcgrrflx  28162  axcgrid  28164  axsegconlem1  28165  axsegconlem9  28173  ax5seglem1  28176  ax5seglem2  28177  ax5seglem9  28185  axlowdimlem16  28205  axlowdimlem17  28206  ecgrtg  28231  finsumvtxdg2ssteplem3  28794  rusgrnumwwlks  29218  fusgrhashclwwlkn  29322  fusgreghash2wsp  29581  numclwwlk6  29633  indsum  33008  indsumin  33009  eulerpartlemsv1  33344  eulerpartlemsf  33347  eulerpartlemgs2  33368  eulerpartlemn  33369  plymulx0  33547  signsvfn  33582  fsum2dsub  33608  reprsuc  33616  hashreprin  33621  reprpmtf1o  33627  breprexplema  33631  breprexplemc  33633  breprexp  33634  breprexpnat  33635  vtsprod  33640  circlemeth  33641  circlemethnat  33642  circlevma  33643  circlemethhgt  33644  hgt750lemd  33649  hgt750lemb  33657  hgt750lema  33658  subfaclim  34168  fwddifnp1  35126  knoppndvlem6  35382  rrnmet  36686  3factsumint2  40876  3factsumint3  40877  lcmineqlem1  40883  lcmineqlem3  40885  lcmineqlem6  40888  sticksstones8  40958  sticksstones9  40959  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones17  40968  sticksstones18  40969  sticksstones19  40970  sumcubes  41207  fltnltalem  41401  jm2.22  41720  jm2.23  41721  flcidc  41902  binomcxplemnn0  43094  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  mccllem  44300  isumneg  44305  sumnnodd  44333  dvnmul  44646  dvnprodlem2  44650  dvnprodlem3  44651  stoweidlem37  44740  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  fourierdlem81  44890  fourierdlem83  44892  fourierdlem93  44902  fourierdlem103  44912  fourierdlem104  44913  elaa2lem  44936  etransclem23  44960  etransclem24  44961  etransclem31  44968  etransclem32  44969  etransclem35  44972  etransclem46  44983  rrxtopnfi  44990  rrndistlt  44993  sge0z  45078  sge0fsummpt  45093  sge0sup  45094  sge0resplit  45109  sge0split  45112  sge0ltfirpmpt2  45129  omeiunltfirp  45222  carageniuncllem2  45225  hoidmvlelem2  45299  hoidmvlelem3  45300  perfectALTVlem2  46377  nnsum3primesprm  46445  nnsum3primesgbe  46447  nnsum4primeseven  46455  altgsumbc  46982  altgsumbcALT  46983  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  nn0sumshdig  47263  aacllem  47802  amgmwlem  47803