Definition map_equi

Definition. map_equi
map f X Y ↔ function f ∧ dom f = X ∧ rng f ⊆ Y

A function f is called a mapping or map from X to Y if its domain is X and its range is a subclass of Y.