Theorem inass 4179

Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)

Assertion

Ref	Expression
inass	⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

Proof of Theorem inass

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anass 473	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
2		elin 3920	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
3	2	anbi2i 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	1, 3	bitr4i 281	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
5		elin 3920	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	anbi1i 635	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶))
7		elin 3920	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
8	4, 6, 7	3bitr4i 306	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)))
9	8	ineqri 4164	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

Syntax hints:   ∧ wa 400   = wceq 1568   ∈ wcel 2141   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911

This theorem is referenced by:  in12  4180  in32  4181  in4  4185  indif2  4233  difun1  4251  dfrab3ss  4275  dfif4  4502  resres  5991  inres  5996  imainrect  6179  cnvrescnv  6194  predidm  6327  onfr  6400  fresaun  6749  fresaunres2  6750  fimacnvinrn2  7067  epfrs  9699  incexclem  15889  sadeq  16529  smuval2  16539  smumul  16550  ressinbas  17304  ressress  17306  resscatc  18165  sylow2a  19688  ablfac1eu  20144  ressmplbas2  22156  restco  23300  restopnb  23311  kgeni  23673  hausdiag  23781  fclsrest  24160  clsocv  25388  itg2cnlem2  25900  rplogsum  27667  chjassi  31804  pjoml2i  31903  cmcmlem  31909  cmbr3i  31918  fh1  31936  fh2  31937  pj3lem1  32524  dmdbr5  32626  mdslmd3i  32650  mdexchi  32653  atabsi  32719  dmdbr6ati  32741  prsss  34272  inelcarsg  34667  carsgclctunlem1  34673  msrid  35991  dfttc4  36985  redundss3  39307  refrelsredund4  39311  dfpetparts2  39567  dfpeters2  39569  osumcllem9N  40684  dihmeetbclemN  42024  dihmeetlem11N  42037  wfac8prim  45659  inabs3  45724  uzinico2  46225  caragenuncllem  47174  resinsn  49595  restclsseplem  49638