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 ∅ ∈ V
2 0nelxp ¬ ∅ ∈ ( V × V )
3 nelss ( ( ∅ ∈ V ∧ ¬ ∅ ∈ ( V × V ) ) → ¬ V ⊆ ( V × V ) )
4 1 2 3 mp2an ¬ V ⊆ ( V × V )
5 df-rel ( Rel V ↔ V ⊆ ( V × V ) )
6 4 5 mtbir ¬ Rel V