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

Theorem ssin 3404
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 3371 . . . . 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 1556 . . 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 1556 . . 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 1583 . . 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 3182 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
9 dfss2 3182 . . 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 3182 . 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 1530    e. wcel 1696    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  ssini  3405  ssind  3406  uneqin  3433  disjpss  3518  trin  4139  pwin  4313  fin  5437  epfrs  7429  tcmin  7442  resscntz  14823  subgdmdprd  15285  tgval  16709  eltg3i  16715  innei  16878  cnprest2  17034  subislly  17223  lly1stc  17238  xkohaus  17363  xkoinjcn  17397  opnfbas  17553  supfil  17606  rnelfm  17664  tsmsres  17842  chabs2  22112  cmbr4i  22196  pjin3i  22790  mdbr2  22892  dmdbr2  22899  dmdbr5  22904  mdslle1i  22913  mdslle2i  22914  mdslj1i  22915  mdslj2i  22916  mdsl2i  22918  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd1i  22925  mdslmd3i  22928  hatomistici  22958  chrelat2i  22961  cvexchlem  22964  mdsymlem1  22999  mdsymlem3  23001  mdsymlem6  23004  dmdbr5ati  23018  ballotlem2  23063  pnfneige0  23389  iccllyscon  23796  wfrlem4  24330  frrlem4  24355  dfps2  25392  toplat  25393  clsint  25616  eltintpar  26002  inttaror  26003  pgapspf2  26156  bsstrs  26249  heibor1lem  26636  dochexmidlem1  32272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator