Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ x ⊆ {a}, hypo.
03. ⊢ a ∈ x ∨ ¬a ∈ x, lem.
04. 4 ⊢ a ∈ x, hypo.
05. 5 ⊢ u ∈ {a}, hypo.
06. 1, 5 ⊢ u = a, sg_elim 1 5.
07. 1, 4, 5 ⊢ u ∈ x, eq_subst_rev 6 4, P u ↔ u ∈ x.
08. 1, 4 ⊢ u ∈ {a} → u ∈ x, subj_intro 7.
09. 1, 4 ⊢ ∀u. u ∈ {a} → u ∈ x, uq_intro 8.
10. 1, 4 ⊢ {a} ⊆ x, incl_intro 9.
11. 1, 2, 4 ⊢ x = {a}, incl_antisym 2 10.
12. 1, 2, 4 ⊢ x = ∅ ∨ x = {a}, disj_intror 11.
13. 13 ⊢ ¬a ∈ x, hypo.
14. 14 ⊢ u ∈ x, hypo.
15. 2, 14 ⊢ u ∈ {a}, incl_elim 2 14.
16. 1, 2, 14 ⊢ u = a, sg_elim 1 15.
17. 1, 2, 14 ⊢ a ∈ x, eq_subst 16 14, P u ↔ u ∈ x.
18. 1, 2, 13, 14 ⊢ ⊥, neg_elim 13 17.
19. 1, 2, 13, 14 ⊢ u ∈ ∅, efq 18.
20. 1, 2, 13 ⊢ u ∈ x → u ∈ ∅, subj_intro 19.
21. 1, 2, 13 ⊢ ∀u. u ∈ x → u ∈ ∅, uq_intro 20.
22. 1, 2, 13 ⊢ x ⊆ ∅, incl_intro 21.
23. ⊢ ∅ ⊆ x, empty_set_is_least.
24. 1, 2, 13 ⊢ x = ∅, incl_antisym 22 23.
25. 1, 2, 13 ⊢ x = ∅ ∨ x = {a}, disj_introl 24.
26. 1, 2 ⊢ x = ∅ ∨ x = {a}, disj_elim 3 12 25.
subsets_of_sg. ⊢ set a → x ⊆ {a} → x = ∅ ∨ x = {a}, subj_intro_ii 26.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.