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 )