Metamath Proof Explorer


Theorem sum2id

Description: The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion sum2id Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 ( I ‘ 𝐵 )

Proof

Step Hyp Ref Expression
1 sumeq2ii ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 ( I ‘ 𝐵 ) )
2 fvex ( I ‘ 𝐵 ) ∈ V
3 fvi ( ( I ‘ 𝐵 ) ∈ V → ( I ‘ ( I ‘ 𝐵 ) ) = ( I ‘ 𝐵 ) )
4 2 3 ax-mp ( I ‘ ( I ‘ 𝐵 ) ) = ( I ‘ 𝐵 )
5 4 eqcomi ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) )
6 5 a1i ( 𝑘𝐴 → ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) ) )
7 1 6 mprg Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 ( I ‘ 𝐵 )