Step |
Hyp |
Ref |
Expression |
1 |
|
eqimss |
⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) ) |
2 |
|
unss |
⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) ) |
3 |
|
ssin |
⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ↔ 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ) |
4 |
|
sstr |
⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 ) |
5 |
3 4
|
sylbir |
⊢ ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) → 𝐴 ⊆ 𝐵 ) |
6 |
|
ssin |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) ↔ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ) |
7 |
|
simpl |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) → 𝐵 ⊆ 𝐴 ) |
8 |
6 7
|
sylbir |
⊢ ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) → 𝐵 ⊆ 𝐴 ) |
9 |
5 8
|
anim12i |
⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ) |
10 |
2 9
|
sylbir |
⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ) |
11 |
1 10
|
syl |
⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ) |
12 |
|
eqss |
⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ) |
13 |
11 12
|
sylibr |
⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → 𝐴 = 𝐵 ) |
14 |
|
unidm |
⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴 |
15 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
16 |
14 15
|
eqtr4i |
⊢ ( 𝐴 ∪ 𝐴 ) = ( 𝐴 ∩ 𝐴 ) |
17 |
|
uneq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) ) |
18 |
|
ineq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) ) |
19 |
16 17 18
|
3eqtr3a |
⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ) |
20 |
13 19
|
impbii |
⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ↔ 𝐴 = 𝐵 ) |