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