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 
|- -. _V e. A

Proof

Step Hyp Ref Expression
1 vprc 
 |-  -. _V e. _V
2 elex 
 |-  ( _V e. A -> _V e. _V )
3 1 2 mto 
 |-  -. _V e. A