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 (/) = (/)