Theorem fn_on_char

Proof
01. 1 ⊢ fn_on f A, hypo.
02. 1 ⊢ relation f, relation_from_fn_on 1.
03. ⊢ restr f A ⊆ f, restr_is_subclass.
04. 1 ⊢ relation (restr f A), relation_subclass 3 2.
05. 5 ⊢ (x, y1) ∈ (restr f A), hypo.
06. 6 ⊢ (x, y2) ∈ (restr f A), hypo.
07. 5 ⊢ (x, y1) ∈ f, incl_elim 3 5.
08. 6 ⊢ (x, y2) ∈ f, incl_elim 3 6.
09. 5 ⊢ x ∈ dom (restr f A), dom_intro 5.
10. ⊢ dom (restr f A) = dom f ∩ A, dom_restr.
11. 5 ⊢ x ∈ dom f ∩ A, eq_subst 10 9, P u ↔ x ∈ u.
12. 5 ⊢ x ∈ A, intersection_elimr 11.
13. 1 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f,
  ex_uniq_from_fn_on 1.
14. 1, 5 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_bounded_elim 13 12.
15. 1, 5, 6 ⊢ y1 = y2, ex_uniq_set_elimr 14 7 8.
16. 1 ⊢ (x, y1) ∈ (restr f A) → (x, y2) ∈ (restr f A) →
  y1 = y2, subj_intro_ii 15.
17. 1 ⊢ ∀y2. (x, y1) ∈ (restr f A) → (x, y2) ∈ (restr f A) →
  y1 = y2, uq_intro 16.
18. 1 ⊢ ∀y1. ∀y2. (x, y1) ∈ (restr f A) → (x, y2) ∈ (restr f A) →
  y1 = y2, uq_intro 17.
19. 1 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ (restr f A) → (x, y2) ∈ (restr f A) →
  y1 = y2, uq_intro 18.
20. 1 ⊢ function (restr f A), function_intro 4 19.
21. 1 ⊢ relation f ∧ function (restr f A), conj_intro 2 20.
22. ⊢ fn_on f A → relation f ∧ function (restr f A), subj_intro 21.
23. 23 ⊢ relation f ∧ function (restr f A), hypo.
24. 23 ⊢ relation f, conj_eliml 23.
25. 23 ⊢ function (restr f A), conj_elimr 23.
26. 26 ⊢ x ∈ A, hypo.
27. 27 ⊢ (x, y1) ∈ f, hypo.
28. 28 ⊢ (x, y2) ∈ f, hypo.
29. 26, 27 ⊢ (x, y1) ∈ restr f A, restr_intro 27 26.
30. 26, 28 ⊢ (x, y2) ∈ restr f A, restr_intro 28 26.
31. 23, 26, 27, 28 ⊢ y1 = y2, fn_unique_value 25 29 30.
32. 23, 26 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, subj_intro_ii 31.
33. 23, 26 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 32.
34. 23, 26 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 33.
35. 35 ⊢ A ⊆ dom f, hypo.
36. 35, 26 ⊢ x ∈ dom f, incl_elim 35 26.
37. 35, 26 ⊢ ∃y. (x, y) ∈ f, dom_elim 36.
38. 38 ⊢ (x, y) ∈ f, hypo.
39. 38 ⊢ set (x, y), set_intro 38.
40. 38 ⊢ set y, setr_from_pair 39.
41. 38 ⊢ set y ∧ (x, y) ∈ f, conj_intro 40 38.
42. 38 ⊢ ∃y. set y ∧ (x, y) ∈ f, ex_intro 41.
43. 35, 26 ⊢ ∃y. set y ∧ (x, y) ∈ f, ex_elim 37 42.
44. 35, 23, 26 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f,
  ex_uniq_set_intro 43 34.
45. 35, 23 ⊢ x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, subj_intro 44.
46. 35, 23 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_intro 45.
47. 35, 23 ⊢ fn_on f A, fn_on_intro 24 46.
48. 35 ⊢ relation f ∧ function (restr f A) → fn_on f A, subj_intro 47.
49. 35 ⊢ fn_on f A ↔ relation f ∧ function (restr f A), bij_intro 22 48.
fn_on_char. ⊢ A ⊆ dom f →
  (fn_on f A ↔ relation f ∧ function (restr f A)), subj_intro 49.

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