Description: The range of the empty set is empty. Part of Theorem 3.8(v) of Monk1 p. 36. (Contributed by NM, 4-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | rn0 | ⊢ ran ∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dm0 | ⊢ dom ∅ = ∅ | |
2 | dm0rn0 | ⊢ ( dom ∅ = ∅ ↔ ran ∅ = ∅ ) | |
3 | 1 2 | mpbi | ⊢ ran ∅ = ∅ |