Theorem function_is_set

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ set (dom f), hypo.
03. 1, 2 ⊢ set (rng f), substitution 1 2.
04. 1 ⊢ relation f, fn_is_rel 1.
05. ⊢ dom f ⊆ dom f, incl_refl.
06. ⊢ rng f ⊆ rng f, incl_refl.
07. 1 ⊢ f ⊆ dom f × rng f, relation_incl_prod 4 5 6.
08. 1, 2 ⊢ set (dom f × rng f), set_prod 2 3.
09. 1, 2 ⊢ set f, subset 7 8.
function_is_set. ⊢ function f → set (dom f) → set f, subj_intro_ii 9.

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