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

Theorem sslin 3724
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 3723 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3691 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3691 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3545 1  |-  ( A 
C_  B  ->  ( C  i^i  A )  C_  ( C  i^i  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    i^i cin 3475    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  ss2in  3725  ssres2  5300  ssrnres  5445  sbthlem7  7633  kmlem5  8534  canthnum  9027  ioodisj  11650  hashun3  12420  xpsc0  14815  dprdres  16877  dprd2da  16893  dmdprdsplit2lem  16896  cnprest  19584  isnrm3  19654  regsep2  19671  llycmpkgen2  19814  kqdisj  19996  regr1lem  20003  fclsbas  20285  fclscf  20289  flimfnfcls  20292  isfcf  20298  metdstri  21118  nulmbl2  21710  uniioombllem4  21758  volsup2  21777  volcn  21778  itg1climres  21884  limcresi  22052  limciun  22061  rlimcnp2  23052  rplogsum  23468  chssoc  26118  cmbr4i  26223  5oai  26283  3oalem6  26289  mdslmd4i  26956  atcvat4i  27020  imadifxp  27159  pnfneige0  27597  onint1  29519  oninhaus  29520  cldbnd  29749  neibastop1  29808  neibastop2  29810  cntotbnd  29923  mapfzcons1  30281  coeq0i  30318  eldioph4b  30377  icccncfext  31254  polcon3N  34731  osumcllem4N  34773  lcfrlem2  36358
  Copyright terms: Public domain W3C validator