Metamath Proof Explorer


Theorem ixpssmap

Description: An infinite Cartesian product is a subset of set exponentiation. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypothesis ixpssmap.2
|- B e. _V
Assertion ixpssmap
|- X_ x e. A B C_ ( U_ x e. A B ^m A )

Proof

Step Hyp Ref Expression
1 ixpssmap.2
 |-  B e. _V
2 1 rgenw
 |-  A. x e. A B e. _V
3 ixpssmapg
 |-  ( A. x e. A B e. _V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
4 2 3 ax-mp
 |-  X_ x e. A B C_ ( U_ x e. A B ^m A )