Proof
01. 1 ⊢ ∅ = {∅}, hypo.
02. 1 ⊢ {∅} ⊆ ∅, incl_from_eq_rev 1.
03. ⊢ ∅ = ∅, eq_refl.
04. ⊢ ∅ ∈ {∅}, sg_intro empty_set_is_set 3.
05. 1 ⊢ ∅ ∈ ∅, incl_elim 2 4.
06. 1 ⊢ ⊥, empty_contra 5.
zero_neq_one. ⊢ ¬∅ = {∅}, neg_intro 6.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, infinity.