Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ x ∈ power {a}, hypo.
03. 2 ⊢ x ⊆ {a}, power_elim 2.
04. 1, 2 ⊢ x = ∅ ∨ x = {a}, subsets_of_sg 1 3.
05. 5 ⊢ x = ∅, hypo.
06. 5 ⊢ x ∈ {∅}, sg_intro empty_set_is_set 5.
07. 5 ⊢ x ∈ {∅, {a}}, union_introl 6.
08. 8 ⊢ x = {a}, hypo.
09. 1 ⊢ set {a}, set_sg 1.
10. 1, 8 ⊢ x ∈ {{a}}, sg_intro 9 8.
11. 1, 8 ⊢ x ∈ {∅, {a}}, union_intror 10.
12. 1, 2 ⊢ x ∈ {∅, {a}}, disj_elim 4 7 11.
13. 1 ⊢ x ∈ power {a} → x ∈ {∅, {a}}, subj_intro 12.
14. 14 ⊢ x ∈ {∅, {a}}, hypo.
15. 14 ⊢ x ∈ {∅} ∨ x ∈ {{a}}, union_elim 14.
16. 16 ⊢ x ∈ {∅}, hypo.
17. 16 ⊢ x = ∅, sg_elim empty_set_is_set 16.
18. ⊢ ∅ ⊆ {a}, empty_set_is_least.
19. 16 ⊢ x ⊆ {a}, eq_subst_rev 17 18, P u ↔ u ⊆ {a}.
20. 20 ⊢ x ∈ {{a}}, hypo.
21. 1, 20 ⊢ x = {a}, sg_elim 9 20.
22. ⊢ {a} ⊆ {a}, incl_refl.
23. 1, 20 ⊢ x ⊆ {a}, eq_subst_rev 21 22, P u ↔ u ⊆ {a}.
24. 1, 14 ⊢ x ⊆ {a}, disj_elim 15 19 23.
25. 14 ⊢ set x, set_intro 14.
26. 1, 14 ⊢ x ∈ power {a}, power_intro 25 24.
27. 1 ⊢ x ∈ {∅, {a}} → x ∈ power {a}, subj_intro 26.
28. 1 ⊢ x ∈ power {a} ↔ x ∈ {∅, {a}}, bij_intro 13 27.
29. 1 ⊢ ∀x. x ∈ power {a} ↔ x ∈ {∅, {a}}, uq_intro 28.
30. 1 ⊢ power {a} = {∅, {a}}, ext 29.
power_sg. ⊢ set a → power {a} = {∅, {a}}, subj_intro 30.
Dependencies
The given proof depends on eight axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, pairing.