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

Theorem sslin 3987
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 3986 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 incom 3956 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 3956 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33sstr4g 3795 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3722  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737
This theorem is referenced by:  ss2in  3989  ssres2  5566  ssrnres  5713  sbthlem7  8232  kmlem5  9178  canthnum  9673  ioodisj  12509  hashun3  13375  xpsc0  16428  dprdres  18635  dprd2da  18649  dmdprdsplit2lem  18652  cnprest  21314  isnrm3  21384  regsep2  21401  llycmpkgen2  21574  kqdisj  21756  regr1lem  21763  fclsbas  22045  fclscf  22049  flimfnfcls  22052  isfcf  22058  metdstri  22874  nulmbl2  23524  uniioombllem4  23574  volsup2  23593  volcn  23594  itg1climres  23701  limcresi  23869  limciun  23878  rlimcnp2  24914  rplogsum  25437  chssoc  28695  cmbr4i  28800  5oai  28860  3oalem6  28866  mdslmd4i  29532  atcvat4i  29596  imadifxp  29752  crefss  30256  pnfneige0  30337  cldbnd  32658  neibastop1  32691  neibastop2  32693  onint1  32785  oninhaus  32786  cntotbnd  33927  inxpssres  34419  polcon3N  35725  osumcllem4N  35767  lcfrlem2  37353  mapfzcons1  37806  coeq0i  37842  eldioph4b  37901  icccncfext  40618  srhmsubc  42604  fldc  42611  fldhmsubc  42612  rhmsubclem3  42616  srhmsubcALTV  42622  fldcALTV  42629  fldhmsubcALTV  42630  rhmsubcALTVlem4  42635
  Copyright terms: Public domain W3C validator