This is an old revision of the document!
Pre-image of the function $f$ w.r.t the codomain subset $Z$.
Mizar files: FUNCT_1
Wikipedia: Image
Set constructor
Function