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

Metamath Proof Explorer

Theorem ndisj2

Description: A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis ndisj2.1 ⊢ x = y → B = C
Assertion ndisj2 ⊢ ¬ Disj x ∈ A B ↔ ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ B ∩ C ≠ ∅

Proof

Step Hyp Ref Expression
1 ndisj2.1 ⊢ x = y → B = C
2 1 disjor ⊢ Disj x ∈ A B ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ B ∩ C = ∅
3 2 notbii ⊢ ¬ Disj x ∈ A B ↔ ¬ ∀ x ∈ A ∀ y ∈ A x = y ∨ B ∩ C = ∅
4 rexnal ⊢ ∃ x ∈ A ¬ ∀ y ∈ A x = y ∨ B ∩ C = ∅ ↔ ¬ ∀ x ∈ A ∀ y ∈ A x = y ∨ B ∩ C = ∅
5 rexnal ⊢ ∃ y ∈ A ¬ x = y ∨ B ∩ C = ∅ ↔ ¬ ∀ y ∈ A x = y ∨ B ∩ C = ∅
6 ioran ⊢ ¬ x = y ∨ B ∩ C = ∅ ↔ ¬ x = y ∧ ¬ B ∩ C = ∅
7 df-ne ⊢ x ≠ y ↔ ¬ x = y
8 df-ne ⊢ B ∩ C ≠ ∅ ↔ ¬ B ∩ C = ∅
9 7 8 anbi12i ⊢ x ≠ y ∧ B ∩ C ≠ ∅ ↔ ¬ x = y ∧ ¬ B ∩ C = ∅
10 6 9 bitr4i ⊢ ¬ x = y ∨ B ∩ C = ∅ ↔ x ≠ y ∧ B ∩ C ≠ ∅
11 10 rexbii ⊢ ∃ y ∈ A ¬ x = y ∨ B ∩ C = ∅ ↔ ∃ y ∈ A x ≠ y ∧ B ∩ C ≠ ∅
12 5 11 bitr3i ⊢ ¬ ∀ y ∈ A x = y ∨ B ∩ C = ∅ ↔ ∃ y ∈ A x ≠ y ∧ B ∩ C ≠ ∅
13 12 rexbii ⊢ ∃ x ∈ A ¬ ∀ y ∈ A x = y ∨ B ∩ C = ∅ ↔ ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ B ∩ C ≠ ∅
14 3 4 13 3bitr2i ⊢ ¬ Disj x ∈ A B ↔ ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ B ∩ C ≠ ∅