Theorem inass 4176

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909

This theorem is used by:  in12  4177  in32  4178  in4  4182  indif2  4230  difun1  4248  dfrab3ss  4272  dfif4  4501  resres  5989  inres  5994  imainrect  6178  cnvrescnv  6193  predidm  6328  onfr  6401  fresaun  6750  fresaunres2  6751  fimacnvinrn2  7068  epfrs  9713  incexclem  15927  sadeq  16566  smuval2  16576  smumul  16587  ressinbas  17341  ressress  17343  resscatc  18202  sylow2a  19747  ablfac1eu  20203  ressmplbas2  22243  restco  23390  restopnb  23401  kgeni  23764  hausdiag  23872  fclsrest  24251  clsocv  25479  itg2cnlem2  25991  rplogsum  27761  chjassi  31953  pjoml2i  32052  cmcmlem  32058  cmbr3i  32067  fh1  32085  fh2  32086  pj3lem1  32673  dmdbr5  32775  mdslmd3i  32799  mdexchi  32802  atabsi  32868  dmdbr6ati  32890  prsss  34413  inelcarsg  34809  carsgclctunlem1  34815  msrid  36111  dfttc4  37136  redundss3  39447  refrelsredund4  39451  dfpetparts2  39707  dfpeters2  39709  osumcllem9N  40824  dihmeetbclemN  42164  dihmeetlem11N  42177  wfac8prim  45812  inabs3  45877  uzinico2  46378  caragenuncllem  47327  resinsn  49785  restclsseplem  49828