Proof
01. 1 ⊢ x ∈ power ∅, hypo.
02. 1 ⊢ x ⊆ ∅, power_elim 1.
03. ⊢ ∅ ⊆ x, empty_set_is_least.
04. 1 ⊢ x = ∅, incl_antisym 2 3.
05. 1 ⊢ x ∈ {∅}, sg_intro empty_set_is_set 4.
06. ⊢ x ∈ power ∅ → x ∈ {∅}, subj_intro 5.
07. 7 ⊢ x ∈ {∅}, hypo.
08. 7 ⊢ x = ∅, sg_elim empty_set_is_set 7.
09. 7 ⊢ x ⊆ ∅, incl_from_eq 8.
10. 7 ⊢ set x, set_intro 7.
11. 7 ⊢ x ∈ power ∅, power_intro 10 9.
12. ⊢ x ∈ {∅} → x ∈ power ∅, subj_intro 11.
13. ⊢ x ∈ power ∅ ↔ x ∈ {∅}, bij_intro 6 12.
14. ⊢ ∀x. x ∈ power ∅ ↔ x ∈ {∅}, uq_intro 13.
power_empty_set. ⊢ power ∅ = {∅}, ext 14.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, infinity.