| 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 1010 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))) | |
| 2 | elin 3967 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 3 | elin 3967 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
| 4 | 2, 3 | orbi12i 915 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))) |
| 5 | 1, 4 | bitr4i 278 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶))) |
| 6 | elun 4153 | . . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
| 7 | 6 | anbi2i 623 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
| 8 | elun 4153 | . . 3 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶))) | |
| 9 | 5, 7, 8 | 3bitr4i 303 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))) |
| 10 | 9 | ineqri 4212 | 1 ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∪ cun 3949 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-in 3958 |
| This theorem is referenced by: indir 4286 difindi 4292 undisj2 4463 disjssun 4468 difdifdir 4492 disjpr2 4713 resundi 6011 fresaun 6779 elfiun 9470 unxpwdom 9629 kmlem2 10192 djuinf 10229 ackbij1lem1 10259 ackbij1lem2 10260 ssxr 11330 incexclem 15872 bitsinv1 16479 bitsinvp1 16486 bitsres 16510 paste 23302 unmbl 25572 ovolioo 25603 uniioombllem4 25621 volcn 25641 ellimc2 25912 lhop2 26054 ex-in 30444 eulerpartgbij 34374 poimirlem3 37630 poimirlem15 37642 asindmre 37710 iunrelexp0 43715 sge0resplit 46421 sge0split 46424 tposresg 48778 tposrescnv 48779 iscnrm3rlem1 48837 topdlat 48893 |
| Copyright terms: Public domain | W3C validator |