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

Theorem elexi 2966
Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
elisseti.1  |-  A  e.  B
Assertion
Ref Expression
elexi  |-  A  e. 
_V

Proof of Theorem elexi
StepHypRef Expression
1 elisseti.1 . 2  |-  A  e.  B
2 elex 2965 . 2  |-  ( A  e.  B  ->  A  e.  _V )
31, 2ax-mp 8 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2957
This theorem is referenced by:  onunisuci  4696  fnprOLD  5952  caovmo  6285  oev  6759  oe0  6767  oev2  6768  oneo  6825  nnneo  6895  endisj  7196  pwen  7281  sdom1  7309  1sdom  7312  cnfcom2  7660  cnfcom3lem  7661  cnfcom3  7662  rankxplim3  7806  pm54.43  7888  mappwen  7994  cda1dif  8057  pm110.643  8058  infcda1  8074  infmap2  8099  ackbij1lem5  8105  cfsuc  8138  isfin4-3  8196  dcomex  8328  pwcfsdom  8459  cfpwsdom  8460  alephom  8461  canthp1lem2  8529  pwxpndom2  8541  inar1  8651  indpi  8785  pinq  8805  archnq  8858  prlem934  8911  0idsr  8973  recexsrlem  8979  supsrlem  8987  opelreal  9006  elreal  9007  elreal2  9008  eqresr  9013  axmulass  9033  ax1ne0  9036  c0ex  9086  1ex  9087  mnfxr  10715  elxr  10717  xnegex  10795  xaddval  10810  xmulval  10812  xrinfmss  10889  xrinfm0  10916  fzprval  11107  fztpval  11108  om2uzrdg  11297  hashgval  11622  hashinf  11624  hashf  11626  hashxplem  11697  caucvgr  12470  xpnnenOLD  12810  rpnnen  12827  rexpen  12828  ruclem11  12840  sadcf  12966  sadcp1  12968  phimullem  13169  pcval  13219  pc0  13229  prmreclem6  13290  ramcl2  13385  xpsc0  13786  xpsc1  13787  xpsfrnel  13789  xpsfrnel2  13791  xpsle  13807  setcepi  14244  efgval  15350  efgi1  15354  frgpuptinv  15404  dmdprdpr  15608  dprdpr  15609  coe1fval3  16607  00ply1bas  16635  ply1plusgfvi  16637  coe1z  16657  coe1mul2  16663  coe1tm  16666  xpstopnlem1  17842  xpstopnlem2  17844  xpsdsval  18412  dscmet  18621  dscopn  18622  icopnfhmeo  18969  iccpnfhmeo  18971  xrhmeo  18972  bndth  18984  mbfimaopnlem  19548  iblcnlem1  19680  dvef  19865  mdegcl  19993  iaa  20243  taylfval  20276  pige3  20426  cxpval  20556  1cubr  20683  xrlimcnp  20808  emcllem7  20841  basellem7  20870  basellem9  20872  prmorcht  20962  sqff1o  20966  ppiublem2  20988  lgsval  21085  lgsdir2lem3  21110  selberglem1  21240  usgraexmpl  21421  wlkntrllem2  21561  2pthlem2  21597  constr3lem2  21634  constr3lem4  21635  constr3lem5  21636  constr3trllem1  21638  vdgrf  21670  eupath  21704  umgrabi  21706  konigsberg  21710  ex-pss  21737  ex-opab  21741  ex-eprel  21742  ex-id  21743  ex-xp  21745  ex-cnv  21746  ex-dm  21748  ex-rn  21749  ex-res  21750  ex-ima  21751  ex-fv  21752  ex-1st  21753  ex-2nd  21754  hhph  22681  hlim0  22739  hsn0elch  22751  elch0  22757  choc0  22829  shintcli  22832  shincli  22865  chincli  22963  h1deoi  23052  h1de2bi  23057  h1de2ctlem  23058  spansni  23060  df0op2  23256  ho01i  23332  nmop0h  23495  opsqrlem2  23645  opsqrlem4  23647  opsqrlem5  23648  hmopidmchi  23655  atoml2i  23887  xrge0iifcv  24321  xrge0iifiso  24322  xrge0iifhmeo  24323  xrge0iifhom  24324  rezh  24356  rrhre  24388  sxbrsigalem5  24639  ballotth  24796  subfacp1lem3  24869  subfacp1lem5  24871  kur14lem7  24899  kur14lem9  24901  nofv  25613  sltres  25620  noxp1o  25622  noxp2o  25623  bdayfo  25631  nobndlem3  25650  nobndlem7  25654  nobndup  25656  nobnddown  25657  axlowdimlem4  25885  axlowdimlem6  25887  axlowdimlem7  25888  axlowdimlem8  25889  axlowdimlem9  25890  axlowdimlem13  25894  onsucsuccmpi  26194  mbfresfi  26254  fdc  26450  rabren3dioph  26877  pw2f1ocnv  27109  lhe4.4ex1a  27524  refsum2cnlem1  27685  wallispilem2  27792  stirlinglem14  27813  bnj1015  29333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-v 2959
  Copyright terms: Public domain W3C validator