Proof of Theorem uneqin
| Step | Hyp | Ref
| Expression |
| 1 | | eqimss 4042 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → (𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵)) |
| 2 | | unss 4190 |
. . . . 5
⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∩ 𝐵)) ↔ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵)) |
| 3 | | ssin 4239 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) ↔ 𝐴 ⊆ (𝐴 ∩ 𝐵)) |
| 4 | | sstr 3992 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) |
| 5 | 3, 4 | sylbir 235 |
. . . . . 6
⊢ (𝐴 ⊆ (𝐴 ∩ 𝐵) → 𝐴 ⊆ 𝐵) |
| 6 | | ssin 4239 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵) ↔ 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
| 7 | | simpl 482 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵) → 𝐵 ⊆ 𝐴) |
| 8 | 6, 7 | sylbir 235 |
. . . . . 6
⊢ (𝐵 ⊆ (𝐴 ∩ 𝐵) → 𝐵 ⊆ 𝐴) |
| 9 | 5, 8 | anim12i 613 |
. . . . 5
⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∩ 𝐵)) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
| 10 | 2, 9 | sylbir 235 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
| 11 | 1, 10 | syl 17 |
. . 3
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
| 12 | | eqss 3999 |
. . 3
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
| 13 | 11, 12 | sylibr 234 |
. 2
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → 𝐴 = 𝐵) |
| 14 | | unidm 4157 |
. . . 4
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
| 15 | | inidm 4227 |
. . . 4
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 16 | 14, 15 | eqtr4i 2768 |
. . 3
⊢ (𝐴 ∪ 𝐴) = (𝐴 ∩ 𝐴) |
| 17 | | uneq2 4162 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐴) = (𝐴 ∪ 𝐵)) |
| 18 | | ineq2 4214 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐴) = (𝐴 ∩ 𝐵)) |
| 19 | 16, 17, 18 | 3eqtr3a 2801 |
. 2
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵)) |
| 20 | 13, 19 | impbii 209 |
1
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) |