Proof
01. 1 ⊢ ∀x. ¬x ∈ A, hypo.
02. 1 ⊢ ¬x ∈ A, uq_elim 1.
03. 3 ⊢ x ∈ A, hypo.
04. 1, 3 ⊢ ⊥, neg_elim 2 3.
05. 3 ⊢ set x, set_intro 3.
06. 1, 3 ⊢ x ∈ {x | ⊥}, comp_intro 5 4.
07. 1, 3 ⊢ x ∈ ∅, eq_subst_rev empty_set_eq 6, P u ↔ x ∈ u.
08. 1 ⊢ x ∈ A → x ∈ ∅, subj_intro 7.
09. 1 ⊢ ∀x. x ∈ A → x ∈ ∅, uq_intro 8.
10. 1 ⊢ A ⊆ ∅, incl_intro 9.
11. ⊢ ∅ ⊆ A, empty_set_is_least.
12. 1 ⊢ A = ∅, incl_antisym 10 11.
set_with_no_elements. ⊢ (∀x. ¬x ∈ A) → A = ∅, subj_intro 12.
Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.