Theorem ex_uniq_from_mixed_form

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

Dependencies
The given proof depends on one axiom:
eq_subst.