![]() |
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 472 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) | |
2 | elin 3897 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
3 | 2 | anbi2i 625 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
4 | 1, 3 | bitr4i 281 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
5 | elin 3897 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
6 | 5 | anbi1i 626 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶)) |
7 | elin 3897 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) | |
8 | 4, 6, 7 | 3bitr4i 306 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶))) |
9 | 8 | ineqri 4130 | 1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∩ cin 3880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 |
This theorem is referenced by: in12 4147 in32 4148 in4 4152 indif2 4197 difun1 4214 dfrab3ss 4233 dfif4 4440 resres 5831 inres 5836 imainrect 6005 cnvrescnv 6019 predidm 6138 onfr 6198 fresaun 6523 fresaunres2 6524 fimacnvinrn2 6818 epfrs 9157 incexclem 15183 sadeq 15811 smuval2 15821 smumul 15832 ressinbas 16552 ressress 16554 resscatc 17357 sylow2a 18736 ablfac1eu 19188 ressmplbas2 20695 restco 21769 restopnb 21780 kgeni 22142 hausdiag 22250 fclsrest 22629 clsocv 23854 itg2cnlem2 24366 rplogsum 26111 chjassi 29269 pjoml2i 29368 cmcmlem 29374 cmbr3i 29383 fh1 29401 fh2 29402 pj3lem1 29989 dmdbr5 30091 mdslmd3i 30115 mdexchi 30118 atabsi 30184 dmdbr6ati 30206 prsss 31269 inelcarsg 31679 carsgclctunlem1 31685 msrid 32905 redundss3 36023 refrelsredund4 36027 osumcllem9N 37260 dihmeetbclemN 38600 dihmeetlem11N 38613 inabs3 41690 uzinico2 42199 caragenuncllem 43151 |
Copyright terms: Public domain | W3C validator |