Step | Hyp | Ref
| Expression |
1 | | elun 3259 |
. . 3
⊢ (𝑥 ∈ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐶))) |
2 | | eldif 3121 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
3 | | eldif 3121 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) |
4 | 2, 3 | orbi12i 754 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))) |
5 | | andi 808 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))) |
6 | 4, 5 | bitr4i 186 |
. . . . 5
⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶))) |
7 | | pm3.14 743 |
. . . . . 6
⊢ ((¬
𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶) → ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
8 | 7 | anim2i 340 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐶)) → (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
9 | 6, 8 | sylbi 120 |
. . . 4
⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
10 | | eldif 3121 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
11 | | elin 3301 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
12 | 11 | notbii 658 |
. . . . . 6
⊢ (¬
𝑥 ∈ (𝐵 ∩ 𝐶) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
13 | 12 | anbi2i 453 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
14 | 10, 13 | bitr2i 184 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ 𝑥 ∈ (𝐴 ∖ (𝐵 ∩ 𝐶))) |
15 | 9, 14 | sylib 121 |
. . 3
⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝑥 ∈ (𝐴 ∖ (𝐵 ∩ 𝐶))) |
16 | 1, 15 | sylbi 120 |
. 2
⊢ (𝑥 ∈ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) → 𝑥 ∈ (𝐴 ∖ (𝐵 ∩ 𝐶))) |
17 | 16 | ssriv 3142 |
1
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∩ 𝐶)) |