Proof
01. 1 ⊢ set y, hypo.
02. 2 ⊢ ¬x = y, hypo.
03. 3 ⊢ x ∈ {y}, hypo.
04. 1, 3 ⊢ x = y, sg_elim 1 3.
05. 1, 2, 3 ⊢ ⊥, neg_elim 2 4.
06. 1, 2 ⊢ ¬x ∈ {y}, neg_intro 5.
sg_neg_intro. ⊢ set y → ¬x = y → ¬x ∈ {y}, subj_intro_ii 6.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.