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

Theorem elexi 2797
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 2796 . 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 1684   _Vcvv 2788
This theorem is referenced by:  onunisuci  4506  caovmo  6057  oev  6513  oe0  6521  oev2  6522  oneo  6579  nnneo  6649  endisj  6949  pwen  7034  sdom1  7062  1sdom  7065  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  rankxplim3  7551  pm54.43  7633  mappwen  7739  cda1dif  7802  pm110.643  7803  infcda1  7819  infmap2  7844  ackbij1lem5  7850  cfsuc  7883  isfin4-3  7941  dcomex  8073  pwcfsdom  8205  cfpwsdom  8206  alephom  8207  canthp1lem2  8275  pwxpndom2  8287  inar1  8397  indpi  8531  pinq  8551  archnq  8604  prlem934  8657  0idsr  8719  recexsrlem  8725  supsrlem  8733  opelreal  8752  elreal  8753  elreal2  8754  eqresr  8759  axmulass  8779  ax1ne0  8782  c0ex  8832  1ex  8833  mnfxr  10456  elxr  10458  xnegex  10535  xaddval  10550  xmulval  10552  xrinfmss  10628  xrinfm0  10655  fzprval  10844  fztpval  10845  om2uzrdg  11019  hashgval  11340  hashinf  11342  hashf  11344  hashxplem  11385  caucvgr  12148  xpnnenOLD  12488  rpnnen  12505  rexpen  12506  ruclem11  12518  sadcf  12644  sadcp1  12646  phimullem  12847  pcval  12897  pc0  12907  prmreclem6  12968  ramcl2  13063  xpsc0  13462  xpsc1  13463  xpsfrnel  13465  xpsfrnel2  13467  xpsle  13483  setcepi  13920  efgval  15026  efgi1  15030  frgpuptinv  15080  dmdprdpr  15284  dprdpr  15285  coe1fval3  16289  00ply1bas  16318  ply1plusgfvi  16320  coe1z  16340  coe1mul2  16346  coe1tm  16349  xpstopnlem1  17500  xpstopnlem2  17502  xpsdsval  17945  dscmet  18095  dscopn  18096  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  bndth  18456  mbfimaopnlem  19010  iblcnlem1  19142  dvef  19327  mdegcl  19455  iaa  19705  taylfval  19738  pige3  19885  cxpval  20011  1cubr  20138  xrlimcnp  20263  emcllem7  20295  basellem7  20324  basellem9  20326  prmorcht  20416  sqff1o  20420  ppiublem2  20442  lgsval  20539  lgsdir2lem3  20564  selberglem1  20694  ex-pss  20815  ex-opab  20819  ex-eprel  20820  ex-id  20821  ex-xp  20823  ex-cnv  20824  ex-dm  20826  ex-rn  20827  ex-res  20828  ex-ima  20829  ex-fv  20830  ex-1st  20831  ex-2nd  20832  hhph  21757  hlim0  21815  hsn0elch  21827  elch0  21833  choc0  21905  shintcli  21908  shincli  21941  chincli  22039  h1deoi  22128  h1de2bi  22133  h1de2ctlem  22134  spansni  22136  df0op2  22332  ho01i  22408  nmop0h  22571  opsqrlem2  22721  opsqrlem4  22723  opsqrlem5  22724  hmopidmchi  22731  atoml2i  22963  ballotth  23096  iuninc  23158  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhmeo  23318  xrge0iifhom  23319  xrge0mulc1cn  23323  lmlimxrge0  23372  esumcvg  23454  dmvlsiga  23490  brsiga  23514  coinflippv  23684  subfacp1lem3  23713  subfacp1lem5  23715  kur14lem7  23743  kur14lem9  23745  eupath  23905  umgrabi  23907  konigsberg  23911  nofv  24311  sltres  24318  noxp1o  24320  noxp2o  24321  bdayfo  24329  nobndlem3  24348  nobndlem7  24352  nobndup  24354  nobnddown  24355  axlowdimlem4  24573  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem13  24582  onsucsuccmpi  24882  fates  24955  dmoprabss6  25035  fvsn2a  25115  fvsn2b  25116  repfuntw  25160  repcpwti  25161  cbcpcp  25162  prl  25167  dstr  25171  domrancur1b  25200  definc  25279  intopcoaconlem3  25539  phckle  26027  psckle  26028  pgapspf  26052  pgapspf2  26053  fdc  26455  rabren3dioph  26898  pw2f1ocnv  27130  lhe4.4ex1a  27546  wallispilem2  27815  stirlinglem14  27836  usgraexmpl  28133  bnj1015  28993
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator