MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sselii Structured version   Unicode version

Theorem sselii 3345
Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseli.1  |-  A  C_  B
sselii.2  |-  C  e.  A
Assertion
Ref Expression
sselii  |-  C  e.  B

Proof of Theorem sselii
StepHypRef Expression
1 sselii.2 . 2  |-  C  e.  A
2 sseli.1 . . 3  |-  A  C_  B
32sseli 3344 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3ax-mp 8 1  |-  C  e.  B
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  fvrn0  5753  brtpos0  6486  rdg0  6679  iunfi  7394  rankdmr1  7727  rankeq0b  7786  cardprclem  7866  alephfp2  7990  dfac2  8011  sdom2en01  8182  fin56  8273  fin1a2lem10  8289  hsmexlem4  8309  canthp1lem2  8528  ax1cn  9024  recni  9102  0xr  9131  nn0rei  10232  nnzi  10305  nn0zi  10306  pnfxr  10713  ccatfn  11741  lbsextlem4  16233  qsubdrg  16751  leordtval2  17276  iooordt  17281  hauspwdom  17564  dfac14  17650  filcon  17915  isufil2  17940  iooretop  18800  ovolfiniun  19397  volfiniun  19441  iblabslem  19719  iblabs  19720  bddmulibl  19730  mdegcl  19992  logcn  20538  logccv  20554  leibpi  20782  xrlimcnp  20807  jensen  20827  emre  20844  lgsdir2lem3  21109  shelii  22717  chelii  22736  omlsilem  22904  nonbooli  23153  pjssmii  23183  riesz4  23567  riesz1  23568  cnlnadjeu  23581  nmopadjlei  23591  adjeq0  23594  qqh0  24368  qqh1  24369  qqhcn  24375  esumcst  24455  volmeas  24587  kur14lem7  24898  kur14lem9  24900  iinllycon  24941  wfrlem16  25553  ftc1cnnclem  26278  ftc2nc  26289  areacirclem2  26293  comppfsc  26387  prdsbnd  26502  reheibor  26548  rmxyadd  26984  rmxy1  26985  rmxy0  26986  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  expdioph  27094  mpaaeu  27332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator