Theorem function_from_fn_on

Proof
01. 1 ⊢ fn_on f X, hypo.
02. 2 ⊢ dom f ⊆ X, hypo.
03. 1 ⊢ ∀x. x ∈ X → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f,
  ex_uniq_from_fn_on 1.
04. 4 ⊢ (x, y1) ∈ f, hypo.
05. 4 ⊢ x ∈ dom f, dom_intro 4.
06. 2, 4 ⊢ x ∈ X, incl_elim 2 5.
07. 1, 2, 4 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_bounded_elim 3 6.
08. 1, 2, 4 ⊢ (x, y2) ∈ f → y1 = y2, ex_uniq_set_elimr 7 4.
09. 1, 2 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, subj_intro 8.
10. 1, 2 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 9.
11. 1, 2 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 10.
12. 1, 2 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 11.
13. 1 ⊢ relation f, relation_from_fn_on 1.
14. 1, 2 ⊢ function f, function_intro 13 12.
function_from_fn_on. ⊢ fn_on f X → dom f ⊆ X → function f,
  subj_intro_ii 14.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.