Theorem 0nelrel

Description: A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021)

	Ref	Expression
Assertion	0nelrel	$$⊢\mathrm{Rel}R\to \varnothing \notin R$$

Proof

Step	Hyp	Ref	Expression
1		0nelrel0	$$⊢\mathrm{Rel}R\to \neg \varnothing \in R$$
2		df-nel	$$⊢\varnothing \notin R\leftrightarrow \neg \varnothing \in R$$
3	1 2	sylibr	$$⊢\mathrm{Rel}R\to \varnothing \notin R$$