Step | Hyp | Ref
| Expression |
1 | | pm2.621 653 |
. . . . . . 7
⊢
((x ∈ A →
¬ x ∈
𝐶) → ((x ∈ A ∨ ¬ x ∈ 𝐶) → ¬ x ∈ 𝐶)) |
2 | | olc 619 |
. . . . . . 7
⊢ (¬
x ∈ 𝐶 → (x ∈ A ∨ ¬ x ∈ 𝐶)) |
3 | 1, 2 | impbid1 130 |
. . . . . 6
⊢
((x ∈ A →
¬ x ∈
𝐶) → ((x ∈ A ∨ ¬ x ∈ 𝐶) ↔ ¬ x ∈ 𝐶)) |
4 | 3 | anbi2d 440 |
. . . . 5
⊢
((x ∈ A →
¬ x ∈
𝐶) → (((x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ ¬ x ∈ 𝐶)) ↔ ((x ∈ A ∨ x ∈ B) ∧ ¬ x ∈ 𝐶))) |
5 | | eldif 2903 |
. . . . . . 7
⊢ (x ∈ (B ∖ 𝐶) ↔ (x ∈ B ∧ ¬ x ∈ 𝐶)) |
6 | 5 | orbi2i 666 |
. . . . . 6
⊢
((x ∈ A ∨ x ∈ (B ∖
𝐶)) ↔ (x ∈ A ∨ (x ∈ B ∧ ¬ x ∈ 𝐶))) |
7 | | ordi 717 |
. . . . . 6
⊢
((x ∈ A ∨ (x ∈ B ∧ ¬ x ∈ 𝐶)) ↔ ((x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ ¬ x ∈ 𝐶))) |
8 | 6, 7 | bitri 173 |
. . . . 5
⊢
((x ∈ A ∨ x ∈ (B ∖
𝐶)) ↔ ((x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ ¬ x ∈ 𝐶))) |
9 | | elun 3060 |
. . . . . 6
⊢ (x ∈ (A ∪ B)
↔ (x ∈ A ∨ x ∈ B)) |
10 | 9 | anbi1i 434 |
. . . . 5
⊢
((x ∈ (A ∪
B) ∧ ¬
x ∈ 𝐶) ↔ ((x ∈ A ∨ x ∈ B) ∧ ¬ x ∈ 𝐶)) |
11 | 4, 8, 10 | 3bitr4g 212 |
. . . 4
⊢
((x ∈ A →
¬ x ∈
𝐶) → ((x ∈ A ∨ x ∈ (B ∖ 𝐶)) ↔ (x ∈ (A ∪ B) ∧ ¬ x ∈ 𝐶))) |
12 | | elun 3060 |
. . . 4
⊢ (x ∈ (A ∪ (B
∖ 𝐶)) ↔
(x ∈
A ∨
x ∈
(B ∖ 𝐶))) |
13 | | eldif 2903 |
. . . 4
⊢ (x ∈ ((A ∪ B)
∖ 𝐶) ↔ (x ∈ (A ∪ B) ∧ ¬ x ∈ 𝐶)) |
14 | 11, 12, 13 | 3bitr4g 212 |
. . 3
⊢
((x ∈ A →
¬ x ∈
𝐶) → (x ∈ (A ∪ (B
∖ 𝐶)) ↔ x ∈ ((A ∪ B)
∖ 𝐶))) |
15 | 14 | alimi 1324 |
. 2
⊢ (∀x(x ∈ A → ¬ x
∈ 𝐶) → ∀x(x ∈ (A ∪ (B
∖ 𝐶)) ↔ x ∈ ((A ∪ B)
∖ 𝐶))) |
16 | | disj1 3246 |
. 2
⊢
((A ∩ 𝐶) = ∅ ↔ ∀x(x ∈ A → ¬ x
∈ 𝐶)) |
17 | | dfcleq 2017 |
. 2
⊢
((A ∪ (B ∖ 𝐶)) = ((A
∪ B) ∖ 𝐶) ↔ ∀x(x ∈ (A ∪ (B
∖ 𝐶)) ↔ x ∈ ((A ∪ B)
∖ 𝐶))) |
18 | 15, 16, 17 | 3imtr4i 190 |
1
⊢
((A ∩ 𝐶) = ∅ → (A ∪ (B
∖ 𝐶)) = ((A ∪ B)
∖ 𝐶)) |