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

Theorem inass 3381
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 3360 . . . . 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 3360 . . . 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 3360 . . 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 3364 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 1625    e. wcel 1686    i^i cin 3153
This theorem is referenced by:  in12  3382  in32  3383  in4  3387  indif2  3414  difun1  3430  dfrab3ss  3448  dfif4  3578  onfr  4433  resres  4970  inres  4975  imainrect  5121  fresaun  5414  fresaunres2  5415  epfrs  7415  incexclem  12297  sadeq  12665  smuval2  12675  smumul  12686  ressinbas  13206  ressress  13207  resscatc  13939  sylow2a  14932  ablfac1eu  15310  ressmplbas2  16201  restco  16897  restopnb  16908  kgeni  17234  hausdiag  17341  fclsrest  17721  clsocv  18679  itg2cnlem2  19119  rplogsum  20678  chjassi  22067  pjoml2i  22166  cmcmlem  22172  cmbr3i  22181  fh1  22199  fh2  22200  pj3lem1  22788  dmdbr5  22890  mdslmd3i  22914  mdexchi  22917  atabsi  22983  dmdbr6ati  23005  fimacnvinrn2  23202  predidm  24190  islimrs3  25592  islimrs4  25593  hdrmp  25717  osumcllem9N  30226  dihmeetbclemN  31567  dihmeetlem11N  31580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161
  Copyright terms: Public domain W3C validator