Theorem 0map0sn0

Description: The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024)

	Ref	Expression
Assertion	0map0sn0	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		f0bi	$$⊢f:\varnothing ⟶\varnothing \leftrightarrow f=\varnothing$$
2	1	abbii	$$⊢\left\{f|f:\varnothing ⟶\varnothing \right\}=\left\{f|f=\varnothing \right\}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3 3	mapval	$$⊢{\varnothing }^{\varnothing }=\left\{f|f:\varnothing ⟶\varnothing \right\}$$
5		df-sn	$$⊢\left\{\varnothing \right\}=\left\{f|f=\varnothing \right\}$$
6	2 4 5	3eqtr4i	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$