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

Metamath Proof Explorer

Theorem funcnv0

Description: The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021)

		Ref	Expression
	Assertion	funcnv0	$⊢ Fun \emptyset^{-1}$

Step	Hyp	Ref	Expression
1		fun0	$⊢ Fun \emptyset$
2		cnv0	$⊢ \emptyset^{-1} = \emptyset$
3	2	funeqi	$⊢ Fun \emptyset^{-1} \leftrightarrow Fun \emptyset$
4	1 3	mpbir	$⊢ Fun \emptyset^{-1}$