This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → ∅ ∉ R

Proof

Step Hyp Ref Expression
1 0nelrel0 ⊢ Rel ⁡ R → ¬ ∅ ∈ R
2 df-nel ⊢ ∅ ∉ R ↔ ¬ ∅ ∈ R
3 1 2 sylibr ⊢ Rel ⁡ R → ∅ ∉ R