This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjel

Description: A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015)

Ref Expression
Assertion disjel ⊢ A ∩ B = ∅ ∧ C ∈ A → ¬ C ∈ B

Proof

Step Hyp Ref Expression
1 disj3 ⊢ A ∩ B = ∅ ↔ A = A ∖ B
2 eleq2 ⊢ A = A ∖ B → C ∈ A ↔ C ∈ A ∖ B
3 eldifn ⊢ C ∈ A ∖ B → ¬ C ∈ B
4 2 3 biimtrdi ⊢ A = A ∖ B → C ∈ A → ¬ C ∈ B
5 1 4 sylbi ⊢ A ∩ B = ∅ → C ∈ A → ¬ C ∈ B
6 5 imp ⊢ A ∩ B = ∅ ∧ C ∈ A → ¬ C ∈ B