Description: Obsolete version of abn0 as of 30-Aug-2024. (Contributed by NM, 26-Dec-1996) (Proof shortened by Mario Carneiro, 11-Nov-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | abn0OLD | |- ( { x | ph } =/= (/) <-> E. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfab1 | |- F/_ x { x | ph } |
|
| 2 | 1 | n0f | |- ( { x | ph } =/= (/) <-> E. x x e. { x | ph } ) |
| 3 | abid | |- ( x e. { x | ph } <-> ph ) |
|
| 4 | 3 | exbii | |- ( E. x x e. { x | ph } <-> E. x ph ) |
| 5 | 2 4 | bitri | |- ( { x | ph } =/= (/) <-> E. x ph ) |