Description: Equality theorem for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | sumeq2 | ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | ⊢ ( 𝐵 = 𝐶 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) | |
2 | 1 | ralimi | ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) |
3 | sumeq2ii | ⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 ) | |
4 | 2 3 | syl | ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 ) |