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

Theorem ssin 3550
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 3517 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
21imbi2i 304 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  /\  x  e.  C ) ) )
32albii 1575 . . 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 834 . . . 4  |-  ( ( x  e.  A  -> 
( x  e.  B  /\  x  e.  C
) )  <->  ( (
x  e.  A  ->  x  e.  B )  /\  ( x  e.  A  ->  x  e.  C ) ) )
54albii 1575 . . 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 1603 . . 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 264 . 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 3324 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
9 dfss2 3324 . . 3  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
108, 9anbi12i 679 . 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 3324 . 2  |-  ( A 
C_  ( B  i^i  C )  <->  A. x ( x  e.  A  ->  x  e.  ( B  i^i  C
) ) )
127, 10, 113bitr4i 269 1  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    e. wcel 1725    i^i cin 3306    C_ wss 3307
This theorem is referenced by:  ssini  3551  ssind  3552  uneqin  3579  disjpss  3665  trin  4299  pwin  4474  fin  5609  epfrs  7651  tcmin  7664  resscntz  15113  subgdmdprd  15575  tgval  17003  eltg3i  17009  innei  17172  cnprest2  17337  subislly  17527  lly1stc  17542  xkohaus  17668  xkoinjcn  17702  opnfbas  17857  supfil  17910  rnelfm  17968  tsmsres  18156  restmetu  18600  chabs2  23002  cmbr4i  23086  pjin3i  23680  mdbr2  23782  dmdbr2  23789  dmdbr5  23794  mdslle1i  23803  mdslle2i  23804  mdslj1i  23805  mdslj2i  23806  mdsl2i  23808  mdslmd1lem1  23811  mdslmd1lem2  23812  mdslmd1i  23815  mdslmd3i  23818  hatomistici  23848  chrelat2i  23851  cvexchlem  23854  mdsymlem1  23889  mdsymlem3  23891  mdsymlem6  23894  dmdbr5ati  23908  pnfneige0  24319  ballotlem2  24729  iccllyscon  24920  wfrlem4  25509  frrlem4  25534  heibor1lem  26450  dochexmidlem1  31989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-in 3314  df-ss 3321
  Copyright terms: Public domain W3C validator