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\in \mathrm{V}$$
	mapsnen.2	$$⊢B\in \mathrm{V}$$
Assertion	mapsnen	$$⊢\left(A^{\left\{B\right\}}\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		mapsnen.1	$$⊢A\in \mathrm{V}$$
2		mapsnen.2	$$⊢B\in \mathrm{V}$$
3		id	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
4	2	a1i	$$⊢A\in \mathrm{V}\to B\in \mathrm{V}$$
5	3 4	mapsnend	$$⊢A\in \mathrm{V}\to \left(A^{\left\{B\right\}}\right)\approx A$$
6	1 5	ax-mp	$$⊢\left(A^{\left\{B\right\}}\right)\approx A$$