Theorem ixpconst

Description: Infinite Cartesian product of a constant B . (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Hypotheses	ixpconst.1	$$⊢A\in \mathrm{V}$$
	ixpconst.2	$$⊢B\in \mathrm{V}$$
Assertion	ixpconst	$$⊢\underset{x\in A}{⨉}B=B^A$$

Proof

Step	Hyp	Ref	Expression
1		ixpconst.1	$$⊢A\in \mathrm{V}$$
2		ixpconst.2	$$⊢B\in \mathrm{V}$$
3		ixpconstg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \underset{x\in A}{⨉}B=B^A$$
4	1 2 3	mp2an	$$⊢\underset{x\in A}{⨉}B=B^A$$