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