Theorem ex_uniq_set_elimr

Proof
01. 1 ⊢ ∃x. S x ∧ ∀y. x = y ↔ P y, hypo.
02. 2 ⊢ S u ∧ ∀y. u = y ↔ P y, hypo.
03. 2 ⊢ ∀y. u = y ↔ P y, conj_elimr 2.
04. 4 ⊢ P x, hypo.
05. 5 ⊢ P y, hypo.
06. 2 ⊢ u = x ↔ P x, uq_elim 3.
07. 2 ⊢ u = y ↔ P y, uq_elim 3.
08. 2 ⊢ P x → u = x, bij_elimr 6.
09. 2 ⊢ P y → u = y, bij_elimr 7.
10. 4, 2 ⊢ u = x, subj_elim 8 4.
11. 5, 2 ⊢ u = y, subj_elim 9 5.
12. 4, 2 ⊢ x = u, eq_symm 10.
13. 4, 5, 2 ⊢ x = y, eq_trans 12 11.
14. 1, 4, 5 ⊢ x = y, ex_elim 1 13.
ex_uniq_set_elimr. ⊢ (∃x. S x ∧ ∀y. x = y ↔ P y) → P x → P y → x = y,
  subj_intro_iii 14.

Dependencies
The given proof depends on two axioms:
eq_refl, eq_subst.