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

Metamath Proof Explorer

Theorem disjsn

Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

Ref Expression
Assertion disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A

Proof

Step Hyp Ref Expression
1 disj1 ⊢ A ∩ B = ∅ ↔ ∀ x x ∈ A → ¬ x ∈ B
2 con2b ⊢ x ∈ A → ¬ x ∈ B ↔ x ∈ B → ¬ x ∈ A
3 velsn ⊢ x ∈ B ↔ x = B
4 3 imbi1i ⊢ x ∈ B → ¬ x ∈ A ↔ x = B → ¬ x ∈ A
5 imnan ⊢ x = B → ¬ x ∈ A ↔ ¬ x = B ∧ x ∈ A
6 2 4 5 3bitri ⊢ x ∈ A → ¬ x ∈ B ↔ ¬ x = B ∧ x ∈ A
7 6 albii ⊢ ∀ x x ∈ A → ¬ x ∈ B ↔ ∀ x ¬ x = B ∧ x ∈ A
8 alnex ⊢ ∀ x ¬ x = B ∧ x ∈ A ↔ ¬ ∃ x x = B ∧ x ∈ A
9 dfclel ⊢ B ∈ A ↔ ∃ x x = B ∧ x ∈ A
10 8 9 xchbinxr ⊢ ∀ x ¬ x = B ∧ x ∈ A ↔ ¬ B ∈ A
11 1 7 10 3bitri ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A