MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inass Structured version   Visualization version   GIF version

Theorem inass 4174
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.
StepHypRef Expression
1 anass 471 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3929 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 624 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 280 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3929 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 625 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3929 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 305 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 4158 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 398   = wceq 1537  wcel 2114  cin 3912
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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-in 3920
This theorem is referenced by:  in12  4175  in32  4176  in4  4180  indif2  4225  difun1  4242  dfrab3ss  4259  dfif4  4458  resres  5842  inres  5847  imainrect  6014  cnvrescnv  6028  predidm  6146  onfr  6206  fresaun  6525  fresaunres2  6526  fimacnvinrn2  6817  epfrs  9151  incexclem  15171  sadeq  15799  smuval2  15809  smumul  15820  ressinbas  16539  ressress  16541  resscatc  17344  sylow2a  18723  ablfac1eu  19174  ressmplbas2  20212  restco  21748  restopnb  21759  kgeni  22121  hausdiag  22229  fclsrest  22608  clsocv  23833  itg2cnlem2  24345  rplogsum  26090  chjassi  29248  pjoml2i  29347  cmcmlem  29353  cmbr3i  29362  fh1  29380  fh2  29381  pj3lem1  29968  dmdbr5  30070  mdslmd3i  30094  mdexchi  30097  atabsi  30163  dmdbr6ati  30185  prsss  31167  inelcarsg  31577  carsgclctunlem1  31583  msrid  32800  redundss3  35899  refrelsredund4  35903  osumcllem9N  37136  dihmeetbclemN  38476  dihmeetlem11N  38489  inabs3  41473  uzinico2  41990  caragenuncllem  42942
  Copyright terms: Public domain W3C validator