Theorem inass 4172

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 474	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
2		elin 3914	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
3	2	anbi2i 635	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	1, 3	bitr4i 281	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
5		elin 3914	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	anbi1i 636	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶))
7		elin 3914	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
8	4, 6, 7	3bitr4i 306	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)))
9	8	ineqri 4157	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∩ cin 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3905

This theorem is used by:  in12  4173  in32  4174  in4  4178  indif2  4226  difun1  4244  dfrab3ss  4268  dfif4  4497  resres  5979  inres  5984  imainrect  6168  cnvrescnv  6183  predidm  6318  onfr  6391  fresaun  6741  fresaunres2  6742  fimacnvinrn2  7060  epfrs  9710  incexclem  15972  sadeq  16609  smuval2  16619  smumul  16630  ressinbas  17384  ressress  17386  resscatc  18245  sylow2a  19794  ablfac1eu  20250  ressmplbas2  22296  restco  23443  restopnb  23454  kgeni  23817  hausdiag  23925  fclsrest  24304  clsocv  25532  itg2cnlem2  26044  rplogsum  27817  chjassi  32021  pjoml2i  32120  cmcmlem  32126  cmbr3i  32135  fh1  32153  fh2  32154  pj3lem1  32741  dmdbr5  32843  mdslmd3i  32867  mdexchi  32870  atabsi  32936  dmdbr6ati  32958  prsss  34481  inelcarsg  34877  carsgclctunlem1  34883  msrid  36231  dfttc4  37240  redundss3  39564  refrelsredund4  39568  dfpetparts2  39824  dfpeters2  39826  osumcllem9N  40941  dihmeetbclemN  42281  dihmeetlem11N  42294  wfac8prim  45929  inabs3  45994  uzinico2  46495  caragenuncllem  47444  resinsn  49902  restclsseplem  49945