Metamath Proof Explorer


Theorem indi

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 ABC=ABAC

Proof

Step Hyp Ref Expression
1 andi xAxBxCxAxBxAxC
2 elin xABxAxB
3 elin xACxAxC
4 2 3 orbi12i xABxACxAxBxAxC
5 1 4 bitr4i xAxBxCxABxAC
6 elun xBCxBxC
7 6 anbi2i xAxBCxAxBxC
8 elun xABACxABxAC
9 5 7 8 3bitr4i xAxBCxABAC
10 9 ineqri ABC=ABAC