Metamath Proof Explorer

Theorem 0nelrel

Description: A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021)

Ref Expression
Assertion 0nelrel 
|- ( Rel R -> (/) e/ R )

Proof

Step Hyp Ref Expression
1 0nelrel0 
 |-  ( Rel R -> -. (/) e. R )
2 df-nel 
 |-  ( (/) e/ R <-> -. (/) e. R )
3 1 2 sylibr 
 |-  ( Rel R -> (/) e/ R )