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

Theorem sslin 3564
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 3563 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3531 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3531 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3385 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 3315    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330
This theorem is referenced by:  ss2in  3565  ssres2  5125  ssrnres  5264  sbthlem7  7415  kmlem5  8311  canthnum  8804  ioodisj  11402  hashun3  12131  xpsc0  14481  dprdres  16499  dprd2da  16515  dmdprdsplit2lem  16518  cnprest  18735  isnrm3  18805  regsep2  18822  llycmpkgen2  18965  kqdisj  19147  regr1lem  19154  fclsbas  19436  fclscf  19440  flimfnfcls  19443  isfcf  19449  metdstri  20269  nulmbl2  20860  uniioombllem4  20908  volsup2  20927  volcn  20928  itg1climres  21034  limcresi  21202  limciun  21211  rlimcnp2  22245  rplogsum  22661  chssoc  24722  cmbr4i  24827  5oai  24887  3oalem6  24893  mdslmd4i  25560  atcvat4i  25624  imadifxp  25763  pnfneige0  26235  onint1  28143  oninhaus  28144  cldbnd  28365  neibastop1  28424  neibastop2  28426  cntotbnd  28539  mapfzcons1  28898  coeq0i  28936  eldioph4b  28995  polcon3N  33155  osumcllem4N  33197  lcfrlem2  34782
  Copyright terms: Public domain W3C validator