This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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