Theorem inass 4124

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091

This theorem is used by:  in12  4125  in32  4126  in4  4130  indif2  4226  difun1  4244  dfrab3ss  4268  dfif4  4497  resres  5982  inres  5987  imainrect  6172  cnvrescnv  6187  predidm  6329  onfr  6402  fresaun  6753  fresaunres2  6754  fimacnvinrn2  7072  epfrs  9732  incexclem  16005  sadeq  16642  smuval2  16652  smumul  16663  ressinbas  17423  ressress  17425  resscatc  18284  sylow2a  19833  ablfac1eu  20289  ressmplbas2  22335  restco  23482  restopnb  23493  kgeni  23856  hausdiag  23964  fclsrest  24343  clsocv  25571  itg2cnlem2  26083  rplogsum  27854  chjassi  32088  pjoml2i  32187  cmcmlem  32193  cmbr3i  32202  fh1  32220  fh2  32221  pj3lem1  32808  dmdbr5  32910  mdslmd3i  32934  mdexchi  32937  atabsi  33003  dmdbr6ati  33025  prsss  34590  inelcarsg  34985  carsgclctunlem1  34991  msrid  36352  dfttc4  37360  redundss3  39687  refrelsredund4  39691  dfpetparts2  39947  dfpeters2  39949  osumcllem9N  41064  dihmeetbclemN  42404  dihmeetlem11N  42417  wfac8prim  46035  inabs3  46116  uzinico2  46616  caragenuncllem  47565  resinsn  50023  restclsseplem  50066