Description: The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0ncn | |- -. (/) e. CC |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0nelxp | |- -. (/) e. ( R. X. R. ) |
|
| 2 | df-c | |- CC = ( R. X. R. ) |
|
| 3 | 2 | eleq2i | |- ( (/) e. CC <-> (/) e. ( R. X. R. ) ) |
| 4 | 1 3 | mtbir | |- -. (/) e. CC |