Theorem sg_eq_from_ex_uniq

Proof
01. 1 ⊢ ∃b. set b ∧ ∀y. b = y ↔ P y, hypo.
02. 2 ⊢ set b ∧ ∀y. b = y ↔ P y, hypo.
03. 2 ⊢ set b, conj_eliml 2.
04. 2 ⊢ ∀y. b = y ↔ P y, conj_elimr 2.
05. 2 ⊢ {b} = {y | P y}, sg_eq_from_uniq 3 4.
06. 2 ⊢ set b ∧ {b} = {y | P y}, conj_intro 3 5.
07. 2 ⊢ ∃b. set b ∧ {b} = {y | P y}, ex_intro 6.
08. 1 ⊢ ∃b. set b ∧ {b} = {y | P y}, ex_elim 1 7.
sg_eq_from_ex_uniq. ⊢ (∃b. set b ∧ ∀y. b = y ↔ P y) →
  (∃b. set b ∧ {b} = {y | P y}), subj_intro 8.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.