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

Theorem sslin 3559
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 3558 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3525 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3525 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3381 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 3311    C_ wss 3312
This theorem is referenced by:  ss2in  3560  ssres2  5165  ssrnres  5301  sbthlem7  7215  kmlem5  8026  canthnum  8516  ioodisj  11018  hashun3  11650  xpsc0  13777  dprdres  15578  dprd2da  15592  dmdprdsplit2lem  15595  cnprest  17345  isnrm3  17415  regsep2  17432  llycmpkgen2  17574  kqdisj  17756  regr1lem  17763  fclsbas  18045  fclscf  18049  flimfnfcls  18052  isfcf  18058  metdstri  18873  nulmbl2  19423  uniioombllem4  19470  volsup2  19489  volcn  19490  itg1climres  19598  limcresi  19764  limciun  19773  rlimcnp2  20797  rplogsum  21213  chssoc  22990  cmbr4i  23095  5oai  23155  3oalem6  23161  mdslmd4i  23828  atcvat4i  23892  imadifxp  24030  pnfneige0  24328  onint1  26191  oninhaus  26192  cldbnd  26320  neibastop1  26379  neibastop2  26381  cntotbnd  26496  mapfzcons1  26764  coeq0i  26802  eldioph4b  26863  polcon3N  30651  osumcllem4N  30693  lcfrlem2  32278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator