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 =