Theorem sumeq2dv 15637

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 15636	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

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

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764  df-fz 13436  df-seq 13937  df-sum 15622

This theorem is referenced by:  2sumeq2dv  15640  sumeq12dv  15641  sumeq12rdv  15642  fsumf1o  15658  fsumss  15660  fsumsplit  15676  isummulc1  15698  isumdivc  15699  isumge0  15701  fsum2dlem  15705  fsumshftm  15716  fsum0diag2  15718  fsummulc1  15720  fsumdivc  15721  fsumneg  15722  fsumsub  15723  fsum2mul  15724  telfsumo2  15738  fsumparts  15741  hashiun  15757  hash2iun  15758  hash2iun1dif1  15759  ackbijnn  15763  binomlem  15764  binom1p  15766  incexclem  15771  incexc  15772  incexc2  15773  isum1p  15776  arisum  15795  trireciplem  15797  geoserg  15801  pwdif  15803  geo2sum  15808  mertenslem1  15819  mertenslem2  15820  mertens  15821  binomfallfaclem2  15975  binomrisefac  15977  bpolylem  15983  bpolydiflem  15989  fsumkthpow  15991  efaddlem  16028  rpnnen2lem10  16160  rpnnen2lem11  16161  fsumdvds  16247  pwp1fsum  16330  phisum  16730  pcfac  16839  ramcl  16969  lagsubg2  19138  sylow2a  19563  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  26640  leibpi  26923  birthdaylem2  26933  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  fsumdvdsmulOLD  27178  sgmppw  27179  1sgmprm  27181  chtlepsi  27188  pclogsum  27197  vmasum  27198  logfac2  27199  chpval2  27200  chpchtsum  27201  logexprlim  27207  logfacrlim2  27208  perfectlem2  27212  dchrsum2  27250  sumdchr2  27252  dchrhash  27253  dchr2sum  27255  sum2dchr  27256  pcbcctr  27258  bposlem2  27267  lgsquadlem1  27362  lgsquadlem2  27363  chebbnd1lem1  27451  rplogsumlem1  27466  rplogsumlem2  27467  rpvmasumlem  27469  dchrisumlem1  27471  dchrisumlem2  27472  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrvmasum2if  27479  dchrvmasumiflem1  27483  dchrvmasumiflem2  27484  dchrisum0flblem1  27490  dchrisum0fno1  27493  rpvmasum2  27494  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrisum0lem3  27501  dchrisum0  27502  rplogsum  27509  mudivsum  27512  mulogsumlem  27513  mulogsum  27514  mulog2sumlem1  27516  mulog2sumlem2  27517  mulog2sumlem3  27518  vmalogdivsum2  27520  vmalogdivsum  27521  2vmadivsumlem  27522  logsqvma  27524  logsqvma2  27525  selberglem1  27527  selberglem2  27528  selberg  27530  selberg2  27533  selberg3lem1  27539  selberg4lem1  27542  selberg4  27543  pntrsumo1  27547  selbergr  27550  selberg3r  27551  selberg4r  27552  selberg34r  27553  pntsval2  27558  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  pntpbnd1  27568  pntlemk  27588  pntlemo  27589  axcgrrflx  29003  axcgrid  29005  axsegconlem1  29006  axsegconlem9  29014  ax5seglem1  29017  ax5seglem2  29018  ax5seglem9  29026  axlowdimlem16  29046  axlowdimlem17  29047  ecgrtg  29072  finsumvtxdg2ssteplem3  29637  rusgrnumwwlks  30066  fusgrhashclwwlkn  30170  fusgreghash2wsp  30429  numclwwlk6  30481  indsum  32957  indsumin  32958  elrgspnlem2  33341  vietadeg1  33759  eulerpartlemsv1  34538  eulerpartlemsf  34541  eulerpartlemgs2  34562  eulerpartlemn  34563  plymulx0  34729  signsvfn  34764  fsum2dsub  34789  reprsuc  34797  hashreprin  34802  reprpmtf1o  34808  breprexplema  34812  breprexplemc  34814  breprexp  34815  breprexpnat  34816  vtsprod  34821  circlemeth  34822  circlemethnat  34823  circlevma  34824  circlemethhgt  34825  hgt750lemd  34830  hgt750lemb  34838  hgt750lema  34839  subfaclim  35408  fwddifnp1  36385  knoppndvlem6  36743  rrnmet  38084  3factsumint2  42396  3factsumint3  42397  lcmineqlem1  42403  lcmineqlem3  42405  lcmineqlem6  42408  sticksstones8  42527  sticksstones9  42528  sticksstones10  42529  sticksstones11  42530  sticksstones12a  42531  sticksstones12  42532  sticksstones17  42537  sticksstones18  42538  sticksstones19  42539  aks6d1c6lem1  42544  aks6d1c6lem3  42546  aks6d1c7lem3  42556  unitscyglem2  42570  sumcubes  42687  fltnltalem  43024  jm2.22  43356  jm2.23  43357  flcidc  43531  binomcxplemnn0  44709  binomcxplemdvsum  44715  binomcxplemnotnn0  44716  mccllem  45961  isumneg  45966  sumnnodd  45994  dvnmul  46305  dvnprodlem2  46309  dvnprodlem3  46310  stoweidlem37  46399  dirkertrigeqlem2  46461  dirkertrigeqlem3  46462  fourierdlem81  46549  fourierdlem83  46551  fourierdlem93  46561  fourierdlem103  46571  fourierdlem104  46572  elaa2lem  46595  etransclem23  46619  etransclem24  46620  etransclem31  46627  etransclem32  46628  etransclem35  46631  etransclem46  46642  rrxtopnfi  46649  rrndistlt  46652  sge0z  46737  sge0fsummpt  46752  sge0sup  46753  sge0resplit  46768  sge0split  46771  sge0ltfirpmpt2  46788  omeiunltfirp  46881  carageniuncllem2  46884  hoidmvlelem2  46958  hoidmvlelem3  46959  perfectALTVlem2  48086  nnsum3primesprm  48154  nnsum3primesgbe  48156  nnsum4primeseven  48164  altgsumbc  48716  altgsumbcALT  48717  nn0sumshdiglemA  48983  nn0sumshdiglemB  48984  nn0sumshdig  48987  aacllem  50164  amgmwlem  50165