Theorem app_restr

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ A ⊆ X, hypo.
03. 3 ⊢ x ∈ A, hypo.
04. 2, 3 ⊢ x ∈ X, incl_elim 2 3.
05. 1, 2, 3 ⊢ set (app f x), map_app_is_set 1 4.
06. 1, 2, 3 ⊢ 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, 3 ⊢ (x, app f x) ∈ f, map_app_elim 1 4 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, 2 ⊢ map (restr f A) A Y, map_restr 1 2.
13. 1, 2, 3 ⊢ app f x = app (restr f A) x, map_app_intro 12 11.
app_restr. ⊢ map f X Y → A ⊆ X → 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.