Theorem nrelv

Description: The universal class is not a relation. (Contributed by Thierry Arnoux, 23-Jan-2022) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	nrelv	$$⊢\neg \mathrm{Rel}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	notnoti	$$⊢\neg \neg \varnothing \in \mathrm{V}$$
3		0nelrel0	$$⊢\mathrm{Rel}\mathrm{V}\to \neg \varnothing \in \mathrm{V}$$
4	2 3	mto	$$⊢\neg \mathrm{Rel}\mathrm{V}$$