Step | Hyp | Ref
| Expression |
1 | | ssel 2933 |
. . . . . . 7
⊢ (A ⊆ 𝐶 → (x ∈ A → x ∈ 𝐶)) |
2 | | ssel 2933 |
. . . . . . 7
⊢ (B ⊆ 𝐶 → (x ∈ B → x ∈ 𝐶)) |
3 | | pm5.1 533 |
. . . . . . 7
⊢
(((x ∈ A →
x ∈ 𝐶) ∧ (x ∈ B →
x ∈ 𝐶)) → ((x ∈ A → x ∈ 𝐶) ↔ (x ∈ B → x ∈ 𝐶))) |
4 | 1, 2, 3 | syl2an 273 |
. . . . . 6
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → ((x ∈ A → x ∈ 𝐶) ↔ (x ∈ B → x ∈ 𝐶))) |
5 | | con2b 592 |
. . . . . . 7
⊢
((x ∈ A →
¬ x ∈
B) ↔ (x ∈ B → ¬ x
∈ A)) |
6 | 5 | a1i 9 |
. . . . . 6
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → ((x ∈ A → ¬ x
∈ B)
↔ (x ∈ B →
¬ x ∈
A))) |
7 | 4, 6 | anbi12d 442 |
. . . . 5
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → (((x ∈ A → x ∈ 𝐶) ∧
(x ∈
A → ¬ x ∈ B)) ↔ ((x
∈ B
→ x ∈ 𝐶) ∧
(x ∈
B → ¬ x ∈ A)))) |
8 | | jcab 535 |
. . . . 5
⊢
((x ∈ A →
(x ∈
𝐶 ∧ ¬ x ∈ B)) ↔
((x ∈
A → x ∈ 𝐶) ∧ (x ∈ A →
¬ x ∈
B))) |
9 | | jcab 535 |
. . . . 5
⊢
((x ∈ B →
(x ∈
𝐶 ∧ ¬ x ∈ A)) ↔
((x ∈
B → x ∈ 𝐶) ∧ (x ∈ B →
¬ x ∈
A))) |
10 | 7, 8, 9 | 3bitr4g 212 |
. . . 4
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → ((x ∈ A → (x
∈ 𝐶 ∧ ¬
x ∈
B)) ↔ (x ∈ B → (x
∈ 𝐶 ∧ ¬
x ∈
A)))) |
11 | | eldif 2921 |
. . . . 5
⊢ (x ∈ (𝐶 ∖ B) ↔ (x
∈ 𝐶 ∧ ¬
x ∈
B)) |
12 | 11 | imbi2i 215 |
. . . 4
⊢
((x ∈ A →
x ∈
(𝐶 ∖ B)) ↔ (x
∈ A
→ (x ∈ 𝐶 ∧ ¬
x ∈
B))) |
13 | | eldif 2921 |
. . . . 5
⊢ (x ∈ (𝐶 ∖ A) ↔ (x
∈ 𝐶 ∧ ¬
x ∈
A)) |
14 | 13 | imbi2i 215 |
. . . 4
⊢
((x ∈ B →
x ∈
(𝐶 ∖ A)) ↔ (x
∈ B
→ (x ∈ 𝐶 ∧ ¬
x ∈
A))) |
15 | 10, 12, 14 | 3bitr4g 212 |
. . 3
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → ((x ∈ A → x ∈ (𝐶 ∖ B)) ↔ (x
∈ B
→ x ∈ (𝐶 ∖ A)))) |
16 | 15 | albidv 1702 |
. 2
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → (∀x(x ∈ A → x ∈ (𝐶 ∖ B)) ↔ ∀x(x ∈ B → x ∈ (𝐶 ∖ A)))) |
17 | | dfss2 2928 |
. 2
⊢ (A ⊆ (𝐶 ∖ B) ↔ ∀x(x ∈ A → x ∈ (𝐶 ∖ B))) |
18 | | dfss2 2928 |
. 2
⊢ (B ⊆ (𝐶 ∖ A) ↔ ∀x(x ∈ B → x ∈ (𝐶 ∖ A))) |
19 | 16, 17, 18 | 3bitr4g 212 |
1
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐶) → (A ⊆ (𝐶 ∖ B) ↔ B
⊆ (𝐶 ∖ A))) |