Theorem nrelv

Description: The universal class is not a relation. (Contributed by Thierry Arnoux, 23-Jan-2022)

	Ref	Expression
Assertion	nrelv	|- -. Rel _V

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		0nelxp	|- -. (/) e. ( _V X. _V )
3		nelss	|- ( ( (/) e. _V /\ -. (/) e. ( _V X. _V ) ) -> -. _V C_ ( _V X. _V ) )
4	1 2 3	mp2an	|- -. _V C_ ( _V X. _V )
5		df-rel	|- ( Rel _V <-> _V C_ ( _V X. _V ) )
6	4 5	mtbir	|- -. Rel _V