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

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 → ¬ ∅ ∈ R

Proof

Step Hyp Ref Expression
1 df-rel ⊢ Rel ⁡ R ↔ R ⊆ V × V
2 1 biimpi ⊢ Rel ⁡ R → R ⊆ V × V
3 0nelxp ⊢ ¬ ∅ ∈ V × V
4 3 a1i ⊢ Rel ⁡ R → ¬ ∅ ∈ V × V
5 2 4 ssneldd ⊢ Rel ⁡ R → ¬ ∅ ∈ R