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

Theorem sslin 3553
Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
Assertion
Ref Expression
sslin

Proof of Theorem sslin
StepHypRef Expression
1 ssrin 3552 . 2
2 incom 3520 . 2
3 incom 3520 . 2
41, 2, 33sstr4g 3374 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  i^icin 3304  C_wss 3305
This theorem is referenced by:  ss2in  3554  ssres2  5109  ssrnres  5248  sbthlem7  7386  kmlem5  8270  canthnum  8762  ioodisj  11359  hashun3  12088  xpsc0  14438  dprdres  16395  dprd2da  16409  dmdprdsplit2lem  16412  cnprest  18597  isnrm3  18667  regsep2  18684  llycmpkgen2  18827  kqdisj  19009  regr1lem  19016  fclsbas  19298  fclscf  19302  flimfnfcls  19305  isfcf  19311  metdstri  20127  nulmbl2  20718  uniioombllem4  20766  volsup2  20785  volcn  20786  itg1climres  20892  limcresi  21060  limciun  21069  rlimcnp2  22101  rplogsum  22517  chssoc  24578  cmbr4i  24683  5oai  24743  3oalem6  24749  mdslmd4i  25416  atcvat4i  25480  imadifxp  25619  pnfneige0  26090  onint1  27998  oninhaus  27999  cldbnd  28192  neibastop1  28251  neibastop2  28253  cntotbnd  28366  mapfzcons1  28726  coeq0i  28764  eldioph4b  28823  polcon3N  32998  osumcllem4N  33040  lcfrlem2  34625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-v 2953  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator