Theorem subclass_dom_from_ex_uniq

Proof
01. 1 ⊢ ∀x. x ∈ X → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 1, 2 ⊢ ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_bounded_elim 1 2.
04. 4 ⊢ z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f, hypo.
05. 4 ⊢ z ∈ Y, conj_eliml 4.
06. 4 ⊢ ∀y. z = y ↔ (x, y) ∈ f, conj_elimr 4.
07. 4 ⊢ z = z ↔ (x, z) ∈ f, uq_elim 6.
08. ⊢ z = z, eq_refl.
09. 4 ⊢ (x, z) ∈ f, lsubj_elim 7 8.
10. 4 ⊢ x ∈ dom f, dom_intro 9.
11. 1, 2 ⊢ x ∈ dom f, ex_elim 3 10.
12. 1 ⊢ x ∈ X → x ∈ dom f, subj_intro 11.
13. 1 ⊢ ∀x. x ∈ X → x ∈ dom f, uq_intro 12.
14. 1 ⊢ X ⊆ dom f, incl_intro 13.
subclass_dom_from_ex_uniq. ⊢
  (∀x. x ∈ X → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f) →
  X ⊆ dom f, subj_intro 14.

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