ex_uniq_eliml

Theorem ex_uniq_eliml

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

Proof
01. 1 ⊢ ∃x. ∀y. x = y ↔ P y, hypo.
02. 2 ⊢ ∀y. x = y ↔ P y, hypo.
03. 2 ⊢ x = x ↔ P x, uq_elim 2.
04. 2 ⊢ x = x → P x, bij_eliml 3.
05. ⊢ x = x, eq_refl.
06. 2 ⊢ P x, subj_elim 4 5.
07. 2 ⊢ ∃x. P x, ex_intro 6.
08. 1 ⊢ ∃x. P x, ex_elim 1 7.
ex_uniq_eliml. ⊢ (∃x. ∀y. x = y ↔ P y) → (∃x. P x), subj_intro 8.

Dependencies
The given proof depends on one axiom:
eq_refl.