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

Theorem sslin 3982
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 3981 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 incom 3948 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 3948 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33sstr4g 3787 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3714  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729
This theorem is referenced by:  ss2in  3983  ssres2  5583  ssrnres  5730  sbthlem7  8241  kmlem5  9168  canthnum  9663  ioodisj  12495  hashun3  13365  xpsc0  16422  dprdres  18627  dprd2da  18641  dmdprdsplit2lem  18644  cnprest  21295  isnrm3  21365  regsep2  21382  llycmpkgen2  21555  kqdisj  21737  regr1lem  21744  fclsbas  22026  fclscf  22030  flimfnfcls  22033  isfcf  22039  metdstri  22855  nulmbl2  23504  uniioombllem4  23554  volsup2  23573  volcn  23574  itg1climres  23680  limcresi  23848  limciun  23857  rlimcnp2  24892  rplogsum  25415  chssoc  28664  cmbr4i  28769  5oai  28829  3oalem6  28835  mdslmd4i  29501  atcvat4i  29565  imadifxp  29721  crefss  30225  pnfneige0  30306  cldbnd  32627  neibastop1  32660  neibastop2  32662  onint1  32754  oninhaus  32755  cntotbnd  33908  inxpssres  34400  polcon3N  35706  osumcllem4N  35748  lcfrlem2  37334  mapfzcons1  37782  coeq0i  37818  eldioph4b  37877  icccncfext  40603  srhmsubc  42586  fldc  42593  fldhmsubc  42594  rhmsubclem3  42598  srhmsubcALTV  42604  fldcALTV  42611  fldhmsubcALTV  42612  rhmsubcALTVlem4  42617
  Copyright terms: Public domain W3C validator