Theorem sumeq2dv 15753

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Σcsu 15737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-n0 12505  df-z 12592  df-uz 12863  df-fz 13536  df-seq 14038  df-sum 15738

This theorem is referenced by:  2sumeq2dv  15756  sumeq12dv  15757  sumeq12rdv  15758  fsumf1o  15774  fsumss  15776  fsumsplit  15792  isummulc1  15814  isumdivc  15815  isumge0  15817  fsum2dlem  15821  fsumshftm  15832  fsum0diag2  15834  fsummulc1  15836  fsumdivc  15837  fsumneg  15838  fsumsub  15839  fsum2mul  15840  telfsumo2  15855  fsumparts  15858  hashiun  15874  hash2iun  15875  hash2iun1dif1  15876  indsum  15880  ackbijnn  15882  binomlem  15883  binom1p  15885  incexclem  15890  incexc  15891  incexc2  15892  isum1p  15895  arisum  15914  trireciplem  15916  geoserg  15920  pwdif  15922  geo2sum  15927  mertenslem1  15938  mertenslem2  15939  mertens  15940  binomfallfaclem2  16094  binomrisefac  16096  bpolylem  16102  bpolydiflem  16108  fsumkthpow  16110  efaddlem  16147  rpnnen2lem10  16279  rpnnen2lem11  16280  fsumdvds  16366  pwp1fsum  16449  phisum  16850  pcfac  16959  ramcl  17089  lagsubg2  19265  sylow2a  19689  rrxcph  25520  trirn  25528  rrxmval  25533  rrxmet  25536  ovoliunnul  25635  ovolicc2lem4  25648  uniioombllem4  25714  vitalilem5  25740  itg1addlem4  25827  itg1addlem5  25828  itg1mulc  25832  itg10a  25838  itg1climres  25842  itgss  25940  itgeqa  25942  itgsplit  25964  elply2  26322  elplyd  26328  plyeq0lem  26336  plyaddlem1  26339  plymullem1  26340  coeeulem  26350  coeeq2  26368  coemullem  26376  coe1termlem  26384  plycjlem  26402  plyrecj  26407  plyn0mulidp  26411  dvply1  26414  elqaalem3  26451  aareccl  26456  aannenlem1  26458  taylpval  26496  dvtaylp  26499  pserdvlem2  26557  pserdv2  26559  abelthlem8  26568  abelthlem9  26569  abelth  26570  logtayl  26791  leibpi  27073  birthdaylem2  27083  amgmlem  27120  emcllem5  27130  fsumharmonic  27142  lgamcvg2  27185  ftalem5  27207  basellem3  27213  basellem8  27218  sgmval2  27273  fsumdvdscom  27315  dvdsflsumcom  27318  musum  27321  musumsum  27322  muinv  27323  fsumdvdsmul  27325  sgmppw  27327  1sgmprm  27329  chtlepsi  27336  pclogsum  27345  vmasum  27346  logfac2  27347  chpval2  27348  chpchtsum  27349  logexprlim  27355  logfacrlim2  27356  perfectlem2  27360  dchrsum2  27398  sumdchr2  27400  dchrhash  27401  dchr2sum  27403  sum2dchr  27404  pcbcctr  27406  bposlem2  27415  lgsquadlem1  27510  lgsquadlem2  27511  chebbnd1lem1  27599  rplogsumlem1  27614  rplogsumlem2  27615  rpvmasumlem  27617  dchrisumlem1  27619  dchrisumlem2  27620  dchrmusum2  27624  dchrvmasumlem1  27625  dchrvmasum2lem  27626  dchrvmasum2if  27627  dchrvmasumiflem1  27631  dchrvmasumiflem2  27632  dchrisum0flblem1  27638  dchrisum0fno1  27641  rpvmasum2  27642  dchrisum0lem2a  27647  dchrisum0lem2  27648  dchrisum0lem3  27649  dchrisum0  27650  rplogsum  27657  mudivsum  27660  mulogsumlem  27661  mulogsum  27662  mulog2sumlem1  27664  mulog2sumlem2  27665  mulog2sumlem3  27666  vmalogdivsum2  27668  vmalogdivsum  27669  2vmadivsumlem  27670  logsqvma  27672  logsqvma2  27673  selberglem1  27675  selberglem2  27676  selberg  27678  selberg2  27681  selberg3lem1  27687  selberg4lem1  27690  selberg4  27691  pntrsumo1  27695  selbergr  27698  selberg3r  27699  selberg4r  27700  selberg34r  27701  pntsval2  27706  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntpbnd1  27716  pntlemk  27736  pntlemo  27737  axcgrrflx  29205  axcgrid  29207  axsegconlem1  29208  axsegconlem9  29216  ax5seglem1  29219  ax5seglem2  29220  ax5seglem9  29228  axlowdimlem16  29248  axlowdimlem17  29249  ecgrtg  29274  finsumvtxdg2ssteplem3  29838  rusgrnumwwlks  30267  fusgrhashclwwlkn  30371  fusgreghash2wsp  30630  numclwwlk6  30682  indsumin  33122  elrgspnlem2  33504  vietadeg1  33913  eulerpartlemsv1  34691  eulerpartlemsf  34694  eulerpartlemgs2  34715  eulerpartlemn  34716  signsvfn  34914  fsum2dsub  34939  reprsuc  34947  hashreprin  34952  reprpmtf1o  34958  breprexplema  34962  breprexplemc  34964  breprexp  34965  breprexpnat  34966  vtsprod  34971  circlemeth  34972  circlemethnat  34973  circlevma  34974  circlemethhgt  34975  hgt750lemd  34980  hgt750lemb  34988  hgt750lema  34989  subfaclim  35613  fwddifnp1  36590  knoppndvlem6  37029  rrnmet  38402  3factsumint2  42713  3factsumint3  42714  lcmineqlem1  42720  lcmineqlem3  42722  lcmineqlem6  42725  sticksstones8  42844  sticksstones9  42845  sticksstones10  42846  sticksstones11  42847  sticksstones12a  42848  sticksstones12  42849  sticksstones17  42854  sticksstones18  42855  sticksstones19  42856  aks6d1c6lem1  42861  aks6d1c6lem3  42863  aks6d1c7lem3  42873  unitscyglem2  42887  sumcubes  42998  fltnltalem  43320  jm2.22  43648  jm2.23  43649  flcidc  43823  binomcxplemnn0  44985  binomcxplemdvsum  44991  binomcxplemnotnn0  44992  mccllem  46239  isumneg  46244  sumnnodd  46272  dvnmul  46583  dvnprodlem2  46587  dvnprodlem3  46588  stoweidlem37  46677  dirkertrigeqlem2  46739  dirkertrigeqlem3  46740  fourierdlem81  46827  fourierdlem83  46829  fourierdlem93  46839  fourierdlem103  46849  fourierdlem104  46850  elaa2lem  46873  etransclem23  46897  etransclem24  46898  etransclem31  46905  etransclem32  46906  etransclem35  46909  etransclem46  46920  rrxtopnfi  46927  rrndistlt  46930  sge0z  47015  sge0fsummpt  47030  sge0sup  47031  sge0resplit  47046  sge0split  47049  sge0ltfirpmpt2  47066  omeiunltfirp  47159  carageniuncllem2  47162  hoidmvlelem2  47236  hoidmvlelem3  47237  ppivalnn  48307  perfectALTVlem2  48410  nnsum3primesprm  48478  nnsum3primesgbe  48480  nnsum4primeseven  48488  altgsumbc  49051  altgsumbcALT  49052  nn0sumshdiglemA  49318  nn0sumshdiglemB  49319  nn0sumshdig  49322  aacllem  50509  amgmwlem  50510