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

Theorem sselii 3190
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 3189 . 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 1696    C_ wss 3165
This theorem is referenced by:  fvrn0  5566  brtpos0  6257  rdg0  6450  iunfi  7160  rankdmr1  7489  rankeq0b  7548  cardprclem  7628  alephfp2  7752  dfac2  7773  sdom2en01  7944  fin56  8035  fin1a2lem10  8051  hsmexlem4  8071  canthp1lem2  8291  ax1cn  8787  recni  8865  0xr  8894  nn0rei  9992  nnzi  10063  nn0zi  10064  pnfxr  10471  ccatfn  11443  tanhbnd  12457  lbsextlem4  15930  qsubdrg  16440  leordtval2  16958  iooordt  16963  hauspwdom  17243  dfac14  17328  filcon  17594  isufil2  17619  iooretop  18291  oprpiece1res2  18466  pcoass  18538  ovolfiniun  18876  volfiniun  18920  vitalilem4  18982  iblabslem  19198  iblabs  19199  bddmulibl  19209  mdegcl  19471  sincosq4sgn  19885  tanabsge  19890  sinq12gt0  19891  cosq14gt0  19894  tanord1  19915  tanregt0  19917  ellogrn  19933  argregt0  19980  argimgt0  19982  argimlt0  19983  logcn  20010  dvloglem  20011  logccv  20026  asinneg  20198  asinsinlem  20203  acoscos  20205  reasinsin  20208  atanlogsublem  20227  atanbndlem  20237  atanbnd  20238  atan1  20240  leibpi  20254  xrlimcnp  20279  scvxcvx  20296  jensen  20299  emre  20315  basellem4  20337  lgsdir2lem3  20580  pntibndlem2  20756  padicabvf  20796  padicabvcxp  20797  shelii  21810  chelii  21829  omlsilem  21997  nonbooli  22246  pjssmii  22276  riesz4  22660  riesz1  22661  cnlnadjeu  22674  nmopadjlei  22684  adjeq0  22687  xrge0iifcnv  23330  esumcst  23451  kur14lem7  23758  kur14lem9  23760  iinllycon  23800  umgrafi  23889  wfrlem14  24340  wfrlem16  24342  ftc1cnnclem  25024  areacirclem4  25030  intopcoaconlem3  25642  phpf  26153  pspf  26154  comppfsc  26410  prdsbnd  26620  reheibor  26666  rmxyadd  27109  rmxy1  27110  rmxy0  27111  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  mpaaeu  27458  wallispilem2  27918
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator