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

Theorem sslin 4195
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 4194 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 incom 4162 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4162 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33sstr4g 3990 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3910  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928
This theorem is referenced by:  ss2in  4197  inxpssres  5651  ssres2  5966  predrelss  6292  sbthlem7  9034  kmlem5  10091  canthnum  10586  ioodisj  13400  hashun3  14285  dprdres  19808  dprd2da  19822  dmdprdsplit2lem  19825  cnprest  22643  isnrm3  22713  regsep2  22730  llycmpkgen2  22904  kqdisj  23086  regr1lem  23093  fclsbas  23375  fclscf  23379  flimfnfcls  23382  isfcf  23388  metdstri  24217  nulmbl2  24903  uniioombllem4  24953  volsup2  24972  volcn  24973  itg1climres  25082  limcresi  25252  limciun  25261  rlimcnp2  26319  rplogsum  26878  chssoc  30441  cmbr4i  30546  5oai  30606  3oalem6  30612  mdslmd4i  31278  atcvat4i  31342  imadifxp  31522  swrdrndisj  31814  crefss  32433  pnfneige0  32535  cldbnd  34801  neibastop1  34834  neibastop2  34836  onint1  34924  oninhaus  34925  bj-idres  35634  cntotbnd  36258  polcon3N  38383  osumcllem4N  38425  lcfrlem2  40009  mapfzcons1  41043  coeq0i  41079  eldioph4b  41137  icccncfext  44135  srhmsubc  46381  fldc  46388  fldhmsubc  46389  rhmsubclem3  46393  srhmsubcALTV  46399  fldcALTV  46406  fldhmsubcALTV  46407  rhmsubcALTVlem4  46412  ssdisjdr  46900  sepnsepolem2  46962
  Copyright terms: Public domain W3C validator