Description: Obsolete proof of vnex as of 25-Apr-2026. (Contributed by NM, 4-Jul-2005) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vnexOLD | |- -. E. x x = _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nalset | |- -. E. x A. y y e. x |
|
| 2 | vex | |- y e. _V |
|
| 3 | 2 | tbt | |- ( y e. x <-> ( y e. x <-> y e. _V ) ) |
| 4 | 3 | albii | |- ( A. y y e. x <-> A. y ( y e. x <-> y e. _V ) ) |
| 5 | dfcleq | |- ( x = _V <-> A. y ( y e. x <-> y e. _V ) ) |
|
| 6 | 4 5 | bitr4i | |- ( A. y y e. x <-> x = _V ) |
| 7 | 6 | exbii | |- ( E. x A. y y e. x <-> E. x x = _V ) |
| 8 | 1 7 | mtbi | |- -. E. x x = _V |