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

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

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 4158 . 2 (𝐴𝐵) ⊆ 𝐴
2 sstr2 3924 . 2 ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶))
31, 2ax-mp 5 1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-in 3890  df-ss 3900 This theorem is referenced by:  inss  4168  wfrlem4  7959  wfrlem5  7960  fipwuni  8892  ssfin4  9739  insubm  17995  distop  21641  fctop  21650  cctop  21652  ntrin  21707  innei  21771  lly1stc  22142  txcnp  22266  isfild  22504  utoptop  22881  restmetu  23218  lecmi  29429  mdslj2i  30147  mdslmd1lem1  30152  mdslmd1lem2  30153  elpwincl1  30342  pnfneige0  31370  inelcarsg  31745  ballotlemfrc  31960  bnj1177  32454  bnj1311  32472  cldbnd  33934  neiin  33940  ontgval  34039  mblfinlem4  35248  pmodlem1  37293  pmodlem2  37294  pmod1i  37295  pmod2iN  37296  pmodl42N  37298  dochdmj1  38837  ssficl  40439  ntrclskb  40943  ntrclsk13  40945  ntrneik3  40970  ntrneik13  40972  ssinss1d  41853  icccncfext  42697  fourierdlem48  42964  fourierdlem49  42965  fourierdlem113  43029  caragendifcl  43321  omelesplit  43325  carageniuncllem2  43329  carageniuncl  43330
 Copyright terms: Public domain W3C validator