Theorem prodsns

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

	Ref	Expression
Assertion	prodsns	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ n A
2		nfcsb1v	|- F/_ k [_ n / k ]_ A
3		csbeq1a	|- ( k = n -> A = [_ n / k ]_ A )
4	1 2 3	cbvprodi	|- prod_ k e. { M } A = prod_ n e. { M } [_ n / k ]_ A
5		csbeq1	|- ( n = M -> [_ n / k ]_ A = [_ M / k ]_ A )
6	5	prodsn	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ n e. { M } [_ n / k ]_ A = [_ M / k ]_ A )
7	4 6	eqtrid	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )