diff_disjoint

Theorem diff_disjoint

Theorem. diff_disjoint
A ∩ B = ∅ → A \ B = A

Proof
01. 1 ⊢ A ∩ B = ∅, hypo.
02. 2 ⊢ u ∈ A, hypo.
03. 3 ⊢ u ∈ B, hypo.
04. 2, 3 ⊢ u ∈ A ∩ B, intersection_intro 2 3.
05. 1, 2, 3 ⊢ u ∈ ∅, eq_subst 1 4, P x ↔ u ∈ x.
06. 1, 2, 3 ⊢ ⊥, empty_contra 5.
07. 1, 2 ⊢ ¬u ∈ B, neg_intro 6.
08. 1, 2 ⊢ u ∈ A \ B, diff_intro 2 7.
09. 1 ⊢ u ∈ A → u ∈ A \ B, subj_intro 8.
10. 1 ⊢ ∀u. u ∈ A → u ∈ A \ B, uq_intro 9.
11. 1 ⊢ A ⊆ A \ B, incl_intro 10.
12. ⊢ A \ B ⊆ A, diff_incl.
13. 1 ⊢ A \ B = A, incl_antisym 12 11.
diff_disjoint. ⊢ A ∩ B = ∅ → A \ B = A, subj_intro 13.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.