Metamath Proof Explorer


Theorem mapsn

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 >. } }

Proof

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 >. } }