Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 3 ⊢ ¬a = b, hypo.
04. 4 ⊢ x ∈ {a} ∩ {b}, hypo.
05. 4 ⊢ x ∈ {a}, intersection_eliml 4.
06. 4 ⊢ x ∈ {b}, intersection_elimr 4.
07. 1, 4 ⊢ x = a, sg_elim 1 5.
08. 1, 4 ⊢ a = x, eq_symm 7.
09. 2, 4 ⊢ x = b, sg_elim 2 6.
10. 1, 2, 4 ⊢ a = b, eq_trans 8 9.
11. 1, 2, 3, 4 ⊢ ⊥, neg_elim 3 10.
12. 1, 2, 3, 4 ⊢ x ∈ ∅, efq 11.
13. 1, 2, 3 ⊢ x ∈ {a} ∩ {b} → x ∈ ∅, subj_intro 12.
14. 1, 2, 3 ⊢ ∀x. x ∈ {a} ∩ {b} → x ∈ ∅, uq_intro 13.
15. 1, 2, 3 ⊢ {a} ∩ {b} ⊆ ∅, incl_intro 14.
16. ⊢ ∅ ⊆ {a} ∩ {b}, empty_set_is_least.
17. 1, 2, 3 ⊢ {a} ∩ {b} = ∅, incl_antisym 15 16.
disjoint_sg_from_neq. ⊢ set a → set b → ¬a = b → {a} ∩ {b} = ∅,
subj_intro_iii 17.
Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.