Theorem nfesum1

Description: Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017)

	Ref	Expression
Hypothesis	nfesum1.1	|- F/_ k A
Assertion	nfesum1	|- F/_ k sum* k e. A B

Proof

Step	Hyp	Ref	Expression
1		nfesum1.1	|- F/_ k A
2		df-esum	|- sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
3		nfcv	|- F/_ k ( RR*s |`s ( 0 [,] +oo ) )
4		nfcv	|- F/_ k tsums
5		nfmpt1	|- F/_ k ( k e. A |-> B )
6	3 4 5	nfov	|- F/_ k ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
7	6	nfuni	|- F/_ k U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
8	2 7	nfcxfr	|- F/_ k sum* k e. A B