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

Theorem sselii 3305
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 3304 . 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 1721    C_ wss 3280
This theorem is referenced by:  fvrn0  5712  brtpos0  6445  rdg0  6638  iunfi  7353  rankdmr1  7683  rankeq0b  7742  cardprclem  7822  alephfp2  7946  dfac2  7967  sdom2en01  8138  fin56  8229  fin1a2lem10  8245  hsmexlem4  8265  canthp1lem2  8484  ax1cn  8980  recni  9058  0xr  9087  nn0rei  10188  nnzi  10261  nn0zi  10262  pnfxr  10669  ccatfn  11696  lbsextlem4  16188  qsubdrg  16706  leordtval2  17230  iooordt  17235  hauspwdom  17517  dfac14  17603  filcon  17868  isufil2  17893  iooretop  18753  ovolfiniun  19350  volfiniun  19394  iblabslem  19672  iblabs  19673  bddmulibl  19683  mdegcl  19945  logcn  20491  logccv  20507  leibpi  20735  xrlimcnp  20760  jensen  20780  emre  20797  lgsdir2lem3  21062  shelii  22670  chelii  22689  omlsilem  22857  nonbooli  23106  pjssmii  23136  riesz4  23520  riesz1  23521  cnlnadjeu  23534  nmopadjlei  23544  adjeq0  23547  qqh0  24321  qqh1  24322  qqhcn  24328  esumcst  24408  volmeas  24540  kur14lem7  24851  kur14lem9  24853  iinllycon  24894  wfrlem14  25483  wfrlem16  25485  ftc1cnnclem  26177  areacirclem4  26183  comppfsc  26277  prdsbnd  26392  reheibor  26438  rmxyadd  26874  rmxy1  26875  rmxy0  26876  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  mpaaeu  27223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator