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

Theorem sselii 3350
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 3349 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3ax-mp 5 1  |-  C  e.  B
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761    C_ wss 3325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339
This theorem is referenced by:  sseliALT  4420  fvrn0  5709  ovima0  6241  brtpos0  6751  rdg0  6873  iunfi  7595  rankdmr1  8004  rankeq0b  8063  cardprclem  8145  alephfp2  8275  dfac2  8296  sdom2en01  8467  fin56  8558  fin1a2lem10  8574  hsmexlem4  8594  canthp1lem2  8816  ax1cn  9312  recni  9394  0xr  9426  nn0rei  10586  nnzi  10666  nn0zi  10667  pnfxr  11088  ccatfn  12268  lbsextlem4  17220  qsubdrg  17824  leordtval2  18775  iooordt  18780  hauspwdom  19064  dfac14  19150  filcon  19415  isufil2  19440  iooretop  20304  ovolfiniun  20943  volfiniun  20987  iblabslem  21264  iblabs  21265  bddmulibl  21275  mdegcl  21499  logcn  22051  logccv  22067  leibpi  22296  xrlimcnp  22321  jensen  22341  emre  22358  lgsdir2lem3  22623  shelii  24552  chelii  24571  omlsilem  24740  nonbooli  24989  pjssmii  25019  riesz4  25403  riesz1  25404  cnlnadjeu  25417  nmopadjlei  25427  adjeq0  25430  qqh0  26349  qqh1  26350  qqhcn  26356  esumcst  26450  volmeas  26583  signsply0  26882  kur14lem7  27030  kur14lem9  27032  iinllycon  27073  wfrlem16  27668  finixpnum  28339  ftc1cnnclem  28390  ftc2nc  28401  areacirclem2  28410  comppfsc  28504  prdsbnd  28617  reheibor  28663  rmxyadd  29187  rmxy1  29188  rmxy0  29189  rmydioph  29288  rmxdioph  29290  expdiophlem2  29296  expdioph  29297  mpaaeu  29432  bj-pinftyccb  32273  bj-minftyccb  32277
  Copyright terms: Public domain W3C validator