Metamath Proof Explorer

Theorem 0nelrel0

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

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

Proof

Step Hyp Ref Expression
1 df-rel 
 |-  ( Rel R <-> R C_ ( _V X. _V ) )
2 1 biimpi 
 |-  ( Rel R -> R C_ ( _V X. _V ) )
3 0nelxp 
 |-  -. (/) e. ( _V X. _V )
4 3 a1i 
 |-  ( Rel R -> -. (/) e. ( _V X. _V ) )
5 2 4 ssneldd 
 |-  ( Rel R -> -. (/) e. R )