Metamath Proof Explorer

Theorem mapsspw

Description: Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion mapsspw A B 𝒫 B × A


Step Hyp Ref Expression
1 mapsspm A B A 𝑝𝑚 B
2 pmsspw A 𝑝𝑚 B 𝒫 B × A
3 1 2 sstri A B 𝒫 B × A