Theorem esumex

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

	Ref	Expression
Assertion	esumex	|- sum* k e. A B e. _V

Proof

Step	Hyp	Ref	Expression
1		df-esum	|- sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
2		ovex	|- ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) e. _V
3	2	uniex	|- U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) e. _V
4	1 3	eqeltri	|- sum* k e. A B e. _V