cnvsn0

Description: The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	cnvsn0	$⊢ {\{\emptyset\}}^{-1} = \emptyset$

Step	Hyp	Ref	Expression
1		dfdm4	$⊢ dom \{\emptyset\} = ran {\{\emptyset\}}^{-1}$
2		dmsn0	$⊢ dom \{\emptyset\} = \emptyset$
3	1 2	eqtr3i	$⊢ ran {\{\emptyset\}}^{-1} = \emptyset$
4		relcnv	$⊢ Rel {\{\emptyset\}}^{-1}$
5		relrn0	$⊢ Rel {\{\emptyset\}}^{-1} \to ({\{\emptyset\}}^{-1} = \emptyset \leftrightarrow ran {\{\emptyset\}}^{-1} = \emptyset)$
6	4 5	ax-mp	$⊢ {\{\emptyset\}}^{-1} = \emptyset \leftrightarrow ran {\{\emptyset\}}^{-1} = \emptyset$
7	3 6	mpbir	$⊢ {\{\emptyset\}}^{-1} = \emptyset$

Metamath Proof Explorer