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

Theorem ssinss1 3726
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 3718 . 2  |-  ( A  i^i  B )  C_  A
2 sstr2 3511 . 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 3475    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  inss  3727  fipwuni  7886  ssfin4  8690  distop  19291  fctop  19299  cctop  19301  ntrin  19356  innei  19420  lly1stc  19791  txcnp  19884  isfild  20122  utoptop  20500  restmetu  20853  lecmi  26224  mdslj2i  26943  mdslmd1lem1  26948  mdslmd1lem2  26949  pnfneige0  27597  probdif  28027  ballotlemfrc  28133  wfrlem4  28951  wfrlem5  28952  frrlem4  28995  frrlem5  28996  ontgval  29501  mblfinlem4  29659  cldbnd  29749  neiin  29755  fourierdlem48  31483  fourierdlem49  31484  fourierdlem113  31548  bnj1177  33159  bnj1311  33177  pmodlem1  34660  pmodlem2  34661  pmod1i  34662  pmod2iN  34663  pmodl42N  34665  dochdmj1  36205  ssficl  36792
  Copyright terms: Public domain W3C validator