Theorem inass 4127

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  in12  4128  in32  4129  in4  4133  indif2  4229  difun1  4247  dfrab3ss  4271  dfif4  4501  resres  5994  inres  5999  imainrect  6185  cnvrescnv  6200  predidm  6347  onfr  6420  fresaun  6775  fresaunres2  6776  fimacnvinrn2  7096  epfrs  9759  incexclem  16034  sadeq  16671  smuval2  16681  smumul  16692  ressinbas  17452  ressress  17454  resscatc  18313  sylow2a  19863  ablfac1eu  20319  ressmplbas2  22365  restco  23512  restopnb  23523  kgeni  23886  hausdiag  23994  fclsrest  24373  clsocv  25601  itg2cnlem2  26113  rplogsum  27884  chjassi  32118  pjoml2i  32217  cmcmlem  32223  cmbr3i  32232  fh1  32250  fh2  32251  pj3lem1  32838  dmdbr5  32940  mdslmd3i  32964  mdexchi  32967  atabsi  33033  dmdbr6ati  33055  prsss  34618  inelcarsg  35013  carsgclctunlem1  35019  msrid  36477  dfttc4  37496  redundss3  39836  refrelsredund4  39840  dfpetparts2  40096  dfpeters2  40098  osumcllem9N  41213  dihmeetbclemN  42553  dihmeetlem11N  42566  wfac8prim  46187  inabs3  46278  uzinico2  46778  caragenuncllem  47727  resinsn  50190  restclsseplem  50234  parcatid2  50968  parcatid  50969