Description: Distributive law for intersection over union. Exercise 10 of TakeutiZaring p. 17. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | indi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | andi | |
|
2 | elin | |
|
3 | elin | |
|
4 | 2 3 | orbi12i | |
5 | 1 4 | bitr4i | |
6 | elun | |
|
7 | 6 | anbi2i | |
8 | elun | |
|
9 | 5 7 8 | 3bitr4i | |
10 | 9 | ineqri | |