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

Theorem inass 3455
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 3434 . . . . 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 3434 . . . 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 3434 . . 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 3438 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 1642    e. wcel 1710    i^i cin 3227
This theorem is referenced by:  in12  3456  in32  3457  in4  3461  indif2  3488  difun1  3504  dfrab3ss  3522  dfif4  3652  onfr  4513  resres  5050  inres  5055  imainrect  5201  fresaun  5495  fresaunres2  5496  epfrs  7503  incexclem  12392  sadeq  12760  smuval2  12770  smumul  12781  ressinbas  13301  ressress  13302  resscatc  14036  sylow2a  15029  ablfac1eu  15407  ressmplbas2  16298  restco  17001  restopnb  17012  kgeni  17338  hausdiag  17445  fclsrest  17821  clsocv  18781  itg2cnlem2  19221  rplogsum  20788  chjassi  22179  pjoml2i  22278  cmcmlem  22284  cmbr3i  22293  fh1  22311  fh2  22312  pj3lem1  22900  dmdbr5  23002  mdslmd3i  23026  mdexchi  23029  atabsi  23095  dmdbr6ati  23117  fimacnvinrn2  23252  predidm  24746  osumcllem9N  30222  dihmeetbclemN  31563  dihmeetlem11N  31576
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235
  Copyright terms: Public domain W3C validator