Metamath Proof Explorer

Theorem vn0

Description: The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008)

Ref Expression
Assertion vn0 
|- _V =/= (/)

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 ne0ii 
 |-  _V =/= (/)