Proof of Theorem difeq
Step | Hyp | Ref
| Expression |
1 | | incom 4128 |
. . . . 5
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∩ 𝐵) |
2 | | disjdif 4379 |
. . . . 5
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
3 | 1, 2 | eqtr3i 2823 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
4 | | ineq1 4131 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∩ 𝐵) = (𝐶 ∩ 𝐵)) |
5 | 3, 4 | syl5reqr 2848 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∩ 𝐵) = ∅) |
6 | | undif1 4382 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
7 | | uneq1 4083 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐶 ∪ 𝐵)) |
8 | 6, 7 | syl5reqr 2848 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) |
9 | 5, 8 | jca 515 |
. 2
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |
10 | | simpl 486 |
. . . 4
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∩ 𝐵) = ∅) |
11 | | disj3 4361 |
. . . . 5
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ 𝐶 = (𝐶 ∖ 𝐵)) |
12 | | eqcom 2805 |
. . . . 5
⊢ (𝐶 = (𝐶 ∖ 𝐵) ↔ (𝐶 ∖ 𝐵) = 𝐶) |
13 | 11, 12 | bitri 278 |
. . . 4
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ (𝐶 ∖ 𝐵) = 𝐶) |
14 | 10, 13 | sylib 221 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∖ 𝐵) = 𝐶) |
15 | | difeq1 4043 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∪ 𝐵) ∖ 𝐵)) |
16 | | difun2 4387 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) ∖ 𝐵) = (𝐶 ∖ 𝐵) |
17 | | difun2 4387 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
18 | 15, 16, 17 | 3eqtr3g 2856 |
. . . . 5
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → (𝐶 ∖ 𝐵) = (𝐴 ∖ 𝐵)) |
19 | 18 | eqeq1d 2800 |
. . . 4
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
20 | 19 | adantl 485 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
21 | 14, 20 | mpbid 235 |
. 2
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐴 ∖ 𝐵) = 𝐶) |
22 | 9, 21 | impbii 212 |
1
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |