# 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 ${⊢}{A}\cap \left({B}\cup {C}\right)=\left({A}\cap {B}\right)\cup \left({A}\cap {C}\right)$

### Proof

Step Hyp Ref Expression
1 andi ${⊢}\left({x}\in {A}\wedge \left({x}\in {B}\vee {x}\in {C}\right)\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\vee \left({x}\in {A}\wedge {x}\in {C}\right)\right)$
2 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
3 elin ${⊢}{x}\in \left({A}\cap {C}\right)↔\left({x}\in {A}\wedge {x}\in {C}\right)$
4 2 3 orbi12i ${⊢}\left({x}\in \left({A}\cap {B}\right)\vee {x}\in \left({A}\cap {C}\right)\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\vee \left({x}\in {A}\wedge {x}\in {C}\right)\right)$
5 1 4 bitr4i ${⊢}\left({x}\in {A}\wedge \left({x}\in {B}\vee {x}\in {C}\right)\right)↔\left({x}\in \left({A}\cap {B}\right)\vee {x}\in \left({A}\cap {C}\right)\right)$
6 elun ${⊢}{x}\in \left({B}\cup {C}\right)↔\left({x}\in {B}\vee {x}\in {C}\right)$
7 6 anbi2i ${⊢}\left({x}\in {A}\wedge {x}\in \left({B}\cup {C}\right)\right)↔\left({x}\in {A}\wedge \left({x}\in {B}\vee {x}\in {C}\right)\right)$
8 elun ${⊢}{x}\in \left(\left({A}\cap {B}\right)\cup \left({A}\cap {C}\right)\right)↔\left({x}\in \left({A}\cap {B}\right)\vee {x}\in \left({A}\cap {C}\right)\right)$
9 5 7 8 3bitr4i ${⊢}\left({x}\in {A}\wedge {x}\in \left({B}\cup {C}\right)\right)↔{x}\in \left(\left({A}\cap {B}\right)\cup \left({A}\cap {C}\right)\right)$
10 9 ineqri ${⊢}{A}\cap \left({B}\cup {C}\right)=\left({A}\cap {B}\right)\cup \left({A}\cap {C}\right)$