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

Theorem sslin 3510
Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
Assertion
Ref Expression
sslin  |-  ( A 
C_  B  ->  ( C  i^i  A )  C_  ( C  i^i  B ) )

Proof of Theorem sslin
StepHypRef Expression
1 ssrin 3509 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3476 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3476 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3332 1  |-  ( A 
C_  B  ->  ( C  i^i  A )  C_  ( C  i^i  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    i^i cin 3262    C_ wss 3263
This theorem is referenced by:  ss2in  3511  ssres2  5113  ssrnres  5249  sbthlem7  7159  kmlem5  7967  canthnum  8457  ioodisj  10958  hashun3  11585  xpsc0  13712  dprdres  15513  dprd2da  15527  dmdprdsplit2lem  15530  cnprest  17275  isnrm3  17345  regsep2  17362  llycmpkgen2  17503  kqdisj  17685  regr1lem  17692  fclsbas  17974  fclscf  17978  flimfnfcls  17981  isfcf  17987  metdstri  18752  nulmbl2  19298  uniioombllem4  19345  volsup2  19364  volcn  19365  itg1climres  19473  limcresi  19639  limciun  19648  rlimcnp2  20672  rplogsum  21088  chssoc  22846  cmbr4i  22951  5oai  23011  3oalem6  23017  mdslmd4i  23684  atcvat4i  23748  imadifxp  23881  pnfneige0  24140  onint1  25913  oninhaus  25914  cldbnd  26020  neibastop1  26079  neibastop2  26081  cntotbnd  26196  mapfzcons1  26464  coeq0i  26502  eldioph4b  26563  polcon3N  30031  osumcllem4N  30073  lcfrlem2  31658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator