This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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