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 𝑅 → ∅ ∉ 𝑅 )

Proof

Step Hyp Ref Expression
1 0nelrel0 ( Rel 𝑅 → ¬ ∅ ∈ 𝑅 )
2 df-nel ( ∅ ∉ 𝑅 ↔ ¬ ∅ ∈ 𝑅 )
3 1 2 sylibr ( Rel 𝑅 → ∅ ∉ 𝑅 )