Proof of Theorem uneqin
Step | Hyp | Ref
| Expression |
1 | | eqimss 2991 |
. . . 4
⊢
((A ∪ B) = (A ∩
B) → (A ∪ B)
⊆ (A ∩ B)) |
2 | | unss 3111 |
. . . . 5
⊢
((A ⊆ (A ∩ B) ∧ B ⊆
(A ∩ B)) ↔ (A
∪ B) ⊆ (A ∩ B)) |
3 | | ssin 3153 |
. . . . . . 7
⊢
((A ⊆ A ∧ A ⊆ B)
↔ A ⊆ (A ∩ B)) |
4 | | sstr 2947 |
. . . . . . 7
⊢
((A ⊆ A ∧ A ⊆ B)
→ A ⊆ B) |
5 | 3, 4 | sylbir 125 |
. . . . . 6
⊢ (A ⊆ (A
∩ B) → A ⊆ B) |
6 | | ssin 3153 |
. . . . . . 7
⊢
((B ⊆ A ∧ B ⊆ B)
↔ B ⊆ (A ∩ B)) |
7 | | simpl 102 |
. . . . . . 7
⊢
((B ⊆ A ∧ B ⊆ B)
→ B ⊆ A) |
8 | 6, 7 | sylbir 125 |
. . . . . 6
⊢ (B ⊆ (A
∩ B) → B ⊆ A) |
9 | 5, 8 | anim12i 321 |
. . . . 5
⊢
((A ⊆ (A ∩ B) ∧ B ⊆
(A ∩ B)) → (A
⊆ B ∧ B ⊆
A)) |
10 | 2, 9 | sylbir 125 |
. . . 4
⊢
((A ∪ B) ⊆ (A
∩ B) → (A ⊆ B
∧ B
⊆ A)) |
11 | 1, 10 | syl 14 |
. . 3
⊢
((A ∪ B) = (A ∩
B) → (A ⊆ B
∧ B
⊆ A)) |
12 | | eqss 2954 |
. . 3
⊢ (A = B ↔
(A ⊆ B ∧ B ⊆ A)) |
13 | 11, 12 | sylibr 137 |
. 2
⊢
((A ∪ B) = (A ∩
B) → A = B) |
14 | | unidm 3080 |
. . . 4
⊢ (A ∪ A) =
A |
15 | | inidm 3140 |
. . . 4
⊢ (A ∩ A) =
A |
16 | 14, 15 | eqtr4i 2060 |
. . 3
⊢ (A ∪ A) =
(A ∩ A) |
17 | | uneq2 3085 |
. . 3
⊢ (A = B →
(A ∪ A) = (A ∪
B)) |
18 | | ineq2 3126 |
. . 3
⊢ (A = B →
(A ∩ A) = (A ∩
B)) |
19 | 16, 17, 18 | 3eqtr3a 2093 |
. 2
⊢ (A = B →
(A ∪ B) = (A ∩
B)) |
20 | 13, 19 | impbii 117 |
1
⊢
((A ∪ B) = (A ∩
B) ↔ A = B) |