Theorem subclass_dom_from_ex_uniq

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

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