Theorem ixpconstg

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

	Ref	Expression
Assertion	ixpconstg	|- ( ( A e. V /\ B e. W ) -> X_ x e. A B = ( B ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- f e. _V
2	1	elixpconst	|- ( f e. X_ x e. A B <-> f : A --> B )
3	2	abbi2i	|- X_ x e. A B = { f | f : A --> B }
4		mapvalg	|- ( ( B e. W /\ A e. V ) -> ( B ^m A ) = { f | f : A --> B } )
5	3 4	eqtr4id	|- ( ( B e. W /\ A e. V ) -> X_ x e. A B = ( B ^m A ) )
6	5	ancoms	|- ( ( A e. V /\ B e. W ) -> X_ x e. A B = ( B ^m A ) )