Metamath Proof Explorer


Theorem vn0ALT

Description: Alternate proof of vn0 . Shorter, but requiring df-clel , ax-8 . (Contributed by NM, 11-Sep-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vn0ALT V

Proof

Step Hyp Ref Expression
1 vex x V
2 1 ne0ii V