Metamath Proof Explorer


Theorem rn0

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 ∅ = ∅

Proof

Step Hyp Ref Expression
1 dm0 dom ∅ = ∅
2 dm0rn0 ( dom ∅ = ∅ ↔ ran ∅ = ∅ )
3 1 2 mpbi ran ∅ = ∅