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

Theorem sselii 3368
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 3367 . 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 1756    C_ wss 3343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3350  df-ss 3357
This theorem is referenced by:  sseliALT  4438  fvrn0  5727  ovima0  6257  brtpos0  6767  rdg0  6892  iunfi  7614  rankdmr1  8023  rankeq0b  8082  cardprclem  8164  alephfp2  8294  dfac2  8315  sdom2en01  8486  fin56  8577  fin1a2lem10  8593  hsmexlem4  8613  canthp1lem2  8835  ax1cn  9331  recni  9413  0xr  9445  nn0rei  10605  nnzi  10685  nn0zi  10686  pnfxr  11107  ccatfn  12287  lbsextlem4  17257  qsubdrg  17880  leordtval2  18831  iooordt  18836  hauspwdom  19120  dfac14  19206  filcon  19471  isufil2  19496  iooretop  20360  ovolfiniun  20999  volfiniun  21043  iblabslem  21320  iblabs  21321  bddmulibl  21331  mdegcl  21555  logcn  22107  logccv  22123  leibpi  22352  xrlimcnp  22377  jensen  22397  emre  22414  lgsdir2lem3  22679  shelii  24632  chelii  24651  omlsilem  24820  nonbooli  25069  pjssmii  25099  riesz4  25483  riesz1  25484  cnlnadjeu  25497  nmopadjlei  25507  adjeq0  25510  qqh0  26428  qqh1  26429  qqhcn  26435  esumcst  26529  volmeas  26662  signsply0  26967  kur14lem7  27115  kur14lem9  27117  iinllycon  27158  wfrlem16  27754  finixpnum  28433  ftc1cnnclem  28484  ftc2nc  28495  areacirclem2  28504  comppfsc  28598  prdsbnd  28711  reheibor  28757  rmxyadd  29281  rmxy1  29282  rmxy0  29283  rmydioph  29382  rmxdioph  29384  expdiophlem2  29390  expdioph  29391  mpaaeu  29526  bj-pinftyccb  32563  bj-minftyccb  32567
  Copyright terms: Public domain W3C validator