DEF-IM. Image.
Let $R$ be a binary relation. If $A\subseteq\operatorname{dom}R$, the image of $A$ under $R$ is
\[R[A] = \operatorname{ran}{R\restriction_A} = \{y\in\operatorname{ran}R:(\exists x\in A:x\,R\,y)\}.\]If $B\subseteq\operatorname{ran}R$, the inverse image / preimage of $B$ under $R$ is $R^{-1}[B]$.
PROP-RIM-EMP.
For any binary relation $R$,
\[R[\varnothing] = \varnothing.\]