Theorem sg_eq_from_uniq

Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ ∀y. x = y ↔ P y, hypo.
03. 2 ⊢ x = y ↔ P y, uq_elim 2.
04. 4 ⊢ y ∈ {x}, hypo.
07. 1, 4 ⊢ y = x, sg_elim 1 4.
08. 1, 4 ⊢ x = y, eq_symm 7.
09. 1, 2, 4 ⊢ P y, lsubj_elim 3 8.
10. 1, 2, 4 ⊢ y ∈ {y | P y}, comp_intro_from 4 9.
11. 1, 2 ⊢ y ∈ {x} → y ∈ {y | P y}, subj_intro 10.
12. 12 ⊢ y ∈ {y | P y}, hypo.
13. 12 ⊢ P y, comp_elim 12.
14. 2, 12 ⊢ x = y, rsubj_elim 3 13.
15. 2, 12 ⊢ y = x, eq_symm 14.
16. 1, 2, 12 ⊢ y ∈ {x}, sg_intro 1 15.
17. 1, 2 ⊢ y ∈ {y | P y} → y ∈ {x}, subj_intro 16.
18. 1, 2 ⊢ y ∈ {x} ↔ y ∈ {y | P y}, bij_intro 11 17.
19. 1, 2 ⊢ ∀y. y ∈ {x} ↔ y ∈ {y | P y}, uq_intro 18.
20. 1, 2 ⊢ {x} = {y | P y}, ext 19.
sg_eq_from_uniq. ⊢ set x → (∀y. x = y ↔ P y) → {x} = {y | P y},
  subj_intro_ii 20.

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