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 V
2 1 ne0ii V