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

Proof

Step Hyp Ref Expression
1 df-rel ( Rel 𝑅𝑅 ⊆ ( V × V ) )
2 1 biimpi ( Rel 𝑅𝑅 ⊆ ( V × V ) )
3 0nelxp ¬ ∅ ∈ ( V × V )
4 3 a1i ( Rel 𝑅 → ¬ ∅ ∈ ( V × V ) )
5 2 4 ssneldd ( Rel 𝑅 → ¬ ∅ ∈ 𝑅 )