Theorem ixpconst

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

	Ref	Expression
Hypotheses	ixpconst.1	|- A e. _V
	ixpconst.2	|- B e. _V
Assertion	ixpconst	|- X_ x e. A B = ( B ^m A )

Proof

Step	Hyp	Ref	Expression
1		ixpconst.1	|- A e. _V
2		ixpconst.2	|- B e. _V
3		ixpconstg	|- ( ( A e. _V /\ B e. _V ) -> X_ x e. A B = ( B ^m A ) )
4	1 2 3	mp2an	|- X_ x e. A B = ( B ^m A )