Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ x ∈ {a}, hypo.
03. 2 ⊢ x ∈ {x | set a → x = a}, eq_subst sg_eq 2, P u ↔ x ∈ u.
04. 2 ⊢ set a → x = a, comp_elim 3.
05. 1, 2 ⊢ x = a, subj_elim 4 1.
06. 1 ⊢ x ∈ {a} → x = a, subj_intro 5.
sg_elim. ⊢ set a → x ∈ {a} → x = a, subj_intro 6.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.