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

Theorem inass 3543
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 631 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
2 elin 3522 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
32anbi2i 676 . . . 4  |-  ( ( x  e.  A  /\  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
41, 3bitr4i 244 . . 3  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
5 elin 3522 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
65anbi1i 677 . . 3  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C ) )
7 elin 3522 . . 3  |-  ( x  e.  ( A  i^i  ( B  i^i  C ) )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
84, 6, 73bitr4i 269 . 2  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  x  e.  ( A  i^i  ( B  i^i  C ) ) )
98ineqri 3526 1  |-  ( ( A  i^i  B )  i^i  C )  =  ( A  i^i  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725    i^i cin 3311
This theorem is referenced by:  in12  3544  in32  3545  in4  3549  indif2  3576  difun1  3593  dfrab3ss  3611  dfif4  3742  onfr  4612  resres  5151  inres  5156  imainrect  5304  fresaun  5606  fresaunres2  5607  epfrs  7659  incexclem  12608  sadeq  12976  smuval2  12986  smumul  12997  ressinbas  13517  ressress  13518  resscatc  14252  sylow2a  15245  ablfac1eu  15623  ressmplbas2  16510  restco  17220  restopnb  17231  kgeni  17561  hausdiag  17669  fclsrest  18048  clsocv  19196  itg2cnlem2  19646  rplogsum  21213  chjassi  22980  pjoml2i  23079  cmcmlem  23085  cmbr3i  23094  fh1  23112  fh2  23113  pj3lem1  23701  dmdbr5  23803  mdslmd3i  23827  mdexchi  23830  atabsi  23896  dmdbr6ati  23918  fimacnvinrn2  24040  predidm  25455  osumcllem9N  30698  dihmeetbclemN  32039  dihmeetlem11N  32052
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319
  Copyright terms: Public domain W3C validator