Theorem funcnv0

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

	Ref	Expression
Assertion	funcnv0	⊢ Fun ◡ ∅

Proof

Step	Hyp	Ref	Expression
1		fun0	⊢ Fun ∅
2		cnv0	⊢ ◡ ∅ = ∅
3	2	funeqi	⊢ ( Fun ◡ ∅ ↔ Fun ∅ )
4	1 3	mpbir	⊢ Fun ◡ ∅