Theorem ex_uniq_from_mixed_form

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

Dependencies
The given proof depends on one axiom:
eq_subst.