# Metamath Proof Explorer

## Theorem prodfc

Description: A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017)

Ref Expression
Assertion prodfc ${⊢}\prod _{{j}\in {A}}\left({k}\in {A}⟼{B}\right)\left({j}\right)=\prod _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
2 1 fvmpt2i ${⊢}{k}\in {A}\to \left({k}\in {A}⟼{B}\right)\left({k}\right)=\mathrm{I}\left({B}\right)$
3 2 prodeq2i ${⊢}\prod _{{k}\in {A}}\left({k}\in {A}⟼{B}\right)\left({k}\right)=\prod _{{k}\in {A}}\mathrm{I}\left({B}\right)$
4 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}\right)\left({j}\right)$
5 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}\right)\left({k}\right)$
6 fveq2 ${⊢}{j}={k}\to \left({k}\in {A}⟼{B}\right)\left({j}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)$
7 4 5 6 cbvprodi ${⊢}\prod _{{j}\in {A}}\left({k}\in {A}⟼{B}\right)\left({j}\right)=\prod _{{k}\in {A}}\left({k}\in {A}⟼{B}\right)\left({k}\right)$
8 prod2id ${⊢}\prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}\mathrm{I}\left({B}\right)$
9 3 7 8 3eqtr4i ${⊢}\prod _{{j}\in {A}}\left({k}\in {A}⟼{B}\right)\left({j}\right)=\prod _{{k}\in {A}}{B}$