Theorem disjoint_sg_from_new

Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ ¬a ∈ X, hypo.
03. 3 ⊢ x ∈ X ∩ {a}, hypo.
04. 3 ⊢ x ∈ X, intersection_eliml 3.
05. 3 ⊢ x ∈ {a}, intersection_elimr 3.
06. 1, 3 ⊢ x = a, sg_elim 1 5.
07. 1, 3 ⊢ a ∈ X, eq_subst 6 4.
08. 1, 2, 3 ⊢ ⊥, neg_elim 2 7.
09. 1, 2, 3 ⊢ x ∈ ∅, efq 8.
10. 1, 2 ⊢ x ∈ X ∩ {a} → x ∈ ∅, subj_intro 9.
11. 1, 2 ⊢ ∀x. x ∈ X ∩ {a} → x ∈ ∅, uq_intro 10.
12. 1, 2 ⊢ X ∩ {a} ⊆ ∅, incl_intro 11.
13. ⊢ ∅ ⊆ X ∩ {a}, empty_set_is_least.
14. 1, 2 ⊢ X ∩ {a} = ∅, incl_antisym 12 13.
disjoint_sg_from_new. ⊢ set a → ¬a ∈ X → X ∩ {a} = ∅,
  subj_intro_ii 14.

Dependencies
The given proof depends on four axioms:
comp, efq, eq_subst, ext.