Theorem sumeq2dv 15779

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Σcsu 15763

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609  df-uz 12881  df-fz 13554  df-seq 14058  df-sum 15764

This theorem is used by:  2sumeq2dv  15781  sumeq12dv  15782  sumeq12rdv  15783  fsumf1o  15799  fsumss  15801  fsumsplit  15817  isummulc1  15839  isumdivc  15840  isumge0  15842  fsum2dlem  15846  fsumshftm  15857  fsum0diag2  15859  fsummulc1  15861  fsumdivc  15862  fsumneg  15863  fsumsub  15864  fsum2mul  15865  telfsumo2  15880  fsumparts  15883  hashiun  15899  hash2iun  15900  hash2iun1dif1  15901  indsum  15905  ackbijnn  15907  binomlem  15908  binom1p  15910  incexclem  15915  incexc  15916  incexc2  15917  isum1p  15920  arisum  15939  trireciplem  15941  geoserg  15945  pwdif  15947  geo2sum  15952  mertenslem1  15963  mertenslem2  15964  mertens  15965  binomfallfaclem2  16118  binomrisefac  16120  bpolylem  16126  bpolydiflem  16132  fsumkthpow  16134  efaddlem  16171  rpnnen2lem10  16303  rpnnen2lem11  16304  fsumdvds  16390  pwp1fsum  16473  phisum  16874  pcfac  16983  ramcl  17113  lagsubg2  19311  sylow2a  19735  rrxcph  25604  trirn  25612  rrxmval  25617  rrxmet  25620  ovoliunnul  25719  ovolicc2lem4  25732  uniioombllem4  25798  vitalilem5  25824  itg1addlem4  25911  itg1addlem5  25912  itg1mulc  25916  itg10a  25922  itg1climres  25926  itgss  26024  itgeqa  26026  itgsplit  26048  elply2  26406  elplyd  26412  plyeq0lem  26420  plyaddlem1  26423  plymullem1  26424  coeeulem  26434  coeeq2  26452  coemullem  26460  coe1termlem  26468  plycjlem  26486  plyrecj  26491  plyn0mulidp  26495  dvply1  26498  elqaalem3  26535  aareccl  26542  aannenlem1  26544  taylpval  26583  dvtaylp  26586  pserdvlem2  26644  pserdv2  26646  abelthlem8  26655  abelthlem9  26656  abelth  26657  logtayl  26878  leibpi  27160  birthdaylem2  27170  amgmlem  27207  emcllem5  27217  fsumharmonic  27229  lgamcvg2  27272  ftalem5  27294  basellem3  27300  basellem8  27305  sgmval2  27360  fsumdvdscom  27402  dvdsflsumcom  27405  musum  27408  musumsum  27409  muinv  27410  fsumdvdsmul  27412  sgmppw  27414  1sgmprm  27416  chtlepsi  27423  pclogsum  27432  vmasum  27433  logfac2  27434  chpval2  27435  chpchtsum  27436  logexprlim  27442  logfacrlim2  27443  perfectlem2  27447  dchrsum2  27485  sumdchr2  27487  dchrhash  27488  dchr2sum  27490  sum2dchr  27491  pcbcctr  27493  bposlem2  27502  lgsquadlem1  27597  lgsquadlem2  27598  chebbnd1lem1  27686  rplogsumlem1  27701  rplogsumlem2  27702  rpvmasumlem  27704  dchrisumlem1  27706  dchrisumlem2  27707  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2lem  27713  dchrvmasum2if  27714  dchrvmasumiflem1  27718  dchrvmasumiflem2  27719  dchrisum0flblem1  27725  dchrisum0fno1  27728  rpvmasum2  27729  dchrisum0lem2a  27734  dchrisum0lem2  27735  dchrisum0lem3  27736  dchrisum0  27737  rplogsum  27744  mudivsum  27747  mulogsumlem  27748  mulogsum  27749  mulog2sumlem1  27751  mulog2sumlem2  27752  mulog2sumlem3  27753  vmalogdivsum2  27755  vmalogdivsum  27756  2vmadivsumlem  27757  logsqvma  27759  logsqvma2  27760  selberglem1  27762  selberglem2  27763  selberg  27765  selberg2  27768  selberg3lem1  27774  selberg4lem1  27777  selberg4  27778  pntrsumo1  27782  selbergr  27785  selberg3r  27786  selberg4r  27787  selberg34r  27788  pntsval2  27793  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntpbnd1  27803  pntlemk  27823  pntlemo  27824  axcgrrflx  29321  axcgrid  29323  axsegconlem1  29324  axsegconlem9  29332  ax5seglem1  29335  ax5seglem2  29336  ax5seglem9  29344  axlowdimlem16  29364  axlowdimlem17  29365  ecgrtg  29390  finsumvtxdg2ssteplem3  29957  rusgrnumwwlks  30395  fusgrhashclwwlkn  30499  fusgreghash2wsp  30762  numclwwlk6  30814  indsumin  33253  elrgspnlem2  33629  vietadeg1  34034  eulerpartlemsv1  34813  eulerpartlemsf  34816  eulerpartlemgs2  34837  eulerpartlemn  34838  signsvfn  35036  fsum2dsub  35061  reprsuc  35069  hashreprin  35074  reprpmtf1o  35080  breprexplema  35084  breprexplemc  35086  breprexp  35087  breprexpnat  35088  vtsprod  35093  circlemeth  35094  circlemethnat  35095  circlevma  35096  circlemethhgt  35097  hgt750lemd  35102  hgt750lemb  35110  hgt750lema  35111  subfaclim  35719  fwddifnp1  36696  knoppndvlem6  37165  rrnmet  38540  3factsumint2  42849  3factsumint3  42850  lcmineqlem1  42856  lcmineqlem3  42858  lcmineqlem6  42861  sticksstones8  42980  sticksstones9  42981  sticksstones10  42982  sticksstones11  42983  sticksstones12a  42984  sticksstones12  42985  sticksstones17  42990  sticksstones18  42991  sticksstones19  42992  aks6d1c6lem1  42997  aks6d1c6lem3  42999  aks6d1c7lem3  43009  unitscyglem2  43023  sumcubes  43134  fltnltalem  43454  jm2.22  43782  jm2.23  43783  flcidc  43957  binomcxplemnn0  45119  binomcxplemdvsum  45125  binomcxplemnotnn0  45126  mccllem  46373  isumneg  46378  sumnnodd  46406  dvnmul  46717  dvnprodlem2  46721  dvnprodlem3  46722  stoweidlem37  46811  dirkertrigeqlem2  46873  dirkertrigeqlem3  46874  fourierdlem81  46961  fourierdlem83  46963  fourierdlem93  46973  fourierdlem103  46983  fourierdlem104  46984  elaa2lem  47007  etransclem23  47031  etransclem24  47032  etransclem31  47039  etransclem32  47040  etransclem35  47043  etransclem46  47054  rrxtopnfi  47061  rrndistlt  47064  sge0z  47149  sge0fsummpt  47164  sge0sup  47165  sge0resplit  47180  sge0split  47183  sge0ltfirpmpt2  47200  omeiunltfirp  47293  carageniuncllem2  47296  hoidmvlelem2  47370  hoidmvlelem3  47371  ppivalnn  48444  perfectALTVlem2  48547  nnsum3primesprm  48615  nnsum3primesgbe  48617  nnsum4primeseven  48625  altgsumbc  49191  altgsumbcALT  49192  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdig  49462  aacllem  50680  amgmwlem  50709