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

Metamath Proof Explorer

Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by GG, 28-Jun-2024)

Ref Expression
Assertion disj ⊢ A ∩ B = ∅ ↔ ∀ x ∈ A ¬ x ∈ B

Proof

Step Hyp Ref Expression
1 df-in ⊢ A ∩ B = y | y ∈ A ∧ y ∈ B
2 1 eqeq1i ⊢ A ∩ B = ∅ ↔ y | y ∈ A ∧ y ∈ B = ∅
3 eleq1w ⊢ y = x → y ∈ A ↔ x ∈ A
4 eleq1w ⊢ y = x → y ∈ B ↔ x ∈ B
5 3 4 anbi12d ⊢ y = x → y ∈ A ∧ y ∈ B ↔ x ∈ A ∧ x ∈ B
6 5 eqabcbw ⊢ y | y ∈ A ∧ y ∈ B = ∅ ↔ ∀ x x ∈ A ∧ x ∈ B ↔ x ∈ ∅
7 imnan ⊢ x ∈ A → ¬ x ∈ B ↔ ¬ x ∈ A ∧ x ∈ B
8 noel ⊢ ¬ x ∈ ∅
9 8 nbn ⊢ ¬ x ∈ A ∧ x ∈ B ↔ x ∈ A ∧ x ∈ B ↔ x ∈ ∅
10 7 9 bitr2i ⊢ x ∈ A ∧ x ∈ B ↔ x ∈ ∅ ↔ x ∈ A → ¬ x ∈ B
11 10 albii ⊢ ∀ x x ∈ A ∧ x ∈ B ↔ x ∈ ∅ ↔ ∀ x x ∈ A → ¬ x ∈ B
12 2 6 11 3bitri ⊢ A ∩ B = ∅ ↔ ∀ x x ∈ A → ¬ x ∈ B
13 df-ral ⊢ ∀ x ∈ A ¬ x ∈ B ↔ ∀ x x ∈ A → ¬ x ∈ B
14 12 13 bitr4i ⊢ A ∩ B = ∅ ↔ ∀ x ∈ A ¬ x ∈ B