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

Theorem inass 3286
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
StepHypRef Expression
1 anass 633 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
2 elin 3266 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
32anbi2i 678 . . . 4  |-  ( ( x  e.  A  /\  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  /\  x  e.  C )
) )
41, 3bitr4i 245 . . 3  |-  ( ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
5 elin 3266 . . . 4  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
65anbi1i 679 . . 3  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  ( ( x  e.  A  /\  x  e.  B
)  /\  x  e.  C ) )
7 elin 3266 . . 3  |-  ( x  e.  ( A  i^i  ( B  i^i  C ) )  <->  ( x  e.  A  /\  x  e.  ( B  i^i  C
) ) )
84, 6, 73bitr4i 270 . 2  |-  ( ( x  e.  ( A  i^i  B )  /\  x  e.  C )  <->  x  e.  ( A  i^i  ( B  i^i  C ) ) )
98ineqri 3270 1  |-  ( ( A  i^i  B )  i^i  C )  =  ( A  i^i  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1619    e. wcel 1621    i^i cin 3077
This theorem is referenced by:  in12  3287  in32  3288  in4  3292  indif2  3319  difun1  3335  dfrab3ss  3353  dfif4  3481  onfr  4324  resres  4875  inres  4880  imainrect  5026  fresaun  5269  fresaunres2  5270  epfrs  7297  sadeq  12537  smuval2  12547  smumul  12558  ressinbas  13078  ressress  13079  resscatc  13781  sylow2a  14765  ablfac1eu  15143  ressmplbas2  16031  restco  16727  restopnb  16738  kgeni  17064  hausdiag  17171  fclsrest  17551  clsocv  18509  itg2cnlem2  18949  rplogsum  20508  chjassi  21895  pjoml2i  22012  cmcmlem  22018  cmbr3i  22027  fh1  22045  fh2  22046  pj3lem1  22616  dmdbr5  22718  mdslmd3i  22742  mdexchi  22745  atabsi  22811  dmdbr6ati  22833  predidm  23356  islimrs3  24747  islimrs4  24748  hdrmp  24872  osumcllem9N  28954  dihmeetbclemN  30295  dihmeetlem11N  30308
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085
  Copyright terms: Public domain W3C validator