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