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 ^m B ) C_ ~P ( B X. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapsspm | |- ( A ^m B ) C_ ( A ^pm B ) |
|
| 2 | pmsspw | |- ( A ^pm B ) C_ ~P ( B X. A ) |
|
| 3 | 1 2 | sstri | |- ( A ^m B ) C_ ~P ( B X. A ) |