# 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}}\mathrm{I}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 prodeq2ii ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left(\mathrm{I}\left({B}\right)\right)\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}\mathrm{I}\left({B}\right)$
2 fvex ${⊢}\mathrm{I}\left({B}\right)\in \mathrm{V}$
3 fvi ${⊢}\mathrm{I}\left({B}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{I}\left({B}\right)\right)=\mathrm{I}\left({B}\right)$
4 2 3 ax-mp ${⊢}\mathrm{I}\left(\mathrm{I}\left({B}\right)\right)=\mathrm{I}\left({B}\right)$
5 4 eqcomi ${⊢}\mathrm{I}\left({B}\right)=\mathrm{I}\left(\mathrm{I}\left({B}\right)\right)$
6 5 a1i ${⊢}{k}\in {A}\to \mathrm{I}\left({B}\right)=\mathrm{I}\left(\mathrm{I}\left({B}\right)\right)$
7 1 6 mprg ${⊢}\prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}\mathrm{I}\left({B}\right)$