Image
Set
context
$ R\in \text{Rel}(X,Y) $
postulate
$ y\in \mathrm{im}(R) $
postulate
$ \exists x\ (\langle x,y \rangle \in R) $
Ramifications
Reference
Mizar files:
RELAT_1
Wikipedia:
Image
Parents
Context
Binary relation