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.
07. 7 ⊢ set a, hypo.
08. 8 ⊢ x = a, hypo.
09. 7, 8 ⊢ set x, eq_subst_rev 8 7, P u ↔ set u.
10. 8, 7 ⊢ x = a, wk 8.
11. 8 ⊢ set a → x = a, subj_intro 10.
12. 7, 8 ⊢ x ∈ {x | set a → x = a}, comp_intro 9 11.
13. 7, 8 ⊢ x ∈ {a}, eq_subst_rev sg_eq 12, P u ↔ x ∈ u.
14. 7 ⊢ x = a → x ∈ {a}, subj_intro 13.
sg_intro. ⊢ set a → x = a → x ∈ {a}, subj_intro 14.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.