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