Theorem inass 4180

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 472	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
2		elin 3921	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
3	2	anbi2i 632	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	1, 3	bitr4i 280	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
5		elin 3921	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	anbi1i 633	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶))
7		elin 3921	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
8	4, 6, 7	3bitr4i 305	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)))
9	8	ineqri 4165	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

Syntax hints:   ∧ wa 399   = wceq 1561   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  in12  4181  in32  4182  in4  4186  indif2  4234  difun1  4252  dfrab3ss  4276  dfif4  4497  resres  5978  inres  5983  imainrect  6167  cnvrescnv  6182  predidm  6313  onfr  6385  fresaun  6735  fresaunres2  6736  fimacnvinrn2  7053  epfrs  9684  incexclem  15876  sadeq  16516  smuval2  16526  smumul  16537  ressinbas  17291  ressress  17293  resscatc  18152  sylow2a  19669  ablfac1eu  20125  ressmplbas2  22086  restco  23231  restopnb  23242  kgeni  23604  hausdiag  23712  fclsrest  24091  clsocv  25319  itg2cnlem2  25831  rplogsum  27598  chjassi  31696  pjoml2i  31795  cmcmlem  31801  cmbr3i  31810  fh1  31828  fh2  31829  pj3lem1  32416  dmdbr5  32518  mdslmd3i  32542  mdexchi  32545  atabsi  32611  dmdbr6ati  32633  prsss  34215  inelcarsg  34610  carsgclctunlem1  34616  msrid  35900  dfttc4  36895  redundss3  39216  refrelsredund4  39220  dfpetparts2  39476  dfpeters2  39478  osumcllem9N  40593  dihmeetbclemN  41933  dihmeetlem11N  41946  wfac8prim  45569  inabs3  45627  uzinico2  46128  caragenuncllem  47077  resinsn  49484  restclsseplem  49527