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} (k \in A ⟼ B) (j) = \prod_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
2	1	fvmpt2i	$⊢ k \in A \to (k \in A ⟼ B) (k) = I (B)$
3	2	prodeq2i	$⊢ \prod_{k \in A} (k \in A ⟼ B) (k) = \prod_{k \in A} I (B)$
4		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (j)$
5		nfcv	$⊢ \underline{Ⅎ} j (k \in A ⟼ B) (k)$
6		fveq2	$⊢ j = k \to (k \in A ⟼ B) (j) = (k \in A ⟼ B) (k)$
7	4 5 6	cbvprodi	$⊢ \prod_{j \in A} (k \in A ⟼ B) (j) = \prod_{k \in A} (k \in A ⟼ B) (k)$
8		prod2id	$⊢ \prod_{k \in A} B = \prod_{k \in A} I (B)$
9	3 7 8	3eqtr4i	$⊢ \prod_{j \in A} (k \in A ⟼ B) (j) = \prod_{k \in A} B$