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	|- -. Rel _V

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2	1	notnoti	|- -. -. (/) e. _V
3		0nelrel0	|- ( Rel _V -> -. (/) e. _V )
4	2 3	mto	|- -. Rel _V