Theorem map_is_set_dom_cod

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ set X, hypo.
03. 3 ⊢ set Y, hypo.
04. 2, 3 ⊢ set (X × Y), set_prod 2 3.
05. 1 ⊢ f ⊆ X × Y, map_incl_in_prod 1.
06. 1, 2, 3 ⊢ set f, subset 5 4.
map_is_set_dom_cod. ⊢ map f X Y → set X → set Y → set f,
  subj_intro_iii 6.

Dependencies
The given proof depends on 10 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, power, subset, union.