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\left(k\in A⟼B\right)\left(j\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}j\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$$