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