Metamath Proof Explorer

Theorem 0nelfun

Description: A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021)

Ref Expression
Assertion 0nelfun 
|- ( Fun R -> (/) e/ R )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun R -> Rel R )
2 0nelrel 
 |-  ( Rel R -> (/) e/ R )
3 1 2 syl 
 |-  ( Fun R -> (/) e/ R )