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 ( ( 𝐴 ∩ { 𝐵 , 𝐶 } ) = ∅ ↔ ( ¬ 𝐵𝐴 ∧ ¬ 𝐶𝐴 ) )