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	$⊢ \sum_{k \in A} B = \sum_{k \in A} I (B)$

Proof

Step	Hyp	Ref	Expression
1		sumeq2ii	$⊢ \forall k \in A I (B) = I (I (B)) \to \sum_{k \in A} B = \sum_{k \in A} I (B)$
2		fvex	$⊢ I (B) \in V$
3		fvi	$⊢ I (B) \in V \to I (I (B)) = I (B)$
4	2 3	ax-mp	$⊢ I (I (B)) = I (B)$
5	4	eqcomi	$⊢ I (B) = I (I (B))$
6	5	a1i	$⊢ k \in A \to I (B) = I (I (B))$
7	1 6	mprg	$⊢ \sum_{k \in A} B = \sum_{k \in A} I (B)$