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

Theorem sslin 3664
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 3663 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 incom 3631 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3631 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33sstr4g 3482 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 3412    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-in 3420  df-ss 3427
This theorem is referenced by:  ss2in  3665  ssres2  5241  ssrnres  5384  sbthlem7  7591  kmlem5  8486  canthnum  8977  ioodisj  11621  hashun3  12407  xpsc0  15066  dprdres  17287  dprd2da  17303  dmdprdsplit2lem  17306  cnprest  19975  isnrm3  20045  regsep2  20062  llycmpkgen2  20235  kqdisj  20417  regr1lem  20424  fclsbas  20706  fclscf  20710  flimfnfcls  20713  isfcf  20719  metdstri  21539  nulmbl2  22131  uniioombllem4  22179  volsup2  22198  volcn  22199  itg1climres  22305  limcresi  22473  limciun  22482  rlimcnp2  23514  rplogsum  23985  chssoc  26708  cmbr4i  26813  5oai  26873  3oalem6  26879  mdslmd4i  27545  atcvat4i  27609  imadifxp  27774  crefss  28185  pnfneige0  28266  cldbnd  30542  neibastop1  30575  neibastop2  30577  onint1  30669  oninhaus  30670  cntotbnd  31555  polcon3N  32915  osumcllem4N  32957  lcfrlem2  34544  mapfzcons1  34992  coeq0i  35028  eldioph4b  35087  icccncfext  37040  srhmsubc  38375  fldc  38382  fldhmsubc  38383  rhmsubclem3  38387  srhmsubcALTV  38394  fldcALTV  38401  fldhmsubcALTV  38402  rhmsubcALTVlem4  38407
  Copyright terms: Public domain W3C validator