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

Theorem sslin 4208
Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
Assertion
Ref Expression
sslin (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))

Proof of Theorem sslin
StepHypRef Expression
1 ssrin 4207 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 incom 4175 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4175 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33sstr4g 4009 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3932  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949
This theorem is referenced by:  ss2in  4210  inxpssres  5565  ssres2  5874  sbthlem7  8621  kmlem5  9568  canthnum  10059  ioodisj  12856  hashun3  13733  dprdres  19079  dprd2da  19093  dmdprdsplit2lem  19096  cnprest  21825  isnrm3  21895  regsep2  21912  llycmpkgen2  22086  kqdisj  22268  regr1lem  22275  fclsbas  22557  fclscf  22561  flimfnfcls  22564  isfcf  22570  metdstri  23386  nulmbl2  24064  uniioombllem4  24114  volsup2  24133  volcn  24134  itg1climres  24242  limcresi  24410  limciun  24419  rlimcnp2  25471  rplogsum  26030  chssoc  29200  cmbr4i  29305  5oai  29365  3oalem6  29371  mdslmd4i  30037  atcvat4i  30101  imadifxp  30279  swrdrndisj  30558  crefss  31012  pnfneige0  31093  cldbnd  33571  neibastop1  33604  neibastop2  33606  onint1  33694  oninhaus  33695  bj-idres  34344  cntotbnd  34955  polcon3N  36933  osumcllem4N  36975  lcfrlem2  38559  mapfzcons1  39192  coeq0i  39228  eldioph4b  39286  icccncfext  42046  srhmsubc  44275  fldc  44282  fldhmsubc  44283  rhmsubclem3  44287  srhmsubcALTV  44293  fldcALTV  44300  fldhmsubcALTV  44301  rhmsubcALTVlem4  44306
  Copyright terms: Public domain W3C validator