Description: The range of the empty set is empty. Part of Theorem 3.8(v) of Monk1 p. 36. (Contributed by NM, 4Jul1994)
Ref  Expression  

Assertion  rn0   ran (/) = (/) 
Step  Hyp  Ref  Expression 

1  dm0   dom (/) = (/) 

2  dm0rn0   ( dom (/) = (/) <> ran (/) = (/) ) 

3  1 2  mpbi   ran (/) = (/) 