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

Theorem ssinss1 3725
Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
Assertion
Ref Expression
ssinss1

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 3717 . 2
2 sstr2 3510 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  i^icin 3474  C_wss 3475
This theorem is referenced by:  inss  3726  fipwuni  7906  ssfin4  8711  distop  19497  fctop  19505  cctop  19507  ntrin  19562  innei  19626  lly1stc  19997  txcnp  20121  isfild  20359  utoptop  20737  restmetu  21090  lecmi  26520  mdslj2i  27239  mdslmd1lem1  27244  mdslmd1lem2  27245  pnfneige0  27933  ballotlemfrc  28465  wfrlem4  29346  wfrlem5  29347  frrlem4  29390  frrlem5  29391  ontgval  29896  mblfinlem4  30054  cldbnd  30144  neiin  30150  icccncfext  31690  fourierdlem48  31937  fourierdlem49  31938  fourierdlem113  32002  bnj1177  34062  bnj1311  34080  pmodlem1  35570  pmodlem2  35571  pmod1i  35572  pmod2iN  35573  pmodl42N  35575  dochdmj1  37117  ssficl  37754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator