Theorem funcnv0

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

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

Proof

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