Theorem ixpconstg

Description: Infinite Cartesian product of a constant B . (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Assertion	ixpconstg	$$⊢\left(A\in V\wedge B\in W\right)\to \underset{x\in A}{⨉}B=B^A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢f\in \mathrm{V}$$
2	1	elixpconst	$$⊢f\in \underset{x\in A}{⨉}B\leftrightarrow f:A⟶B$$
3	2	eqabi	$$⊢\underset{x\in A}{⨉}B=\left\{f|f:A⟶B\right\}$$
4		mapvalg	$$⊢\left(B\in W\wedge A\in V\right)\to B^A=\left\{f|f:A⟶B\right\}$$
5	3 4	eqtr4id	$$⊢\left(B\in W\wedge A\in V\right)\to \underset{x\in A}{⨉}B=B^A$$
6	5	ancoms	$$⊢\left(A\in V\wedge B\in W\right)\to \underset{x\in A}{⨉}B=B^A$$