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

Theorem sslin 3690
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 3689 . 2
2 incom 3657 . 2
3 incom 3657 . 2
41, 2, 33sstr4g 3511 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  i^icin 3441  C_wss 3442
This theorem is referenced by:  ss2in  3691  ssres2  5254  ssrnres  5395  sbthlem7  7561  kmlem5  8460  canthnum  8953  ioodisj  11560  hashun3  12305  xpsc0  14657  dprdres  16700  dprd2da  16716  dmdprdsplit2lem  16719  cnprest  19292  isnrm3  19362  regsep2  19379  llycmpkgen2  19522  kqdisj  19704  regr1lem  19711  fclsbas  19993  fclscf  19997  flimfnfcls  20000  isfcf  20006  metdstri  20826  nulmbl2  21418  uniioombllem4  21466  volsup2  21485  volcn  21486  itg1climres  21592  limcresi  21760  limciun  21769  rlimcnp2  22760  rplogsum  23176  chssoc  25368  cmbr4i  25473  5oai  25533  3oalem6  25539  mdslmd4i  26206  atcvat4i  26270  imadifxp  26407  pnfneige0  26838  onint1  28751  oninhaus  28752  cldbnd  28981  neibastop1  29040  neibastop2  29042  cntotbnd  29155  mapfzcons1  29513  coeq0i  29551  eldioph4b  29610  icccncfext  30455  polcon3N  34412  osumcllem4N  34454  lcfrlem2  36039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-ss 3456
  Copyright terms: Public domain W3C validator