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

Theorem ssinss1 3685
Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
Assertion
Ref Expression
ssinss1  |-  ( A 
C_  C  ->  ( A  i^i  B )  C_  C )

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 3677 . 2  |-  ( A  i^i  B )  C_  A
2 sstr2 3470 . 2  |-  ( ( A  i^i  B ) 
C_  A  ->  ( A  C_  C  ->  ( A  i^i  B )  C_  C ) )
31, 2ax-mp 5 1  |-  ( A 
C_  C  ->  ( A  i^i  B )  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    i^i cin 3434    C_ wss 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-in 3442  df-ss 3449
This theorem is referenced by:  inss  3686  fipwuni  7786  ssfin4  8589  distop  18731  fctop  18739  cctop  18741  ntrin  18796  innei  18860  lly1stc  19231  txcnp  19324  isfild  19562  utoptop  19940  restmetu  20293  lecmi  25156  mdslj2i  25875  mdslmd1lem1  25880  mdslmd1lem2  25881  pnfneige0  26525  probdif  26946  ballotlemfrc  27052  wfrlem4  27870  wfrlem5  27871  frrlem4  27914  frrlem5  27915  ontgval  28420  mblfinlem4  28578  cldbnd  28668  neiin  28674  bnj1177  32314  bnj1311  32332  pmodlem1  33813  pmodlem2  33814  pmod1i  33815  pmod2iN  33816  pmodl42N  33818  dochdmj1  35358
  Copyright terms: Public domain W3C validator