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 468	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
2		elin 3916	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
3	2	anbi2i 623	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	1, 3	bitr4i 278	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
5		elin 3916	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	anbi1i 624	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶))
7		elin 3916	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∩ 𝐶)))
8	4, 6, 7	3bitr4i 303	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 ∩ 𝐶)))
9	8	ineqri 4160	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2110   ∩ cin 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-in 3907

This theorem is referenced by:  in12  4177  in32  4178  in4  4182  indif2  4229  difun1  4247  dfrab3ss  4271  dfif4  4489  resres  5938  inres  5943  imainrect  6125  cnvrescnv  6139  predidm  6269  onfr  6341  fresaun  6690  fresaunres2  6691  fimacnvinrn2  7000  epfrs  9616  incexclem  15735  sadeq  16375  smuval2  16385  smumul  16396  ressinbas  17148  ressress  17150  resscatc  18008  sylow2a  19524  ablfac1eu  19980  ressmplbas2  21955  restco  23072  restopnb  23083  kgeni  23445  hausdiag  23553  fclsrest  23932  clsocv  25170  itg2cnlem2  25683  rplogsum  27458  chjassi  31456  pjoml2i  31555  cmcmlem  31561  cmbr3i  31570  fh1  31588  fh2  31589  pj3lem1  32176  dmdbr5  32278  mdslmd3i  32302  mdexchi  32305  atabsi  32371  dmdbr6ati  32393  prsss  33919  inelcarsg  34314  carsgclctunlem1  34320  msrid  35557  redundss3  38644  refrelsredund4  38648  osumcllem9N  39982  dihmeetbclemN  41322  dihmeetlem11N  41335  wfac8prim  45014  inabs3  45072  uzinico2  45580  caragenuncllem  46529  resinsn  48882  restclsseplem  48925