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

Theorem sslin 3683
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 3682 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3650 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3650 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3504 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 3434    C_ wss 3435
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 3078  df-in 3442  df-ss 3449
This theorem is referenced by:  ss2in  3684  ssres2  5244  ssrnres  5383  sbthlem7  7536  kmlem5  8433  canthnum  8926  ioodisj  11531  hashun3  12264  xpsc0  14616  dprdres  16646  dprd2da  16662  dmdprdsplit2lem  16665  cnprest  19024  isnrm3  19094  regsep2  19111  llycmpkgen2  19254  kqdisj  19436  regr1lem  19443  fclsbas  19725  fclscf  19729  flimfnfcls  19732  isfcf  19738  metdstri  20558  nulmbl2  21150  uniioombllem4  21198  volsup2  21217  volcn  21218  itg1climres  21324  limcresi  21492  limciun  21501  rlimcnp2  22492  rplogsum  22908  chssoc  25050  cmbr4i  25155  5oai  25215  3oalem6  25221  mdslmd4i  25888  atcvat4i  25952  imadifxp  26089  pnfneige0  26525  onint1  28438  oninhaus  28439  cldbnd  28668  neibastop1  28727  neibastop2  28729  cntotbnd  28842  mapfzcons1  29200  coeq0i  29238  eldioph4b  29297  polcon3N  33884  osumcllem4N  33926  lcfrlem2  35511
  Copyright terms: Public domain W3C validator