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

Theorem sslin 3571
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 3570 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3538 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3538 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3392 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 3322    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337
This theorem is referenced by:  ss2in  3572  ssres2  5132  ssrnres  5271  sbthlem7  7419  kmlem5  8315  canthnum  8808  ioodisj  11407  hashun3  12139  xpsc0  14490  dprdres  16513  dprd2da  16529  dmdprdsplit2lem  16532  cnprest  18868  isnrm3  18938  regsep2  18955  llycmpkgen2  19098  kqdisj  19280  regr1lem  19287  fclsbas  19569  fclscf  19573  flimfnfcls  19576  isfcf  19582  metdstri  20402  nulmbl2  20993  uniioombllem4  21041  volsup2  21060  volcn  21061  itg1climres  21167  limcresi  21335  limciun  21344  rlimcnp2  22335  rplogsum  22751  chssoc  24850  cmbr4i  24955  5oai  25015  3oalem6  25021  mdslmd4i  25688  atcvat4i  25752  imadifxp  25890  pnfneige0  26333  onint1  28247  oninhaus  28248  cldbnd  28474  neibastop1  28533  neibastop2  28535  cntotbnd  28648  mapfzcons1  29006  coeq0i  29044  eldioph4b  29103  polcon3N  33401  osumcllem4N  33443  lcfrlem2  35028
  Copyright terms: Public domain W3C validator