Theorem fn_on_from_function

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ A ⊆ dom f, hypo.
03. 1 ⊢ relation f, fn_is_rel 1.
04. 4 ⊢ x ∈ A, hypo.
05. 2, 4 ⊢ x ∈ dom f, incl_elim 2 4.
06. 2, 4 ⊢ ∃y. (x, y) ∈ f, dom_elim 5.
07. 7 ⊢ (x, y) ∈ f, hypo.
08. 7 ⊢ set (x, y), set_intro 7.
09. 7 ⊢ set y, setr_from_pair 8.
10. 7 ⊢ set y ∧ (x, y) ∈ f, conj_intro 9 7.
11. 7 ⊢ ∃y. set y ∧ (x, y) ∈ f, ex_intro 10.
12. 2, 4 ⊢ ∃y. set y ∧ (x, y) ∈ f, ex_elim 6 11.
13. 1 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, fn_unique_value 1.
14. 1 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 13.
15. 1 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 14.
16. 1, 2, 4 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, ex_uniq_set_intro 12 15.
17. 1, 2 ⊢ x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, subj_intro 16.
18. 1, 2 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_intro 17.
19. 1, 2 ⊢ fn_on f A, fn_on_intro 3 18.
fn_on_from_function. ⊢ function f → A ⊆ dom f → fn_on f A,
  subj_intro_ii 19.

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