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

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

Proof of Theorem ssinss1
StepHypRef Expression
1 inss1 4237 . 2 (𝐴𝐵) ⊆ 𝐴
2 sstr2 3990 . 2 ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶))
31, 2ax-mp 5 1 (𝐴𝐶 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cin 3950  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968
This theorem is referenced by:  ssinss1d  4247  inss  4248  inindif  4375  wfrlem4OLD  8352  wfrlem5OLD  8353  fipwuni  9466  ssfin4  10350  insubm  18831  distop  23002  fctop  23011  cctop  23013  ntrin  23069  innei  23133  lly1stc  23504  txcnp  23628  isfild  23866  utoptop  24243  restmetu  24583  lecmi  31621  mdslj2i  32339  mdslmd1lem1  32344  mdslmd1lem2  32345  elpwincl1  32544  pnfneige0  33950  inelcarsg  34313  ballotlemfrc  34529  bnj1177  35020  bnj1311  35038  cldbnd  36327  neiin  36333  ontgval  36432  mblfinlem4  37667  pmodlem1  39848  pmodlem2  39849  pmod1i  39850  pmod2iN  39851  pmodl42N  39853  dochdmj1  41392  redvmptabs  42390  ssficl  43582  ntrclskb  44082  ntrclsk13  44084  ntrneik3  44109  ntrneik13  44111  sswfaxreg  45004  icccncfext  45902  fourierdlem48  46169  fourierdlem49  46170  fourierdlem113  46234  caragendifcl  46529  omelesplit  46533  carageniuncllem2  46537  carageniuncl  46538
  Copyright terms: Public domain W3C validator