Theorem inass 4170

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

Syntax hints:   ∧ wa 398   = wceq 1550   ∈ wcel 2132   ∩ cin 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-in 3902

This theorem is referenced by:  in12  4171  in32  4172  in4  4176  indif2  4224  difun1  4242  dfrab3ss  4266  dfif4  4486  resres  5967  inres  5972  imainrect  6152  cnvrescnv  6167  predidm  6298  onfr  6370  fresaun  6720  fresaunres2  6721  fimacnvinrn2  7038  epfrs  9672  incexclem  15838  sadeq  16478  smuval2  16488  smumul  16499  ressinbas  17253  ressress  17255  resscatc  18114  sylow2a  19631  ablfac1eu  20087  ressmplbas2  22048  restco  23193  restopnb  23204  kgeni  23566  hausdiag  23674  fclsrest  24053  clsocv  25281  itg2cnlem2  25793  rplogsum  27557  chjassi  31624  pjoml2i  31723  cmcmlem  31729  cmbr3i  31738  fh1  31756  fh2  31757  pj3lem1  32344  dmdbr5  32446  mdslmd3i  32470  mdexchi  32473  atabsi  32539  dmdbr6ati  32561  prsss  34157  inelcarsg  34552  carsgclctunlem1  34558  msrid  35833  dfttc4  36828  redundss3  39149  refrelsredund4  39153  dfpetparts2  39409  dfpeters2  39411  osumcllem9N  40526  dihmeetbclemN  41866  dihmeetlem11N  41879  wfac8prim  45516  inabs3  45574  uzinico2  46075  caragenuncllem  47024  resinsn  49431  restclsseplem  49474