Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ ¬x ∈ B, hypo.
03. 1 ⊢ set x, set_intro 1.
04. 1, 2 ⊢ x ∈ A ∧ ¬x ∈ B, conj_intro 1 2.
05. 1, 2 ⊢ x ∈ {x | x ∈ A ∧ ¬x ∈ B}, comp_intro 3 4.
06. 1, 2 ⊢ x ∈ A \ B, eq_subst_rev diff_eq 5, P u ↔ x ∈ u.
diff_intro. ⊢ x ∈ A → ¬x ∈ B → x ∈ A \ B, subj_intro_ii 6.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.