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

Theorem inass 3354
Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
Assertion
Ref Expression
inass  |-  ( ( A  i^i  B )  i^i  C )  =  ( A  i^i  ( B  i^i  C ) )

Proof of Theorem inass
StepHypRef Expression
1 anass 633 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
2 elin 3333 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
32anbi2i 678 . . . 4  |-  ( ( x  e.  A  /\  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
41, 3bitr4i 245 . . 3  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
5 elin 3333 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
65anbi1i 679 . . 3  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C ) )
7 elin 3333 . . 3  |-  ( x  e.  ( A  i^i  ( B  i^i  C ) )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
84, 6, 73bitr4i 270 . 2  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  x  e.  ( A  i^i  ( B  i^i  C ) ) )
98ineqri 3337 1  |-  ( ( A  i^i  B )  i^i  C )  =  ( A  i^i  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1619    e. wcel 1621    i^i cin 3126
This theorem is referenced by:  in12  3355  in32  3356  in4  3360  indif2  3387  difun1  3403  dfrab3ss  3421  dfif4  3550  onfr  4403  resres  4956  inres  4961  imainrect  5107  fresaun  5350  fresaunres2  5351  epfrs  7381  sadeq  12626  smuval2  12636  smumul  12647  ressinbas  13167  ressress  13168  resscatc  13900  sylow2a  14893  ablfac1eu  15271  ressmplbas2  16162  restco  16858  restopnb  16869  kgeni  17195  hausdiag  17302  fclsrest  17682  clsocv  18640  itg2cnlem2  19080  rplogsum  20639  chjassi  22026  pjoml2i  22125  cmcmlem  22131  cmbr3i  22140  fh1  22158  fh2  22159  pj3lem1  22747  dmdbr5  22849  mdslmd3i  22873  mdexchi  22876  atabsi  22942  dmdbr6ati  22964  predidm  23558  islimrs3  24949  islimrs4  24950  hdrmp  25074  osumcllem9N  29403  dihmeetbclemN  30744  dihmeetlem11N  30757
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134
  Copyright terms: Public domain W3C validator