Theorem nfesum2

Description: Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020)

	Ref	Expression
Hypotheses	nfesum2.1	|- F/_ x A
	nfesum2.2	|- F/_ x B
Assertion	nfesum2	|- F/_ x sum* k e. A B

Proof

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