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

Theorem sslin 3527
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 3526 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3493 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3493 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3349 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 3279    C_ wss 3280
This theorem is referenced by:  ss2in  3528  ssres2  5132  ssrnres  5268  sbthlem7  7182  kmlem5  7990  canthnum  8480  ioodisj  10982  hashun3  11613  xpsc0  13740  dprdres  15541  dprd2da  15555  dmdprdsplit2lem  15558  cnprest  17307  isnrm3  17377  regsep2  17394  llycmpkgen2  17535  kqdisj  17717  regr1lem  17724  fclsbas  18006  fclscf  18010  flimfnfcls  18013  isfcf  18019  metdstri  18834  nulmbl2  19384  uniioombllem4  19431  volsup2  19450  volcn  19451  itg1climres  19559  limcresi  19725  limciun  19734  rlimcnp2  20758  rplogsum  21174  chssoc  22951  cmbr4i  23056  5oai  23116  3oalem6  23122  mdslmd4i  23789  atcvat4i  23853  imadifxp  23991  pnfneige0  24289  onint1  26103  oninhaus  26104  cldbnd  26219  neibastop1  26278  neibastop2  26280  cntotbnd  26395  mapfzcons1  26663  coeq0i  26701  eldioph4b  26762  polcon3N  30399  osumcllem4N  30441  lcfrlem2  32026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator