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 681 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) | |
2 | elin 3796 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
3 | 2 | anbi2i 730 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
4 | 1, 3 | bitr4i 267 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
5 | elin 3796 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
6 | 5 | anbi1i 731 | . . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶)) |
7 | elin 3796 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶))) | |
8 | 4, 6, 7 | 3bitr4i 292 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶))) |
9 | 8 | ineqri 3806 | 1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∩ cin 3573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 |
This theorem is referenced by: in12 3824 in32 3825 in4 3829 indif2 3870 difun1 3887 dfrab3ss 3905 dfif4 4101 resres 5409 inres 5414 imainrect 5575 predidm 5702 onfr 5763 fresaun 6075 fresaunres2 6076 fimacnvinrn2 6349 epfrs 8607 incexclem 14568 sadeq 15194 smuval2 15204 smumul 15215 ressinbas 15936 ressress 15938 resscatc 16755 sylow2a 18034 ablfac1eu 18472 ressmplbas2 19455 restco 20968 restopnb 20979 kgeni 21340 hausdiag 21448 fclsrest 21828 clsocv 23049 itg2cnlem2 23529 rplogsum 25216 chjassi 28345 pjoml2i 28444 cmcmlem 28450 cmbr3i 28459 fh1 28477 fh2 28478 pj3lem1 29065 dmdbr5 29167 mdslmd3i 29191 mdexchi 29194 atabsi 29260 dmdbr6ati 29282 prsss 29962 inelcarsg 30373 carsgclctunlem1 30379 msrid 31442 osumcllem9N 35250 dihmeetbclemN 36593 dihmeetlem11N 36606 inabs3 39224 uzinico2 39789 caragenuncllem 40726 |
Copyright terms: Public domain | W3C validator |