Description: A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fsum1.1 | ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 ) | |
Assertion | sumsn | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsum1.1 | ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 ) | |
2 | nfcv | ⊢ Ⅎ 𝑘 𝐵 | |
3 | 2 1 | sumsnf | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 ) |