Metamath Proof Explorer


Theorem mapsnen

Description: Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of Mendelson p. 255. (Contributed by NM, 17-Dec-2003) (Revised by Mario Carneiro, 15-Nov-2014) (Proof shortened by AV, 17-Jul-2022)

Ref Expression
Hypotheses mapsnen.1
|- A e. _V
mapsnen.2
|- B e. _V
Assertion mapsnen
|- ( A ^m { B } ) ~~ A

Proof

Step Hyp Ref Expression
1 mapsnen.1
 |-  A e. _V
2 mapsnen.2
 |-  B e. _V
3 id
 |-  ( A e. _V -> A e. _V )
4 2 a1i
 |-  ( A e. _V -> B e. _V )
5 3 4 mapsnend
 |-  ( A e. _V -> ( A ^m { B } ) ~~ A )
6 1 5 ax-mp
 |-  ( A ^m { B } ) ~~ A