Metamath Proof Explorer

Theorem prod2id

Description: The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017)

		Ref	Expression
	Assertion	prod2id	$⊢ \prod_{k \in A} B = \prod_{k \in A} I (B)$

Step	Hyp	Ref	Expression
1		prodeq2ii	$⊢ \forall k \in A I (B) = I (I (B)) \to \prod_{k \in A} B = \prod_{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	$⊢ \prod_{k \in A} B = \prod_{k \in A} I (B)$