Proof
01. 1 ⊢ x ∈ A \ {x}, hypo.
02. 1 ⊢ ¬x ∈ {x}, diff_elimr 1.
03. 1 ⊢ set x, set_intro 1.
04. ⊢ x = x, eq_refl.
05. 1 ⊢ x ∈ {x}, sg_intro 3 4.
06. 1 ⊢ ⊥, neg_elim 2 5.
diff_sg_contra. ⊢ x ∈ A \ {x} → ⊥, subj_intro 6.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.