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

Theorem elexi 2810
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 2809 . 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 1696   _Vcvv 2801
This theorem is referenced by:  onunisuci  4522  caovmo  6073  oev  6529  oe0  6537  oev2  6538  oneo  6595  nnneo  6665  endisj  6965  pwen  7050  sdom1  7078  1sdom  7081  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  rankxplim3  7567  pm54.43  7649  mappwen  7755  cda1dif  7818  pm110.643  7819  infcda1  7835  infmap2  7860  ackbij1lem5  7866  cfsuc  7899  isfin4-3  7957  dcomex  8089  pwcfsdom  8221  cfpwsdom  8222  alephom  8223  canthp1lem2  8291  pwxpndom2  8303  inar1  8413  indpi  8547  pinq  8567  archnq  8620  prlem934  8673  0idsr  8735  recexsrlem  8741  supsrlem  8749  opelreal  8768  elreal  8769  elreal2  8770  eqresr  8775  axmulass  8795  ax1ne0  8798  c0ex  8848  1ex  8849  mnfxr  10472  elxr  10474  xnegex  10551  xaddval  10566  xmulval  10568  xrinfmss  10644  xrinfm0  10671  fzprval  10860  fztpval  10861  om2uzrdg  11035  hashgval  11356  hashinf  11358  hashf  11360  hashxplem  11401  caucvgr  12164  xpnnenOLD  12504  rpnnen  12521  rexpen  12522  ruclem11  12534  sadcf  12660  sadcp1  12662  phimullem  12863  pcval  12913  pc0  12923  prmreclem6  12984  ramcl2  13079  xpsc0  13478  xpsc1  13479  xpsfrnel  13481  xpsfrnel2  13483  xpsle  13499  setcepi  13936  efgval  15042  efgi1  15046  frgpuptinv  15096  dmdprdpr  15300  dprdpr  15301  coe1fval3  16305  00ply1bas  16334  ply1plusgfvi  16336  coe1z  16356  coe1mul2  16362  coe1tm  16365  xpstopnlem1  17516  xpstopnlem2  17518  xpsdsval  17961  dscmet  18111  dscopn  18112  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  bndth  18472  mbfimaopnlem  19026  iblcnlem1  19158  dvef  19343  mdegcl  19471  iaa  19721  taylfval  19754  pige3  19901  cxpval  20027  1cubr  20154  xrlimcnp  20279  emcllem7  20311  basellem7  20340  basellem9  20342  prmorcht  20432  sqff1o  20436  ppiublem2  20458  lgsval  20555  lgsdir2lem3  20580  selberglem1  20710  ex-pss  20831  ex-opab  20835  ex-eprel  20836  ex-id  20837  ex-xp  20839  ex-cnv  20840  ex-dm  20842  ex-rn  20843  ex-res  20844  ex-ima  20845  ex-fv  20846  ex-1st  20847  ex-2nd  20848  hhph  21773  hlim0  21831  hsn0elch  21843  elch0  21849  choc0  21921  shintcli  21924  shincli  21957  chincli  22055  h1deoi  22144  h1de2bi  22149  h1de2ctlem  22150  spansni  22152  df0op2  22348  ho01i  22424  nmop0h  22587  opsqrlem2  22737  opsqrlem4  22739  opsqrlem5  22740  hmopidmchi  22747  atoml2i  22979  ballotth  23112  iuninc  23174  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhmeo  23333  xrge0iifhom  23334  xrge0mulc1cn  23338  lmlimxrge0  23387  esumcvg  23469  dmvlsiga  23505  brsiga  23529  coinflippv  23699  subfacp1lem3  23728  subfacp1lem5  23730  kur14lem7  23758  kur14lem9  23760  eupath  23920  umgrabi  23922  konigsberg  23926  nofv  24382  sltres  24389  noxp1o  24391  noxp2o  24392  bdayfo  24400  nobndlem3  24419  nobndlem7  24423  nobndup  24425  nobnddown  24426  axlowdimlem4  24645  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem8  24649  axlowdimlem9  24650  axlowdimlem13  24654  onsucsuccmpi  24954  fates  25058  dmoprabss6  25138  fvsn2a  25218  fvsn2b  25219  repfuntw  25263  repcpwti  25264  cbcpcp  25265  prl  25270  dstr  25274  domrancur1b  25303  definc  25382  intopcoaconlem3  25642  phckle  26130  psckle  26131  pgapspf  26155  pgapspf2  26156  fdc  26558  rabren3dioph  27001  pw2f1ocnv  27233  lhe4.4ex1a  27649  wallispilem2  27918  stirlinglem14  27939  usgraexmpl  28267  wlkntrllem3  28347  wlkntrllem4  28348  constr3lem2  28392  constr3lem4  28393  constr3lem5  28394  constr3trllem1  28396  bnj1015  29309
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-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator