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

Theorem ssinss1 3672
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 3664 . 2  |-  ( A  i^i  B )  C_  A
2 sstr2 3451 . 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 3415    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430
This theorem is referenced by:  inss  3673  wfrlem4  7065  wfrlem5  7066  fipwuni  7966  ssfin4  8766  distop  20060  fctop  20068  cctop  20070  ntrin  20125  innei  20190  lly1stc  20560  txcnp  20684  isfild  20922  utoptop  21298  restmetu  21634  lecmi  27304  mdslj2i  28022  mdslmd1lem1  28027  mdslmd1lem2  28028  elpwincl1  28203  pnfneige0  28806  inelcarsg  29192  ballotlemfrc  29408  ballotlemfrcOLD  29446  bnj1177  29864  bnj1311  29882  frrlem4  30566  frrlem5  30567  cldbnd  31031  neiin  31037  ontgval  31140  mblfinlem4  32025  pmodlem1  33456  pmodlem2  33457  pmod1i  33458  pmod2iN  33459  pmodl42N  33461  dochdmj1  35003  ssficl  36218  ssinss1d  37423  icccncfext  37803  fourierdlem48  38056  fourierdlem49  38057  fourierdlem113  38121  caragendifcl  38373  omelesplit  38377  carageniuncllem2  38381  carageniuncl  38382
  Copyright terms: Public domain W3C validator