Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > indi | Structured version Visualization version GIF version |
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 |
---|---|
indi | ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | andi 1004 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))) | |
2 | elin 4169 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
3 | elin 4169 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
4 | 2, 3 | orbi12i 911 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))) |
5 | 1, 4 | bitr4i 280 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶))) |
6 | elun 4125 | . . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
7 | 6 | anbi2i 624 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
8 | elun 4125 | . . 3 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶))) | |
9 | 5, 7, 8 | 3bitr4i 305 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))) |
10 | 9 | ineqri 4180 | 1 ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ∪ cun 3934 ∩ cin 3935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-un 3941 df-in 3943 |
This theorem is referenced by: indir 4252 difindi 4258 undisj2 4412 disjssun 4417 difdifdir 4437 disjpr2 4649 resundi 5867 fresaun 6549 elfiun 8894 unxpwdom 9053 kmlem2 9577 djuinf 9614 ackbij1lem1 9642 ackbij1lem2 9643 ssxr 10710 incexclem 15191 bitsinv1 15791 bitsinvp1 15798 bitsres 15822 paste 21902 unmbl 24138 ovolioo 24169 uniioombllem4 24187 volcn 24207 ellimc2 24475 lhop2 24612 ex-in 28204 eulerpartgbij 31630 poimirlem3 34910 poimirlem15 34922 asindmre 34992 iunrelexp0 40096 sge0resplit 42737 sge0split 42740 |
Copyright terms: Public domain | W3C validator |