ex_uniq_elimr

Theorem ex_uniq_elimr

Theorem. ex_uniq_elimr
(∃x. ∀y. x = y ↔ P y) → P x → P y → x = y

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

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