Metamath Proof Explorer


Theorem esumex

Description: An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017)

Ref Expression
Assertion esumex *kABV

Proof

Step Hyp Ref Expression
1 df-esum *kAB=𝑠*𝑠0+∞tsumskAB
2 ovex 𝑠*𝑠0+∞tsumskABV
3 2 uniex 𝑠*𝑠0+∞tsumskABV
4 1 3 eqeltri *kABV