Metamath Proof Explorer


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