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 𝐵 ∈ V
Assertion ixpssmap X 𝑥𝐴 𝐵 ⊆ ( 𝑥𝐴 𝐵m 𝐴 )

Proof

Step Hyp Ref Expression
1 ixpssmap.2 𝐵 ∈ V
2 1 rgenw 𝑥𝐴 𝐵 ∈ V
3 ixpssmapg ( ∀ 𝑥𝐴 𝐵 ∈ V → X 𝑥𝐴 𝐵 ⊆ ( 𝑥𝐴 𝐵m 𝐴 ) )
4 2 3 ax-mp X 𝑥𝐴 𝐵 ⊆ ( 𝑥𝐴 𝐵m 𝐴 )