Step |
Hyp |
Ref |
Expression |
1 |
|
ineq1 |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 → ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ( 𝐶 ∩ 𝐵 ) ) |
2 |
|
disjdifr |
⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ |
3 |
1 2
|
eqtr3di |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 → ( 𝐶 ∩ 𝐵 ) = ∅ ) |
4 |
|
uneq1 |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 → ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐶 ∪ 𝐵 ) ) |
5 |
|
undif1 |
⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) |
6 |
4 5
|
eqtr3di |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 → ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) |
7 |
3 6
|
jca |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 → ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) ) |
8 |
|
simpl |
⊢ ( ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) → ( 𝐶 ∩ 𝐵 ) = ∅ ) |
9 |
|
disj3 |
⊢ ( ( 𝐶 ∩ 𝐵 ) = ∅ ↔ 𝐶 = ( 𝐶 ∖ 𝐵 ) ) |
10 |
|
eqcom |
⊢ ( 𝐶 = ( 𝐶 ∖ 𝐵 ) ↔ ( 𝐶 ∖ 𝐵 ) = 𝐶 ) |
11 |
9 10
|
bitri |
⊢ ( ( 𝐶 ∩ 𝐵 ) = ∅ ↔ ( 𝐶 ∖ 𝐵 ) = 𝐶 ) |
12 |
8 11
|
sylib |
⊢ ( ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) → ( 𝐶 ∖ 𝐵 ) = 𝐶 ) |
13 |
|
difeq1 |
⊢ ( ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → ( ( 𝐶 ∪ 𝐵 ) ∖ 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) |
14 |
|
difun2 |
⊢ ( ( 𝐶 ∪ 𝐵 ) ∖ 𝐵 ) = ( 𝐶 ∖ 𝐵 ) |
15 |
|
difun2 |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 ) |
16 |
13 14 15
|
3eqtr3g |
⊢ ( ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → ( 𝐶 ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 ) ) |
17 |
16
|
eqeq1d |
⊢ ( ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → ( ( 𝐶 ∖ 𝐵 ) = 𝐶 ↔ ( 𝐴 ∖ 𝐵 ) = 𝐶 ) ) |
18 |
17
|
adantl |
⊢ ( ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) → ( ( 𝐶 ∖ 𝐵 ) = 𝐶 ↔ ( 𝐴 ∖ 𝐵 ) = 𝐶 ) ) |
19 |
12 18
|
mpbid |
⊢ ( ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 ∖ 𝐵 ) = 𝐶 ) |
20 |
7 19
|
impbii |
⊢ ( ( 𝐴 ∖ 𝐵 ) = 𝐶 ↔ ( ( 𝐶 ∩ 𝐵 ) = ∅ ∧ ( 𝐶 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) ) ) |