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\in \mathrm{V}$$
	map0.2	$$⊢B\in \mathrm{V}$$
Assertion	mapsn	$$⊢A^{\left\{B\right\}}=\left\{f|\exists y\in Af=\left\{⟨B,y⟩\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		map0.1	$$⊢A\in \mathrm{V}$$
2		map0.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	mapsnd	$$⊢A\in \mathrm{V}\to A^{\left\{B\right\}}=\left\{f|\exists y\in Af=\left\{⟨B,y⟩\right\}\right\}$$
6	1 5	ax-mp	$$⊢A^{\left\{B\right\}}=\left\{f|\exists y\in Af=\left\{⟨B,y⟩\right\}\right\}$$