Description: The domain of the empty set is empty. Part of Theorem 3.8(v) of Monk1 p. 36. (Contributed by NM, 4-Jul-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dm0 | |- dom (/) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel | |- -. <. x , y >. e. (/) |
|
| 2 | 1 | nex | |- -. E. y <. x , y >. e. (/) |
| 3 | vex | |- x e. _V |
|
| 4 | 3 | eldm2 | |- ( x e. dom (/) <-> E. y <. x , y >. e. (/) ) |
| 5 | 2 4 | mtbir | |- -. x e. dom (/) |
| 6 | 5 | nel0 | |- dom (/) = (/) |