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