Theorem dom_restr

Proof
01. 1 ⊢ x ∈ dom (restr f A), hypo.
02. 1 ⊢ ∃y. (x, y) ∈ restr f A, dom_elim 1.
03. 3 ⊢ (x, y) ∈ restr f A, hypo.
04. 3 ⊢ (x, y) ∈ f ∩ (A × UnivCl), eq_subst restr_eq 3, P u ↔ (x, y) ∈ u.
05. 3 ⊢ (x, y) ∈ f, intersection_eliml 4.
06. 3 ⊢ (x, y) ∈ A × UnivCl, intersection_elimr 4.
07. 3 ⊢ x ∈ A ∧ y ∈ UnivCl, prod_elim_pair 6.
08. 3 ⊢ x ∈ A, conj_eliml 7.
09. 3 ⊢ x ∈ dom f, dom_intro 5.
10. 3 ⊢ x ∈ dom f ∩ A, intersection_intro 9 8.
11. 1 ⊢ x ∈ dom f ∩ A, ex_elim 2 10.
12. ⊢ x ∈ dom (restr f A) → x ∈ dom f ∩ A, subj_intro 11.
13. 13 ⊢ x ∈ dom f ∩ A, hypo.
14. 13 ⊢ x ∈ dom f, intersection_eliml 13.
15. 13 ⊢ x ∈ A, intersection_elimr 13.
16. 13 ⊢ ∃y. (x, y) ∈ f, dom_elim 14.
17. 17 ⊢ (x, y) ∈ f, hypo.
18. 17 ⊢ set (x, y), set_intro 17.
19. 17 ⊢ set y, setr_from_pair 18.
20. 17 ⊢ y ∈ UnivCl, UnivCl_intro 19.
21. 13, 17 ⊢ (x, y) ∈ A × UnivCl, prod_intro 15 20.
22. 13, 17 ⊢ (x, y) ∈ f ∩ (A × UnivCl), intersection_intro 17 21.
23. 13, 17 ⊢ (x, y) ∈ restr f A, eq_subst_rev restr_eq 22, P u ↔ (x, y) ∈ u.
24. 13, 17 ⊢ x ∈ dom (restr f A), dom_intro 23.
25. 13 ⊢ x ∈ dom (restr f A), ex_elim 16 24.
26. ⊢ x ∈ dom f ∩ A → x ∈ dom (restr f A), subj_intro 25.
27. ⊢ x ∈ dom (restr f A) ↔ x ∈ dom f ∩ A, bij_intro 12 26.
28. ⊢ ∀x. x ∈ dom (restr f A) ↔ x ∈ dom f ∩ A, uq_intro 27.
dom_restr. ⊢ dom (restr f A) = dom f ∩ A, ext 28.

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