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

Theorem sselii 3501
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 3500 . 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 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sseliALT  4578  fvrn0  5886  ovima0  6436  brtpos0  6959  rdg0  7084  iunfi  7804  rankdmr1  8215  rankeq0b  8274  cardprclem  8356  alephfp2  8486  dfac2  8507  sdom2en01  8678  fin56  8769  fin1a2lem10  8785  hsmexlem4  8805  canthp1lem2  9027  ax1cn  9522  recni  9604  0xr  9636  nn0rei  10802  nnzi  10884  nn0zi  10885  pnfxr  11317  ccatfn  12552  lbsextlem4  17590  qsubdrg  18238  leordtval2  19479  iooordt  19484  hauspwdom  19768  dfac14  19854  filcon  20119  isufil2  20144  iooretop  21008  ovolfiniun  21647  volfiniun  21692  iblabslem  21969  iblabs  21970  bddmulibl  21980  mdegcl  22204  logcn  22756  logccv  22772  leibpi  23001  xrlimcnp  23026  jensen  23046  emre  23063  lgsdir2lem3  23328  shelii  25808  chelii  25827  omlsilem  25996  nonbooli  26245  pjssmii  26275  riesz4  26659  riesz1  26660  cnlnadjeu  26673  nmopadjlei  26683  adjeq0  26686  qqh0  27601  qqh1  27602  qqhcn  27608  esumcst  27711  volmeas  27843  signsply0  28148  kur14lem7  28296  kur14lem9  28298  iinllycon  28339  wfrlem16  28935  finixpnum  29615  ftc1cnnclem  29665  ftc2nc  29676  areacirclem2  29685  comppfsc  29779  prdsbnd  29892  reheibor  29938  rmxyadd  30461  rmxy1  30462  rmxy0  30463  rmydioph  30560  rmxdioph  30562  expdiophlem2  30568  expdioph  30569  mpaaeu  30704  dirkeritg  31402  dirkercncflem2  31404  fourierdlem62  31469  fourierdlem85  31492  fourierdlem94  31501  fourierdlem101  31508  fourierdlem102  31509  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  fourierdlem114  31521  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  bj-pinftyccb  33696  bj-minftyccb  33700
  Copyright terms: Public domain W3C validator