Theorem ex_uniq_intro

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

Dependencies
The given proof depends on one axiom:
eq_subst.