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

Theorem ssin 3298
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
StepHypRef Expression
1 elin 3266 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
21imbi2i 305 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  /\  x  e.  C ) ) )
32albii 1554 . . 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 836 . . . 4  |-  ( ( x  e.  A  -> 
( x  e.  B  /\  x  e.  C
) )  <->  ( (
x  e.  A  ->  x  e.  B )  /\  ( x  e.  A  ->  x  e.  C ) ) )
54albii 1554 . . 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 1592 . . 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 265 . 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 3092 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
9 dfss2 3092 . . 3  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
108, 9anbi12i 681 . 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 3092 . 2  |-  ( A 
C_  ( B  i^i  C )  <->  A. x ( x  e.  A  ->  x  e.  ( B  i^i  C
) ) )
127, 10, 113bitr4i 270 1  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    e. wcel 1621    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  ssini  3299  ssind  3300  uneqin  3327  disjpss  3412  trin  4020  pwin  4190  fin  5278  epfrs  7297  tcmin  7310  resscntz  14642  subgdmdprd  15104  tgval  16525  eltg3i  16531  innei  16694  cnprest2  16850  subislly  17039  lly1stc  17054  xkohaus  17179  xkoinjcn  17213  opnfbas  17369  supfil  17422  rnelfm  17480  tsmsres  17658  chabs2  21926  cmbr4i  22028  pjin3i  22604  mdbr2  22706  dmdbr2  22713  dmdbr5  22718  mdslle1i  22727  mdslle2i  22728  mdslj1i  22729  mdslj2i  22730  mdsl2i  22732  mdslmd1lem1  22735  mdslmd1lem2  22736  mdslmd1i  22739  mdslmd3i  22742  hatomistici  22772  chrelat2i  22775  cvexchlem  22778  mdsymlem1  22813  mdsymlem3  22815  mdsymlem6  22818  dmdbr5ati  22832  iccllyscon  22952  wfrlem4  23427  frrlem4  23452  dfps2  24455  toplat  24456  clsint  24679  eltintpar  25065  inttaror  25066  pgapspf2  25219  bsstrs  25312  heibor1lem  25699  dochexmidlem1  30554
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  df-ss 3089
  Copyright terms: Public domain W3C validator