Proof of Theorem difeq
Step | Hyp | Ref
| Expression |
1 | | incom 3805 |
. . . . 5
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∩ 𝐵) |
2 | | disjdif 4040 |
. . . . 5
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
3 | 1, 2 | eqtr3i 2646 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
4 | | ineq1 3807 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∩ 𝐵) = (𝐶 ∩ 𝐵)) |
5 | 3, 4 | syl5reqr 2671 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∩ 𝐵) = ∅) |
6 | | undif1 4043 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
7 | | uneq1 3760 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐶 ∪ 𝐵)) |
8 | 6, 7 | syl5reqr 2671 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) |
9 | 5, 8 | jca 554 |
. 2
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |
10 | | simpl 473 |
. . . 4
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∩ 𝐵) = ∅) |
11 | | disj3 4021 |
. . . . 5
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ 𝐶 = (𝐶 ∖ 𝐵)) |
12 | | eqcom 2629 |
. . . . 5
⊢ (𝐶 = (𝐶 ∖ 𝐵) ↔ (𝐶 ∖ 𝐵) = 𝐶) |
13 | 11, 12 | bitri 264 |
. . . 4
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ (𝐶 ∖ 𝐵) = 𝐶) |
14 | 10, 13 | sylib 208 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∖ 𝐵) = 𝐶) |
15 | | difeq1 3721 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∪ 𝐵) ∖ 𝐵)) |
16 | | difun2 4048 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) ∖ 𝐵) = (𝐶 ∖ 𝐵) |
17 | | difun2 4048 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
18 | 15, 16, 17 | 3eqtr3g 2679 |
. . . . 5
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → (𝐶 ∖ 𝐵) = (𝐴 ∖ 𝐵)) |
19 | 18 | eqeq1d 2624 |
. . . 4
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
20 | 19 | adantl 482 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
21 | 14, 20 | mpbid 222 |
. 2
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐴 ∖ 𝐵) = 𝐶) |
22 | 9, 21 | impbii 199 |
1
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |