|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > inass | Structured version Visualization version GIF version | ||
| Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) | 
| Ref | Expression | 
|---|---|
| inass | ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | anass 468 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) | |
| 2 | elin 3966 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
| 3 | 2 | anbi2i 623 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) | 
| 4 | 1, 3 | bitr4i 278 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) | 
| 5 | elin 3966 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 6 | 5 | anbi1i 624 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶)) | 
| 7 | elin 3966 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) | |
| 8 | 4, 6, 7 | 3bitr4i 303 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶))) | 
| 9 | 8 | ineqri 4211 | 1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∩ cin 3949 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-in 3957 | 
| This theorem is referenced by: in12 4228 in32 4229 in4 4233 indif2 4280 difun1 4298 dfrab3ss 4322 dfif4 4540 resres 6009 inres 6014 imainrect 6200 cnvrescnv 6214 predidm 6346 onfr 6422 fresaun 6778 fresaunres2 6779 fimacnvinrn2 7091 epfrs 9772 incexclem 15873 sadeq 16510 smuval2 16520 smumul 16531 ressinbas 17292 ressress 17294 resscatc 18155 sylow2a 19638 ablfac1eu 20094 ressmplbas2 22046 restco 23173 restopnb 23184 kgeni 23546 hausdiag 23654 fclsrest 24033 clsocv 25285 itg2cnlem2 25798 rplogsum 27572 chjassi 31506 pjoml2i 31605 cmcmlem 31611 cmbr3i 31620 fh1 31638 fh2 31639 pj3lem1 32226 dmdbr5 32328 mdslmd3i 32352 mdexchi 32355 atabsi 32421 dmdbr6ati 32443 prsss 33916 inelcarsg 34314 carsgclctunlem1 34320 msrid 35551 redundss3 38630 refrelsredund4 38634 osumcllem9N 39967 dihmeetbclemN 41307 dihmeetlem11N 41320 wfac8prim 45024 inabs3 45066 uzinico2 45580 caragenuncllem 46532 resinsn 48778 restclsseplem 48819 | 
| Copyright terms: Public domain | W3C validator |