Metamath Proof Explorer


Theorem nfesum1

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

Ref Expression
Hypothesis nfesum1.1 𝑘 𝐴
Assertion nfesum1 𝑘 Σ* 𝑘𝐴 𝐵

Proof

Step Hyp Ref Expression
1 nfesum1.1 𝑘 𝐴
2 df-esum Σ* 𝑘𝐴 𝐵 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) )
3 nfcv 𝑘 ( ℝ*𝑠s ( 0 [,] +∞ ) )
4 nfcv 𝑘 tsums
5 nfmpt1 𝑘 ( 𝑘𝐴𝐵 )
6 3 4 5 nfov 𝑘 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) )
7 6 nfuni 𝑘 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) )
8 2 7 nfcxfr 𝑘 Σ* 𝑘𝐴 𝐵