Theorem diff_eliml

Proof
01. 1 ⊢ x ∈ A \ B, hypo.
02. 1 ⊢ x ∈ A ∧ ¬x ∈ B, diff_elim 1.
03. 1 ⊢ x ∈ A, conj_eliml 2.
diff_eliml. ⊢ x ∈ A \ B → x ∈ A, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.