Description: Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | indifdi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | eldif | |
|
3 | 2 | anbi2i | |
4 | abai | |
|
5 | 4 | anbi2i | |
6 | an12 | |
|
7 | eldif | |
|
8 | elin | |
|
9 | 8 | bicomi | |
10 | imnan | |
|
11 | elin | |
|
12 | 10 11 | xchbinxr | |
13 | 9 12 | anbi12i | |
14 | an21 | |
|
15 | 7 13 14 | 3bitr2i | |
16 | 5 6 15 | 3bitr4i | |
17 | 1 3 16 | 3bitri | |
18 | 17 | eqriv | |