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

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

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 3981 . 2 (𝐴𝐵) ⊆ 𝐴
2 sstr2 3759 . 2 ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶))
31, 2ax-mp 5 1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3722  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737
This theorem is referenced by:  inss  3991  wfrlem4  7570  wfrlem4OLD  7571  wfrlem5  7572  fipwuni  8488  ssfin4  9334  distop  21020  fctop  21029  cctop  21031  ntrin  21086  innei  21150  lly1stc  21520  txcnp  21644  isfild  21882  utoptop  22258  restmetu  22595  lecmi  28801  mdslj2i  29519  mdslmd1lem1  29524  mdslmd1lem2  29525  elpwincl1  29695  pnfneige0  30337  inelcarsg  30713  ballotlemfrc  30928  bnj1177  31412  bnj1311  31430  frrlem5  32121  cldbnd  32658  neiin  32664  ontgval  32767  mblfinlem4  33782  pmodlem1  35654  pmodlem2  35655  pmod1i  35656  pmod2iN  35657  pmodl42N  35659  dochdmj1  37200  ssficl  38400  ntrclskb  38893  ntrclsk13  38895  ntrneik3  38920  ntrneik13  38922  ssinss1d  39735  icccncfext  40618  fourierdlem48  40888  fourierdlem49  40889  fourierdlem113  40953  caragendifcl  41248  omelesplit  41252  carageniuncllem2  41256  carageniuncl  41257
  Copyright terms: Public domain W3C validator