Theorem dom_restr_subclass

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ A ⊆ X, hypo.
03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
04. 1 ⊢ function f ∧ dom f = X, conj_eliml 3.
05. 1 ⊢ dom f = X, conj_elimr 4.
06. ⊢ dom (restr f A) = dom f ∩ A, dom_restr.
07. 1 ⊢ dom (restr f A) = X ∩ A, eq_subst 5 6,
  P u ↔ dom (restr f A) = u ∩ A.
08. 2 ⊢ A ∩ X = A, intersection_from_incl 2.
09. ⊢ A ∩ X = X ∩ A, intersection_comm.
10. 2 ⊢ X ∩ A = A, eq_subst 9 8, P u ↔ u = A.
08. 1, 2 ⊢ dom (restr f A) = A, eq_subst 10 7,
  P u ↔ dom (restr f A) = u.
dom_restr_subclass. ⊢ map f X Y → A ⊆ X →
  dom (restr f A) = A, subj_intro_ii 8.

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