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

Theorem ssinss1 3640
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 3632 . 2  |-  ( A  i^i  B )  C_  A
2 sstr2 3424 . 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 3388    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403
This theorem is referenced by:  inss  3641  fipwuni  7801  ssfin4  8603  distop  19582  fctop  19590  cctop  19592  ntrin  19647  innei  19712  lly1stc  20082  txcnp  20206  isfild  20444  utoptop  20822  restmetu  21175  lecmi  26637  mdslj2i  27355  mdslmd1lem1  27360  mdslmd1lem2  27361  elpwincl1  27539  pnfneige0  28087  inelcarsg  28438  ballotlemfrc  28648  wfrlem4  29511  wfrlem5  29512  frrlem4  29555  frrlem5  29556  ontgval  30049  mblfinlem4  30219  cldbnd  30310  neiin  30316  icccncfext  31856  fourierdlem48  32103  fourierdlem49  32104  fourierdlem113  32168  bnj1177  34409  bnj1311  34427  pmodlem1  35983  pmodlem2  35984  pmod1i  35985  pmod2iN  35986  pmodl42N  35988  dochdmj1  37530  ssficl  38183
  Copyright terms: Public domain W3C validator