Theorem inass 4158

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 470	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
2		elin 3900	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
3	2	anbi2i 630	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	1, 3	bitr4i 280	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
5		elin 3900	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	anbi1i 631	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶))
7		elin 3900	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
8	4, 6, 7	3bitr4i 305	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)))
9	8	ineqri 4143	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

Syntax hints:   ∧ wa 397   = wceq 1548   ∈ wcel 2121   ∩ cin 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3891

This theorem is referenced by:  in12  4159  in32  4160  in4  4164  indif2  4211  difun1  4229  dfrab3ss  4253  dfif4  4472  resres  5950  inres  5955  imainrect  6135  cnvrescnv  6149  predidm  6280  onfr  6352  fresaun  6701  fresaunres2  6702  fimacnvinrn2  7016  epfrs  9647  incexclem  15796  sadeq  16436  smuval2  16446  smumul  16457  ressinbas  17210  ressress  17212  resscatc  18071  sylow2a  19588  ablfac1eu  20044  ressmplbas2  22005  restco  23150  restopnb  23161  kgeni  23523  hausdiag  23631  fclsrest  24010  clsocv  25238  itg2cnlem2  25750  rplogsum  27511  chjassi  31577  pjoml2i  31676  cmcmlem  31682  cmbr3i  31691  fh1  31709  fh2  31710  pj3lem1  32297  dmdbr5  32399  mdslmd3i  32423  mdexchi  32426  atabsi  32492  dmdbr6ati  32514  prsss  34110  inelcarsg  34505  carsgclctunlem1  34511  msrid  35786  dfttc4  36771  redundss3  39092  refrelsredund4  39096  dfpetparts2  39352  dfpeters2  39354  osumcllem9N  40469  dihmeetbclemN  41809  dihmeetlem11N  41822  wfac8prim  45459  inabs3  45517  uzinico2  46018  caragenuncllem  46967  resinsn  49374  restclsseplem  49417