Proof of Theorem uneqin
Step | Hyp | Ref
| Expression |
1 | | eqimss 3978 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → (𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵)) |
2 | | unss 4119 |
. . . . 5
⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∩ 𝐵)) ↔ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵)) |
3 | | ssin 4166 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) ↔ 𝐴 ⊆ (𝐴 ∩ 𝐵)) |
4 | | sstr 3930 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ 𝐵) |
5 | 3, 4 | sylbir 234 |
. . . . . 6
⊢ (𝐴 ⊆ (𝐴 ∩ 𝐵) → 𝐴 ⊆ 𝐵) |
6 | | ssin 4166 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵) ↔ 𝐵 ⊆ (𝐴 ∩ 𝐵)) |
7 | | simpl 483 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵) → 𝐵 ⊆ 𝐴) |
8 | 6, 7 | sylbir 234 |
. . . . . 6
⊢ (𝐵 ⊆ (𝐴 ∩ 𝐵) → 𝐵 ⊆ 𝐴) |
9 | 5, 8 | anim12i 613 |
. . . . 5
⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∩ 𝐵)) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
10 | 2, 9 | sylbir 234 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
11 | 1, 10 | syl 17 |
. . 3
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
12 | | eqss 3937 |
. . 3
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
13 | 11, 12 | sylibr 233 |
. 2
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) → 𝐴 = 𝐵) |
14 | | unidm 4087 |
. . . 4
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
15 | | inidm 4154 |
. . . 4
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
16 | 14, 15 | eqtr4i 2769 |
. . 3
⊢ (𝐴 ∪ 𝐴) = (𝐴 ∩ 𝐴) |
17 | | uneq2 4092 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐴) = (𝐴 ∪ 𝐵)) |
18 | | ineq2 4142 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐴) = (𝐴 ∩ 𝐵)) |
19 | 16, 17, 18 | 3eqtr3a 2802 |
. 2
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵)) |
20 | 13, 19 | impbii 208 |
1
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) |