Metamath Proof Explorer

Theorem mapdm0

Description: The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020) (Proof shortened by Thierry Arnoux, 3-Dec-2021)

		Ref	Expression
	Assertion	mapdm0	$⊢ B \in V \to B^{\emptyset} = \{\emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		elmapg	$⊢ (B \in V \land \emptyset \in V) \to (f \in (B^{\emptyset}) \leftrightarrow f : \emptyset ⟶ B)$
3	1 2	mpan2	$⊢ B \in V \to (f \in (B^{\emptyset}) \leftrightarrow f : \emptyset ⟶ B)$
4		f0bi	$⊢ f : \emptyset ⟶ B \leftrightarrow f = \emptyset$
5	3 4	bitrdi	$⊢ B \in V \to (f \in (B^{\emptyset}) \leftrightarrow f = \emptyset)$
6		velsn	$⊢ f \in \{\emptyset\} \leftrightarrow f = \emptyset$
7	5 6	bitr4di	$⊢ B \in V \to (f \in (B^{\emptyset}) \leftrightarrow f \in \{\emptyset\})$
8	7	eqrdv	$⊢ B \in V \to B^{\emptyset} = \{\emptyset\}$