Theorem prodsns

Description: A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017)

	Ref	Expression
Assertion	prodsns	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \prod _{k\in \left\{M\right\}}A=⦋M/k⦌A$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}nA$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋n/k⦌A$$
3		csbeq1a	$$⊢k=n\to A=⦋n/k⦌A$$
4	1 2 3	cbvprodi	$$⊢\prod _{k\in \left\{M\right\}}A=\prod _{n\in \left\{M\right\}}⦋n/k⦌A$$
5		csbeq1	$$⊢n=M\to ⦋n/k⦌A=⦋M/k⦌A$$
6	5	prodsn	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \prod _{n\in \left\{M\right\}}⦋n/k⦌A=⦋M/k⦌A$$
7	4 6	eqtrid	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \prod _{k\in \left\{M\right\}}A=⦋M/k⦌A$$