Step | Hyp | Ref
| Expression |
1 | | ax-in2 605 |
. . . . . . . 8
⊢ (¬
(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ⊥)) |
2 | 1 | expd 256 |
. . . . . . 7
⊢ (¬
(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 → ⊥))) |
3 | | dfnot 1353 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐵 → ⊥)) |
4 | 2, 3 | syl6ibr 161 |
. . . . . 6
⊢ (¬
(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
5 | 4 | com12 30 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐵)) |
6 | 5 | imdistani 442 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
7 | | simpr 109 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | 7 | con3i 622 |
. . . . 5
⊢ (¬
𝑥 ∈ 𝐵 → ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
9 | 8 | anim2i 340 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
10 | 6, 9 | impbii 125 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
11 | | eldif 3111 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))) |
12 | | elin 3291 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
13 | 12 | notbii 658 |
. . . . 5
⊢ (¬
𝑥 ∈ (𝐴 ∩ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
14 | 13 | anbi2i 453 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
15 | 11, 14 | bitri 183 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
16 | | eldif 3111 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
17 | 10, 15, 16 | 3bitr4i 211 |
. 2
⊢ (𝑥 ∈ (𝐴 ∖ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
18 | 17 | eqriv 2154 |
1
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) |