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

Theorem sselii 3177
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 3176 . 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 1684    C_ wss 3152
This theorem is referenced by:  fvrn0  5550  brtpos0  6241  rdg0  6434  iunfi  7144  rankdmr1  7473  rankeq0b  7532  cardprclem  7612  alephfp2  7736  dfac2  7757  sdom2en01  7928  fin56  8019  fin1a2lem10  8035  hsmexlem4  8055  canthp1lem2  8275  ax1cn  8771  recni  8849  0xr  8878  nn0rei  9976  nnzi  10047  nn0zi  10048  pnfxr  10455  ccatfn  11427  tanhbnd  12441  lbsextlem4  15914  qsubdrg  16424  leordtval2  16942  iooordt  16947  hauspwdom  17227  dfac14  17312  filcon  17578  isufil2  17603  iooretop  18275  oprpiece1res2  18450  pcoass  18522  ovolfiniun  18860  volfiniun  18904  vitalilem4  18966  iblabslem  19182  iblabs  19183  bddmulibl  19193  mdegcl  19455  sincosq4sgn  19869  tanabsge  19874  sinq12gt0  19875  cosq14gt0  19878  tanord1  19899  tanregt0  19901  ellogrn  19917  argregt0  19964  argimgt0  19966  argimlt0  19967  logcn  19994  dvloglem  19995  logccv  20010  asinneg  20182  asinsinlem  20187  acoscos  20189  reasinsin  20192  atanlogsublem  20211  atanbndlem  20221  atanbnd  20222  atan1  20224  leibpi  20238  xrlimcnp  20263  scvxcvx  20280  jensen  20283  emre  20299  basellem4  20321  lgsdir2lem3  20564  pntibndlem2  20740  padicabvf  20780  padicabvcxp  20781  shelii  21794  chelii  21813  omlsilem  21981  nonbooli  22230  pjssmii  22260  riesz4  22644  riesz1  22645  cnlnadjeu  22658  nmopadjlei  22668  adjeq0  22671  kur14lem7  23154  kur14lem9  23156  iinllycon  23196  umgrafi  23285  wfrlem14  23680  wfrlem16  23682  areacirclem4  24339  intopcoaconlem3  24951  phpf  25462  pspf  25463  comppfsc  25719  prdsbnd  25929  reheibor  25975  rmxyadd  26418  rmxy1  26419  rmxy0  26420  rmydioph  26519  rmxdioph  26521  expdiophlem2  26527  expdioph  26528  mpaaeu  26767  wallispilem2  27227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator