Theorem ex_uniq_set_intro

Proof
01. 1 ⊢ ∃x. S x ∧ P x, hypo.
02. 2 ⊢ ∀x. ∀y. P x → P y → x = y, hypo.
03. 3 ⊢ S x ∧ P x, hypo.
04. 3 ⊢ S x, conj_eliml 3.
05. 3 ⊢ P x, conj_elimr 3.
06. 6 ⊢ x = y, hypo.
07. 3, 6 ⊢ P y, eq_subst 6 5.
08. 3 ⊢ x = y → P y, subj_intro 7.
09. 2 ⊢ ∀y. P x → P y → x = y, uq_elim 2.
10. 2 ⊢ P x → P y → x = y, uq_elim 9.
11. 2, 3 ⊢ P y → x = y, subj_elim 10 5.
12. 2, 3 ⊢ x = y ↔ P y, bij_intro 8 11.
13. 2, 3 ⊢ ∀y. x = y ↔ P y, uq_intro 12.
14. 2, 3 ⊢ S x ∧ ∀y. x = y ↔ P y, conj_intro 4 13.
15. 2, 3 ⊢ ∃x. S x ∧ ∀y. x = y ↔ P y, ex_intro 14.
16. 1, 2 ⊢ ∃x. S x ∧ ∀y. x = y ↔ P y, ex_elim 1 15.
ex_uniq_set_intro. ⊢ (∃x. S x ∧ P x) → (∀x. ∀y. P x → P y → x = y) →
  (∃x. S x ∧ ∀y. x = y ↔ P y), subj_intro_ii 16.

Dependencies
The given proof depends on one axiom:
eq_subst.