Theorem fn_app_restr

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ x ∈ dom f, hypo.
03. 3 ⊢ x ∈ A, hypo.
05. 1, 2 ⊢ set (app f x), app_is_set 1 2.
06. 1, 2 ⊢ app f x ∈ UnivCl, UnivCl_intro 5.
07. 1, 2, 3 ⊢ (x, app f x) ∈ A × UnivCl, prod_intro 3 6.
08. ⊢ app f x = app f x, eq_refl.
09. 1, 2 ⊢ (x, app f x) ∈ f, app_elim 1 2 8.
10. 1, 2, 3 ⊢ (x, app f x) ∈ f ∩ (A × UnivCl), intersection_intro 9 7.
11. 1, 2, 3 ⊢ (x, app f x) ∈ restr f A, eq_subst_rev restr_eq 10,
  P u ↔ (x, app f x) ∈ u.
12. 1 ⊢ function (restr f A), restr_is_function 1.
13. 1, 2, 3 ⊢ app f x = app (restr f A) x, app_intro 12 11.
fn_app_restr. ⊢ function f → x ∈ dom f → x ∈ A → app f x = app (restr f A) x,
  subj_intro_iii 13.

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