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

Metamath Proof Explorer

Theorem inpr0

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

Ref Expression
Assertion inpr0 ( ( 𝐴 ∩ { 𝐵 , 𝐶 } ) = ∅ ↔ ( ¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐶 ) )
2 nelpr ⊢ ( 𝑥 ∈ V → ( ¬ 𝑥 ∈ { 𝐵 , 𝐶 } ↔ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
3 2 elv ⊢ ( ¬ 𝑥 ∈ { 𝐵 , 𝐶 } ↔ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) )
4 3 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 , 𝐶 } ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
5 4 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 , 𝐶 } ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
6 disj1 ⊢ ( ( 𝐴 ∩ { 𝐵 , 𝐶 } ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 , 𝐶 } ) )
7 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
8 5 6 7 3bitr4i ⊢ ( ( 𝐴 ∩ { 𝐵 , 𝐶 } ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) )
9 nelb ⊢ ( ¬ 𝐵 ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐵 )
10 nelb ⊢ ( ¬ 𝐶 ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐶 )
11 9 10 anbi12i ⊢ ( ( ¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≠ 𝐶 ) )
12 1 8 11 3bitr4i ⊢ ( ( 𝐴 ∩ { 𝐵 , 𝐶 } ) = ∅ ↔ ( ¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) )