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

Theorem ssinss1 3573
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 3565 . 2  |-  ( A  i^i  B )  C_  A
2 sstr2 3358 . 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 3322    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337
This theorem is referenced by:  inss  3574  fipwuni  7668  ssfin4  8471  distop  18580  fctop  18588  cctop  18590  ntrin  18645  innei  18709  lly1stc  19080  txcnp  19173  isfild  19411  utoptop  19789  restmetu  20142  lecmi  24973  mdslj2i  25692  mdslmd1lem1  25697  mdslmd1lem2  25698  pnfneige0  26350  probdif  26772  ballotlemfrc  26878  wfrlem4  27696  wfrlem5  27697  frrlem4  27740  frrlem5  27741  ontgval  28247  mblfinlem4  28402  cldbnd  28492  neiin  28498  bnj1177  31926  bnj1311  31944  pmodlem1  33383  pmodlem2  33384  pmod1i  33385  pmod2iN  33386  pmodl42N  33388  dochdmj1  34928
  Copyright terms: Public domain W3C validator