Step |
Hyp |
Ref |
Expression |
1 |
|
indif1 |
⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) |
2 |
1
|
eqeq1i |
⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ ) |
3 |
|
ssdif0 |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ ) |
4 |
2 3
|
sylbb2 |
⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) |
5 |
4
|
adantr |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) |
6 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 |
7 |
6
|
a1i |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) |
8 |
5 7
|
ssind |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐵 ) ) |
9 |
|
indif1 |
⊢ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 ) |
10 |
9
|
eqeq1i |
⊢ ( ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ↔ ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 ) = ∅ ) |
11 |
|
ssdif0 |
⊢ ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 ) = ∅ ) |
12 |
10 11
|
sylbb2 |
⊢ ( ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 ) |
13 |
12
|
adantl |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 ) |
14 |
|
inss2 |
⊢ ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 |
15 |
14
|
a1i |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 ) |
16 |
13 15
|
ssind |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) ) |
17 |
8 16
|
eqssd |
⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ( 𝐶 ∩ 𝐵 ) ) |