Theorem map_unfold

Theorem. map_unfold
map f X Y → function f ∧ dom f = X ∧ rng f ⊆ Y
Proof
map_unfold. ⊢ map f X Y → function f ∧ dom f = X ∧ rng f ⊆ Y,
  bij_eliml map_equi.