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

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

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 3813 . 2 (𝐴𝐵) ⊆ 𝐴
2 sstr2 3591 . 2 ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶))
31, 2ax-mp 5 1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3555  wss 3556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3563  df-ss 3570
This theorem is referenced by:  inss  3822  wfrlem4  7366  wfrlem5  7367  fipwuni  8279  ssfin4  9079  distop  20713  fctop  20721  cctop  20723  ntrin  20778  innei  20842  lly1stc  21212  txcnp  21336  isfild  21575  utoptop  21951  restmetu  22288  lecmi  28322  mdslj2i  29040  mdslmd1lem1  29045  mdslmd1lem2  29046  elpwincl1  29216  pnfneige0  29791  inelcarsg  30166  ballotlemfrc  30381  bnj1177  30803  bnj1311  30821  frrlem4  31505  frrlem5  31506  cldbnd  31984  neiin  31990  ontgval  32093  mblfinlem4  33102  pmodlem1  34633  pmodlem2  34634  pmod1i  34635  pmod2iN  34636  pmodl42N  34638  dochdmj1  36180  ssficl  37376  ntrclskb  37870  ntrclsk13  37872  ntrneik3  37897  ntrneik13  37899  ssinss1d  38718  icccncfext  39421  fourierdlem48  39694  fourierdlem49  39695  fourierdlem113  39759  caragendifcl  40051  omelesplit  40055  carageniuncllem2  40059  carageniuncl  40060
  Copyright terms: Public domain W3C validator