Description: The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o ). (Contributed by BJ, 6-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-0nelsngl | |- (/) e/ sngl A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | snnz | |- { x } =/= (/) |
| 3 | 2 | nesymi | |- -. (/) = { x } |
| 4 | 3 | nex | |- -. E. x (/) = { x } |
| 5 | bj-elsngl | |- ( (/) e. sngl A <-> E. x e. A (/) = { x } ) |
|
| 6 | rexex | |- ( E. x e. A (/) = { x } -> E. x (/) = { x } ) |
|
| 7 | 5 6 | sylbi | |- ( (/) e. sngl A -> E. x (/) = { x } ) |
| 8 | 4 7 | mto | |- -. (/) e. sngl A |
| 9 | 8 | nelir | |- (/) e/ sngl A |