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

Theorem sselii 3414
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 3413 . 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 1826    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  sseliALT  4498  fvrn0  5796  ovima0  6353  brtpos0  6880  rdg0  7005  iunfi  7723  rankdmr1  8132  rankeq0b  8191  cardprclem  8273  alephfp2  8403  dfac2  8424  sdom2en01  8595  fin56  8686  fin1a2lem10  8702  hsmexlem4  8722  canthp1lem2  8942  ax1cn  9437  recni  9519  0xr  9551  nn0rei  10723  nnzi  10805  nn0zi  10806  pnfxr  11242  ccatfnOLD  12500  lbsextlem4  17920  qsubdrg  18583  leordtval2  19799  iooordt  19804  hauspwdom  20087  comppfsc  20118  dfac14  20204  filcon  20469  isufil2  20494  iooretop  21358  ovolfiniun  21997  volfiniun  22042  iblabslem  22319  iblabs  22320  bddmulibl  22330  mdegcl  22554  logcn  23115  logccv  23131  leibpi  23389  xrlimcnp  23415  jensen  23435  emre  23452  lgsdir2lem3  23717  shelii  26249  chelii  26268  omlsilem  26437  nonbooli  26686  pjssmii  26716  riesz4  27099  riesz1  27100  cnlnadjeu  27113  nmopadjlei  27123  adjeq0  27126  qqh0  28118  qqh1  28119  qqhcn  28125  esumcst  28211  esumrnmpt2  28216  volmeas  28359  kur14lem7  28845  kur14lem9  28847  iinllycon  28888  wfrlem16  29523  finixpnum  30203  ftc1cnnclem  30254  ftc2nc  30265  areacirclem2  30274  prdsbnd  30455  reheibor  30501  rmxyadd  31022  rmxy1  31023  rmxy0  31024  rmydioph  31122  rmxdioph  31124  expdiophlem2  31130  expdioph  31131  mpaaeu  31267  fprodge0  31763  fourierdlem85  32140  fourierdlem102  32157  fourierdlem114  32169  bj-pinftyccb  34971  bj-minftyccb  34975
  Copyright terms: Public domain W3C validator