Theorem map0e

Description: Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of Mendelson p. 255. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 14-Jul-2022)

	Ref	Expression
Assertion	map0e	$$⊢A\in V\to A^{\varnothing }=1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		mapdm0	$$⊢A\in V\to A^{\varnothing }=\left\{\varnothing \right\}$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3	1 2	eqtr4di	$$⊢A\in V\to A^{\varnothing }=1_{𝑜}$$