# Metamath Proof Explorer

## Theorem undi

Description: Distributive law for union over intersection. Exercise 11 of TakeutiZaring p. 17. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion undi ${⊢}{A}\cup \left({B}\cap {C}\right)=\left({A}\cup {B}\right)\cap \left({A}\cup {C}\right)$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{x}\in \left({B}\cap {C}\right)↔\left({x}\in {B}\wedge {x}\in {C}\right)$
2 1 orbi2i ${⊢}\left({x}\in {A}\vee {x}\in \left({B}\cap {C}\right)\right)↔\left({x}\in {A}\vee \left({x}\in {B}\wedge {x}\in {C}\right)\right)$
3 ordi ${⊢}\left({x}\in {A}\vee \left({x}\in {B}\wedge {x}\in {C}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee {x}\in {C}\right)\right)$
4 elin ${⊢}{x}\in \left(\left({A}\cup {B}\right)\cap \left({A}\cup {C}\right)\right)↔\left({x}\in \left({A}\cup {B}\right)\wedge {x}\in \left({A}\cup {C}\right)\right)$
5 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
6 elun ${⊢}{x}\in \left({A}\cup {C}\right)↔\left({x}\in {A}\vee {x}\in {C}\right)$
7 5 6 anbi12i ${⊢}\left({x}\in \left({A}\cup {B}\right)\wedge {x}\in \left({A}\cup {C}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee {x}\in {C}\right)\right)$
8 4 7 bitr2i ${⊢}\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee {x}\in {C}\right)\right)↔{x}\in \left(\left({A}\cup {B}\right)\cap \left({A}\cup {C}\right)\right)$
9 2 3 8 3bitri ${⊢}\left({x}\in {A}\vee {x}\in \left({B}\cap {C}\right)\right)↔{x}\in \left(\left({A}\cup {B}\right)\cap \left({A}\cup {C}\right)\right)$
10 9 uneqri ${⊢}{A}\cup \left({B}\cap {C}\right)=\left({A}\cup {B}\right)\cap \left({A}\cup {C}\right)$