Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Proof shortened by AV, 17-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | map0.1 | |- A e. _V |
|
map0.2 | |- B e. _V |
||
Assertion | mapsn | |- ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | map0.1 | |- A e. _V |
|
2 | map0.2 | |- B e. _V |
|
3 | id | |- ( A e. _V -> A e. _V ) |
|
4 | 2 | a1i | |- ( A e. _V -> B e. _V ) |
5 | 3 4 | mapsnd | |- ( A e. _V -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } ) |
6 | 1 5 | ax-mp | |- ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } |