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

Theorem sslin 3408
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 3407 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3374 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3374 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3232 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 3164    C_ wss 3165
This theorem is referenced by:  ss2in  3409  ssres2  4998  ssrnres  5132  sbthlem7  6993  kmlem5  7796  canthnum  8287  ioodisj  10781  hashun3  11382  xpsc0  13478  dprdres  15279  dprd2da  15293  dmdprdsplit2lem  15296  cnprest  17033  isnrm3  17103  regsep2  17120  llycmpkgen2  17261  kqdisj  17439  regr1lem  17446  fclsbas  17732  fclscf  17736  flimfnfcls  17739  isfcf  17745  metdstri  18371  nulmbl2  18910  uniioombllem4  18957  volsup2  18976  volcn  18977  itg1climres  19085  limcresi  19251  limciun  19260  rlimcnp2  20277  rplogsum  20692  chssoc  22091  cmbr4i  22196  5oai  22256  3oalem6  22262  mdslmd4i  22929  atcvat4i  22993  pnfneige0  23389  onint1  24960  oninhaus  24961  residcp  25180  cldbnd  26347  neibastop1  26411  neibastop2  26413  cntotbnd  26623  mapfzcons1  26897  coeq0i  26935  eldioph4b  26997  polcon3N  30728  osumcllem4N  30770  lcfrlem2  32355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator