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

Theorem ssinss1 3984
Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
Assertion
Ref Expression
ssinss1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 3976 . 2 (𝐴𝐵) ⊆ 𝐴
2 sstr2 3751 . 2 ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶))
31, 2ax-mp 5 1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3714  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729
This theorem is referenced by:  inss  3985  wfrlem4  7588  wfrlem5  7589  fipwuni  8499  ssfin4  9344  distop  21021  fctop  21030  cctop  21032  ntrin  21087  innei  21151  lly1stc  21521  txcnp  21645  isfild  21883  utoptop  22259  restmetu  22596  lecmi  28791  mdslj2i  29509  mdslmd1lem1  29514  mdslmd1lem2  29515  elpwincl1  29685  pnfneige0  30327  inelcarsg  30703  ballotlemfrc  30918  bnj1177  31402  bnj1311  31420  frrlem5  32111  cldbnd  32648  neiin  32654  ontgval  32757  mblfinlem4  33780  pmodlem1  35653  pmodlem2  35654  pmod1i  35655  pmod2iN  35656  pmodl42N  35658  dochdmj1  37199  ssficl  38394  ntrclskb  38887  ntrclsk13  38889  ntrneik3  38914  ntrneik13  38916  ssinss1d  39731  icccncfext  40621  fourierdlem48  40892  fourierdlem49  40893  fourierdlem113  40957  caragendifcl  41252  omelesplit  41256  carageniuncllem2  41260  carageniuncl  41261
  Copyright terms: Public domain W3C validator