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	$$⊢\mathrm{Rel}R\to \neg \varnothing \in R$$

Proof

Step	Hyp	Ref	Expression
1		df-rel	$$⊢\mathrm{Rel}R\leftrightarrow R\subseteq \mathrm{V}\times \mathrm{V}$$
2	1	biimpi	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{V}\times \mathrm{V}$$
3		0nelxp	$$⊢\neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
4	3	a1i	$$⊢\mathrm{Rel}R\to \neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
5	2 4	ssneldd	$$⊢\mathrm{Rel}R\to \neg \varnothing \in R$$