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	⊢ ∅ ∈ V
2	1	notnoti	⊢ ¬ ¬ ∅ ∈ V
3		0nelrel0	⊢ ( Rel V → ¬ ∅ ∈ V )
4	2 3	mto	⊢ ¬ Rel V