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	$$⊢\mathrm{ran}\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
2		dm0rn0	$$⊢\mathrm{dom}\varnothing =\varnothing \leftrightarrow \mathrm{ran}\varnothing =\varnothing$$
3	1 2	mpbi	$$⊢\mathrm{ran}\varnothing =\varnothing$$