Proof 01. 1 ⊢ A ∩ B = ∅, hypo. 02. 2 ⊢ x ∈ A, hypo. 03. 3 ⊢ x ∈ B, hypo. 04. 2, 3 ⊢ x ∈ A ∩ B, intersection_intro 2 3. 05. 1, 2, 3 ⊢ x ∈ ∅, eq_subst 1 4, P u ↔ x ∈ u. 06. 1, 2, 3 ⊢ ⊥, empty_contra 5. disjoint_property. ⊢ A ∩ B = ∅ → x ∈ A → x ∈ B → ⊥, subj_intro_iii 6.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.