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

Theorem sslin 3709
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 3708 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3676 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3676 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3530 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 3460    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475
This theorem is referenced by:  ss2in  3710  ssres2  5290  ssrnres  5435  sbthlem7  7635  kmlem5  8537  canthnum  9030  ioodisj  11661  hashun3  12434  xpsc0  14939  dprdres  17054  dprd2da  17070  dmdprdsplit2lem  17073  cnprest  19768  isnrm3  19838  regsep2  19855  llycmpkgen2  20029  kqdisj  20211  regr1lem  20218  fclsbas  20500  fclscf  20504  flimfnfcls  20507  isfcf  20513  metdstri  21333  nulmbl2  21925  uniioombllem4  21973  volsup2  21992  volcn  21993  itg1climres  22099  limcresi  22267  limciun  22276  rlimcnp2  23274  rplogsum  23690  chssoc  26392  cmbr4i  26497  5oai  26557  3oalem6  26563  mdslmd4i  27230  atcvat4i  27294  imadifxp  27436  crefss  27830  pnfneige0  27911  onint1  29890  oninhaus  29891  cldbnd  30120  neibastop1  30153  neibastop2  30155  cntotbnd  30268  mapfzcons1  30625  coeq0i  30662  eldioph4b  30721  icccncfext  31644  srhmsubc  32752  fldc  32759  fldhmsubc  32760  rhmsubclem3  32764  srhmsubcOLD  32771  fldcOLD  32778  fldhmsubcOLD  32779  rhmsubcOLDlem4  32784  polcon3N  35516  osumcllem4N  35558  lcfrlem2  37145
  Copyright terms: Public domain W3C validator