Proof 01. 1 ⊢ x ∈ A ∩ (B \ A), hypo. 02. 1 ⊢ x ∈ A, intersection_eliml 1. 03. 1 ⊢ x ∈ B \ A, intersection_elimr 1. 04. 1 ⊢ ¬x ∈ A, diff_elimr 3. 05. 1 ⊢ ⊥, neg_elim 4 2. 06. 1 ⊢ x ∈ ∅, efq 5. 07. ⊢ x ∈ A ∩ (B \ A) → x ∈ ∅, subj_intro 6. 08. ⊢ ∀x. x ∈ A ∩ (B \ A) → x ∈ ∅, uq_intro 7. 09. ⊢ A ∩ (B \ A) ⊆ ∅, incl_intro 8. 10. ⊢ ∅ ⊆ A ∩ (B \ A), empty_set_is_least. intersection_rel_compl. ⊢ A ∩ (B \ A) = ∅, incl_antisym 9 10.
Dependencies
The given proof depends on four axioms:
comp, efq, eq_subst, ext.