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 =/= (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | ne0ii | |- _V =/= (/) |