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

Metamath Proof Explorer

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	$⊢ \emptyset^{\emptyset} = \{\emptyset\}$

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