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 V
map0.2 B V
Assertion mapsn A B = f | y A f = B y

Proof

Step Hyp Ref Expression
1 map0.1 A V
2 map0.2 B V
3 id A V A V
4 2 a1i A V B V
5 3 4 mapsnd A V A B = f | y A f = B y
6 1 5 ax-mp A B = f | y A f = B y