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 𝐴 ∈ V
mapsnen.2 𝐵 ∈ V
Assertion mapsnen ( 𝐴m { 𝐵 } ) ≈ 𝐴

Proof

Step Hyp Ref Expression
1 mapsnen.1 𝐴 ∈ V
2 mapsnen.2 𝐵 ∈ V
3 id ( 𝐴 ∈ V → 𝐴 ∈ V )
4 2 a1i ( 𝐴 ∈ V → 𝐵 ∈ V )
5 3 4 mapsnend ( 𝐴 ∈ V → ( 𝐴m { 𝐵 } ) ≈ 𝐴 )
6 1 5 ax-mp ( 𝐴m { 𝐵 } ) ≈ 𝐴