Proof of Theorem difeq
| Step | Hyp | Ref
| Expression |
| 1 | | ineq1 4213 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∩ 𝐵) = (𝐶 ∩ 𝐵)) |
| 2 | | disjdifr 4473 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
| 3 | 1, 2 | eqtr3di 2792 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∩ 𝐵) = ∅) |
| 4 | | uneq1 4161 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐶 ∪ 𝐵)) |
| 5 | | undif1 4476 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
| 6 | 4, 5 | eqtr3di 2792 |
. . 3
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) |
| 7 | 3, 6 | jca 511 |
. 2
⊢ ((𝐴 ∖ 𝐵) = 𝐶 → ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |
| 8 | | simpl 482 |
. . . 4
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∩ 𝐵) = ∅) |
| 9 | | disj3 4454 |
. . . . 5
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ 𝐶 = (𝐶 ∖ 𝐵)) |
| 10 | | eqcom 2744 |
. . . . 5
⊢ (𝐶 = (𝐶 ∖ 𝐵) ↔ (𝐶 ∖ 𝐵) = 𝐶) |
| 11 | 9, 10 | bitri 275 |
. . . 4
⊢ ((𝐶 ∩ 𝐵) = ∅ ↔ (𝐶 ∖ 𝐵) = 𝐶) |
| 12 | 8, 11 | sylib 218 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐶 ∖ 𝐵) = 𝐶) |
| 13 | | difeq1 4119 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∪ 𝐵) ∖ 𝐵)) |
| 14 | | difun2 4481 |
. . . . . 6
⊢ ((𝐶 ∪ 𝐵) ∖ 𝐵) = (𝐶 ∖ 𝐵) |
| 15 | | difun2 4481 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
| 16 | 13, 14, 15 | 3eqtr3g 2800 |
. . . . 5
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → (𝐶 ∖ 𝐵) = (𝐴 ∖ 𝐵)) |
| 17 | 16 | eqeq1d 2739 |
. . . 4
⊢ ((𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
| 18 | 17 | adantl 481 |
. . 3
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → ((𝐶 ∖ 𝐵) = 𝐶 ↔ (𝐴 ∖ 𝐵) = 𝐶)) |
| 19 | 12, 18 | mpbid 232 |
. 2
⊢ (((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)) → (𝐴 ∖ 𝐵) = 𝐶) |
| 20 | 7, 19 | impbii 209 |
1
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) |