Proof
01. 1 ⊢ x ∈ A \ B, hypo.
02. 1 ⊢ x ∈ A, diff_eliml 1.
03. 1 ⊢ ¬x ∈ B, diff_elimr 1.
04. 1 ⊢ set x, set_intro 2.
05. 1 ⊢ x ∈ {x | ¬x ∈ B}, comp_intro 4 3.
06. ⊢ compl B = {x | ¬x ∈ B}, compl_eq.
07. 1 ⊢ x ∈ compl B, eq_subst_rev 6 5, P u ↔ x ∈ u.
08. 1 ⊢ x ∈ A ∩ compl B, intersection_intro 2 7.
09. ⊢ x ∈ A \ B → x ∈ A ∩ compl B, subj_intro 8.
10. 10 ⊢ x ∈ A ∩ compl B, hypo.
11. 10 ⊢ x ∈ A, intersection_eliml 10.
12. 10 ⊢ x ∈ compl B, intersection_elimr 10.
13. 10 ⊢ x ∈ {x | ¬x ∈ B}, eq_subst 6 12, P u ↔ x ∈ u.
14. 10 ⊢ ¬x ∈ B, comp_elim 13.
15. 10 ⊢ x ∈ A \ B, diff_intro 11 14.
16. ⊢ x ∈ A ∩ compl B → x ∈ A \ B, subj_intro 15.
17. ⊢ x ∈ A \ B ↔ x ∈ A ∩ compl B, bij_intro 9 16.
18. ⊢ ∀x. x ∈ A \ B ↔ x ∈ A ∩ compl B, uq_intro 17.
diff_as_inter. ⊢ A \ B = A ∩ compl B, ext 18.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.