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

Theorem inass 3380
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 3359 . . . . 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 3359 . . . 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 3359 . . 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 3363 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 1623    e. wcel 1685    i^i cin 3152
This theorem is referenced by:  in12  3381  in32  3382  in4  3386  indif2  3413  difun1  3429  dfrab3ss  3447  dfif4  3577  onfr  4430  resres  4967  inres  4972  imainrect  5118  fresaun  5378  fresaunres2  5379  epfrs  7409  incexclem  12291  sadeq  12659  smuval2  12669  smumul  12680  ressinbas  13200  ressress  13201  resscatc  13933  sylow2a  14926  ablfac1eu  15304  ressmplbas2  16195  restco  16891  restopnb  16902  kgeni  17228  hausdiag  17335  fclsrest  17715  clsocv  18673  itg2cnlem2  19113  rplogsum  20672  chjassi  22061  pjoml2i  22160  cmcmlem  22166  cmbr3i  22175  fh1  22193  fh2  22194  pj3lem1  22782  dmdbr5  22884  mdslmd3i  22908  mdexchi  22911  atabsi  22977  dmdbr6ati  22999  predidm  23592  islimrs3  24992  islimrs4  24993  hdrmp  25117  osumcllem9N  29432  dihmeetbclemN  30773  dihmeetlem11N  30786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator