Description: The universal class is not equal to any setvar. (Contributed by NM, 4-Jul-2005) Extract from vnex and shorten proof. (Revised by BJ, 25-Apr-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vneqv | |- -. x = _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- y e. _V |
|
| 2 | eleq2 | |- ( x = _V -> ( y e. x <-> y e. _V ) ) |
|
| 3 | 1 2 | mpbiri | |- ( x = _V -> y e. x ) |
| 4 | 3 | con3i | |- ( -. y e. x -> -. x = _V ) |
| 5 | exnelv | |- E. y -. y e. x |
|
| 6 | 4 5 | exlimiiv | |- -. x = _V |