Metamath Proof Explorer

Theorem ima0

Description: Image of the empty set. Theorem 3.16(ii) of Monk1 p. 38. (Contributed by NM, 20-May-1998)

Ref Expression
Assertion ima0 
|- ( A " (/) ) = (/)

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( A " (/) ) = ran ( A |` (/) )
2 res0 
 |-  ( A |` (/) ) = (/)
3 2 rneqi 
 |-  ran ( A |` (/) ) = ran (/)
4 rn0 
 |-  ran (/) = (/)
5 1 3 4 3eqtri 
 |-  ( A " (/) ) = (/)