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

Theorem sslin 3689
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 3688 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3656 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3656 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3506 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 3436    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-ss 3451
This theorem is referenced by:  ss2in  3690  ssres2  5148  ssrnres  5292  sbthlem7  7692  kmlem5  8586  canthnum  9076  ioodisj  11764  hashun3  12564  xpsc0  15459  dprdres  17654  dprd2da  17668  dmdprdsplit2lem  17671  cnprest  20297  isnrm3  20367  regsep2  20384  llycmpkgen2  20557  kqdisj  20739  regr1lem  20746  fclsbas  21028  fclscf  21032  flimfnfcls  21035  isfcf  21041  metdstri  21860  metdstriOLD  21875  nulmbl2  22482  uniioombllem4  22536  volsup2  22555  volcn  22556  itg1climres  22664  limcresi  22832  limciun  22841  rlimcnp2  23884  rplogsum  24357  chssoc  27141  cmbr4i  27246  5oai  27306  3oalem6  27312  mdslmd4i  27978  atcvat4i  28042  imadifxp  28208  crefss  28678  pnfneige0  28759  cldbnd  30981  neibastop1  31014  neibastop2  31016  onint1  31108  oninhaus  31109  cntotbnd  32048  polcon3N  33407  osumcllem4N  33449  lcfrlem2  35036  mapfzcons1  35484  coeq0i  35520  eldioph4b  35579  icccncfext  37591  srhmsubc  39382  fldc  39389  fldhmsubc  39390  rhmsubclem3  39394  srhmsubcALTV  39401  fldcALTV  39408  fldhmsubcALTV  39409  rhmsubcALTVlem4  39414
  Copyright terms: Public domain W3C validator