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

Theorem ssin 3716
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 3683 . . . . 5  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
21imbi2i 312 . . . 4  |-  ( ( x  e.  A  ->  x  e.  ( B  i^i  C ) )  <->  ( x  e.  A  ->  ( x  e.  B  /\  x  e.  C ) ) )
32albii 1641 . . 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 863 . . . 4  |-  ( ( x  e.  A  -> 
( x  e.  B  /\  x  e.  C
) )  <->  ( (
x  e.  A  ->  x  e.  B )  /\  ( x  e.  A  ->  x  e.  C ) ) )
54albii 1641 . . 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 1681 . . 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 272 . 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 3488 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
9 dfss2 3488 . . 3  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
108, 9anbi12i 697 . 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 3488 . 2  |-  ( A 
C_  ( B  i^i  C )  <->  A. x ( x  e.  A  ->  x  e.  ( B  i^i  C
) ) )
127, 10, 113bitr4i 277 1  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1393    e. wcel 1819    i^i cin 3470    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485
This theorem is referenced by:  ssini  3717  ssind  3718  uneqin  3756  disjpss  3880  trin  4560  pwin  4793  fin  5771  epfrs  8179  tcmin  8189  resscntz  16495  subgdmdprd  17207  tgval  19582  eltg3i  19588  innei  19752  cnprest2  19917  subislly  20107  lly1stc  20122  xkohaus  20279  xkoinjcn  20313  opnfbas  20468  supfil  20521  rnelfm  20579  tsmsresOLD  20770  tsmsres  20771  restmetu  21215  chabs2  26561  cmbr4i  26645  pjin3i  27239  mdbr2  27341  dmdbr2  27348  dmdbr5  27353  mdslle1i  27362  mdslle2i  27363  mdslj1i  27364  mdslj2i  27365  mdsl2i  27367  mdslmd1lem1  27370  mdslmd1lem2  27371  mdslmd1i  27374  mdslmd3i  27377  hatomistici  27407  chrelat2i  27410  cvexchlem  27413  mdsymlem1  27448  mdsymlem3  27450  mdsymlem6  27453  dmdbr5ati  27467  pnfneige0  28086  ballotlem2  28602  iccllyscon  28870  wfrlem4  29520  frrlem4  29564  heibor1lem  30467  dochexmidlem1  37288  superficl  37853
  Copyright terms: Public domain W3C validator