Metamath Proof Explorer

Theorem inpr0

Description: Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion inpr0 ⊢ A ∩ B C = ∅ ↔ ¬ B ∈ A ∧ ¬ C ∈ A

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ x ∈ A x ≠ B ∧ x ≠ C ↔ ∀ x ∈ A x ≠ B ∧ ∀ x ∈ A x ≠ C
2 nelpr ⊢ x ∈ V → ¬ x ∈ B C ↔ x ≠ B ∧ x ≠ C
3 2 elv ⊢ ¬ x ∈ B C ↔ x ≠ B ∧ x ≠ C
4 3 imbi2i ⊢ x ∈ A → ¬ x ∈ B C ↔ x ∈ A → x ≠ B ∧ x ≠ C
5 4 albii ⊢ ∀ x x ∈ A → ¬ x ∈ B C ↔ ∀ x x ∈ A → x ≠ B ∧ x ≠ C
6 disj1 ⊢ A ∩ B C = ∅ ↔ ∀ x x ∈ A → ¬ x ∈ B C
7 df-ral ⊢ ∀ x ∈ A x ≠ B ∧ x ≠ C ↔ ∀ x x ∈ A → x ≠ B ∧ x ≠ C
8 5 6 7 3bitr4i ⊢ A ∩ B C = ∅ ↔ ∀ x ∈ A x ≠ B ∧ x ≠ C
9 nelb ⊢ ¬ B ∈ A ↔ ∀ x ∈ A x ≠ B
10 nelb ⊢ ¬ C ∈ A ↔ ∀ x ∈ A x ≠ C
11 9 10 anbi12i ⊢ ¬ B ∈ A ∧ ¬ C ∈ A ↔ ∀ x ∈ A x ≠ B ∧ ∀ x ∈ A x ≠ C
12 1 8 11 3bitr4i ⊢ A ∩ B C = ∅ ↔ ¬ B ∈ A ∧ ¬ C ∈ A