Theorem diff_elimr

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

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