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

Theorem ssin 3391
Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
ssin  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )

Proof of Theorem ssin
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elin 3358 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
21imbi2i 303 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  /\  x  e.  C ) ) )
32albii 1553 . . 3  |-  ( A. x ( x  e.  A  ->  x  e.  ( B  i^i  C ) )  <->  A. x ( x  e.  A  ->  (
x  e.  B  /\  x  e.  C )
) )
4 jcab 833 . . . 4  |-  ( ( x  e.  A  -> 
( x  e.  B  /\  x  e.  C
) )  <->  ( (
x  e.  A  ->  x  e.  B )  /\  ( x  e.  A  ->  x  e.  C ) ) )
54albii 1553 . . 3  |-  ( A. x ( x  e.  A  ->  ( x  e.  B  /\  x  e.  C ) )  <->  A. x
( ( x  e.  A  ->  x  e.  B )  /\  (
x  e.  A  ->  x  e.  C )
) )
6 19.26 1580 . . 3  |-  ( A. x ( ( x  e.  A  ->  x  e.  B )  /\  (
x  e.  A  ->  x  e.  C )
)  <->  ( A. x
( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  A  ->  x  e.  C )
) )
73, 5, 63bitrri 263 . 2  |-  ( ( A. x ( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  A  ->  x  e.  C ) )  <->  A. x
( x  e.  A  ->  x  e.  ( B  i^i  C ) ) )
8 dfss2 3169 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
9 dfss2 3169 . . 3  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
108, 9anbi12i 678 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  <->  ( A. x ( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  A  ->  x  e.  C ) ) )
11 dfss2 3169 . 2  |-  ( A 
C_  ( B  i^i  C )  <->  A. x ( x  e.  A  ->  x  e.  ( B  i^i  C
) ) )
127, 10, 113bitr4i 268 1  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    e. wcel 1684    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  ssini  3392  ssind  3393  uneqin  3420  disjpss  3505  trin  4123  pwin  4297  fin  5421  epfrs  7413  tcmin  7426  resscntz  14807  subgdmdprd  15269  tgval  16693  eltg3i  16699  innei  16862  cnprest2  17018  subislly  17207  lly1stc  17222  xkohaus  17347  xkoinjcn  17381  opnfbas  17537  supfil  17590  rnelfm  17648  tsmsres  17826  chabs2  22096  cmbr4i  22180  pjin3i  22774  mdbr2  22876  dmdbr2  22883  dmdbr5  22888  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  mdsl2i  22902  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd1i  22909  mdslmd3i  22912  hatomistici  22942  chrelat2i  22945  cvexchlem  22948  mdsymlem1  22983  mdsymlem3  22985  mdsymlem6  22988  dmdbr5ati  23002  ballotlem2  23047  pnfneige0  23374  iccllyscon  23781  wfrlem4  24259  frrlem4  24284  dfps2  25289  toplat  25290  clsint  25513  eltintpar  25899  inttaror  25900  pgapspf2  26053  bsstrs  26146  heibor1lem  26533  dochexmidlem1  31650
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator