Metamath Proof Explorer


Theorem nvel

Description: The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006)

Ref Expression
Assertion nvel ¬VA

Proof

Step Hyp Ref Expression
1 vprc ¬VV
2 elex VAVV
3 1 2 mto ¬VA