Step |
Hyp |
Ref |
Expression |
1 |
|
sseqin2 |
⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐶 ∩ 𝐴 ) = 𝐴 ) |
2 |
1
|
biimpi |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐶 ∩ 𝐴 ) = 𝐴 ) |
3 |
|
incom |
⊢ ( 𝐶 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐶 ) |
4 |
2 3
|
eqtr3di |
⊢ ( 𝐴 ⊆ 𝐶 → 𝐴 = ( 𝐴 ∩ 𝐶 ) ) |
5 |
4
|
difeq1d |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∖ 𝐵 ) = ( ( 𝐴 ∩ 𝐶 ) ∖ 𝐵 ) ) |
6 |
|
difundi |
⊢ ( 𝐶 ∖ ( ( 𝐶 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) ∩ ( 𝐶 ∖ 𝐵 ) ) |
7 |
|
dfss4 |
⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) = 𝐴 ) |
8 |
7
|
biimpi |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) = 𝐴 ) |
9 |
8
|
ineq1d |
⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) ∩ ( 𝐶 ∖ 𝐵 ) ) = ( 𝐴 ∩ ( 𝐶 ∖ 𝐵 ) ) ) |
10 |
6 9
|
syl5eq |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐶 ∖ ( ( 𝐶 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( 𝐴 ∩ ( 𝐶 ∖ 𝐵 ) ) ) |
11 |
|
indif2 |
⊢ ( 𝐴 ∩ ( 𝐶 ∖ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∖ 𝐵 ) |
12 |
10 11
|
eqtrdi |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐶 ∖ ( ( 𝐶 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∖ 𝐵 ) ) |
13 |
5 12
|
eqtr4d |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∖ 𝐵 ) = ( 𝐶 ∖ ( ( 𝐶 ∖ 𝐴 ) ∪ 𝐵 ) ) ) |