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

Theorem inass 3392
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 anass 630 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
2 elin 3371 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
32anbi2i 675 . . . 4  |-  ( ( x  e.  A  /\  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
41, 3bitr4i 243 . . 3  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
5 elin 3371 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
65anbi1i 676 . . 3  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C ) )
7 elin 3371 . . 3  |-  ( x  e.  ( A  i^i  ( B  i^i  C ) )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
84, 6, 73bitr4i 268 . 2  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  x  e.  ( A  i^i  ( B  i^i  C ) ) )
98ineqri 3375 1  |-  ( ( A  i^i  B )  i^i  C )  =  ( A  i^i  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696    i^i cin 3164
This theorem is referenced by:  in12  3393  in32  3394  in4  3398  indif2  3425  difun1  3441  dfrab3ss  3459  dfif4  3589  onfr  4447  resres  4984  inres  4989  imainrect  5135  fresaun  5428  fresaunres2  5429  epfrs  7429  incexclem  12311  sadeq  12679  smuval2  12689  smumul  12700  ressinbas  13220  ressress  13221  resscatc  13953  sylow2a  14946  ablfac1eu  15324  ressmplbas2  16215  restco  16911  restopnb  16922  kgeni  17248  hausdiag  17355  fclsrest  17735  clsocv  18693  itg2cnlem2  19133  rplogsum  20692  chjassi  22081  pjoml2i  22180  cmcmlem  22186  cmbr3i  22195  fh1  22213  fh2  22214  pj3lem1  22802  dmdbr5  22904  mdslmd3i  22928  mdexchi  22931  atabsi  22997  dmdbr6ati  23019  fimacnvinrn2  23215  predidm  24259  islimrs3  25684  islimrs4  25685  hdrmp  25809  osumcllem9N  30775  dihmeetbclemN  32116  dihmeetlem11N  32129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator