Proof
01. 1 ⊢ x ∈ A \ B, hypo.
02. 1 ⊢ x ∈ {x | x ∈ A ∧ ¬x ∈ B}, eq_subst diff_eq 1, P u ↔ x ∈ u.
03. 1 ⊢ x ∈ A ∧ ¬x ∈ B, comp_elim 2.
diff_elim. ⊢ x ∈ A \ B → x ∈ A ∧ ¬x ∈ B, subj_intro 3.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.