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 `' (/)

Proof

Step Hyp Ref Expression
1 fun0 
 |-  Fun (/)
2 cnv0 
 |-  `' (/) = (/)
3 2 funeqi 
 |-  ( Fun `' (/) <-> Fun (/) )
4 1 3 mpbir 
 |-  Fun `' (/)