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

Theorem sslin 3395
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 3394 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3361 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3361 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3219 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 3151    C_ wss 3152
This theorem is referenced by:  ss2in  3396  ssres2  4982  ssrnres  5116  sbthlem7  6977  kmlem5  7780  canthnum  8271  ioodisj  10765  hashun3  11366  xpsc0  13462  dprdres  15263  dprd2da  15277  dmdprdsplit2lem  15280  cnprest  17017  isnrm3  17087  regsep2  17104  llycmpkgen2  17245  kqdisj  17423  regr1lem  17430  fclsbas  17716  fclscf  17720  flimfnfcls  17723  isfcf  17729  metdstri  18355  nulmbl2  18894  uniioombllem4  18941  volsup2  18960  volcn  18961  itg1climres  19069  limcresi  19235  limciun  19244  rlimcnp2  20261  rplogsum  20676  chssoc  22075  cmbr4i  22180  5oai  22240  3oalem6  22246  mdslmd4i  22913  atcvat4i  22977  pnfneige0  23374  onint1  24888  oninhaus  24889  residcp  25077  cldbnd  26244  neibastop1  26308  neibastop2  26310  cntotbnd  26520  mapfzcons1  26794  coeq0i  26832  eldioph4b  26894  polcon3N  30106  osumcllem4N  30148  lcfrlem2  31733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator