Description: Obsolete version of neq0 as of 28-Jun-2024. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | neq0OLD | |- ( -. A = (/) <-> E. x x e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv | |- F/_ x A |
|
| 2 | 1 | neq0f | |- ( -. A = (/) <-> E. x x e. A ) |