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

Theorem elexi 2925
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 2924 . 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 1721   _Vcvv 2916
This theorem is referenced by:  onunisuci  4654  fnprOLD  5910  caovmo  6243  oev  6717  oe0  6725  oev2  6726  oneo  6783  nnneo  6853  endisj  7154  pwen  7239  sdom1  7267  1sdom  7270  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  rankxplim3  7761  pm54.43  7843  mappwen  7949  cda1dif  8012  pm110.643  8013  infcda1  8029  infmap2  8054  ackbij1lem5  8060  cfsuc  8093  isfin4-3  8151  dcomex  8283  pwcfsdom  8414  cfpwsdom  8415  alephom  8416  canthp1lem2  8484  pwxpndom2  8496  inar1  8606  indpi  8740  pinq  8760  archnq  8813  prlem934  8866  0idsr  8928  recexsrlem  8934  supsrlem  8942  opelreal  8961  elreal  8962  elreal2  8963  eqresr  8968  axmulass  8988  ax1ne0  8991  c0ex  9041  1ex  9042  mnfxr  10670  elxr  10672  xnegex  10750  xaddval  10765  xmulval  10767  xrinfmss  10844  xrinfm0  10871  fzprval  11062  fztpval  11063  om2uzrdg  11251  hashgval  11576  hashinf  11578  hashf  11580  hashxplem  11651  caucvgr  12424  xpnnenOLD  12764  rpnnen  12781  rexpen  12782  ruclem11  12794  sadcf  12920  sadcp1  12922  phimullem  13123  pcval  13173  pc0  13183  prmreclem6  13244  ramcl2  13339  xpsc0  13740  xpsc1  13741  xpsfrnel  13743  xpsfrnel2  13745  xpsle  13761  setcepi  14198  efgval  15304  efgi1  15308  frgpuptinv  15358  dmdprdpr  15562  dprdpr  15563  coe1fval3  16561  00ply1bas  16589  ply1plusgfvi  16591  coe1z  16611  coe1mul2  16617  coe1tm  16620  xpstopnlem1  17794  xpstopnlem2  17796  xpsdsval  18364  dscmet  18573  dscopn  18574  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  bndth  18936  mbfimaopnlem  19500  iblcnlem1  19632  dvef  19817  mdegcl  19945  iaa  20195  taylfval  20228  pige3  20378  cxpval  20508  1cubr  20635  xrlimcnp  20760  emcllem7  20793  basellem7  20822  basellem9  20824  prmorcht  20914  sqff1o  20918  ppiublem2  20940  lgsval  21037  lgsdir2lem3  21062  selberglem1  21192  usgraexmpl  21373  wlkntrllem2  21513  2pthlem2  21549  constr3lem2  21586  constr3lem4  21587  constr3lem5  21588  constr3trllem1  21590  vdgrf  21622  eupath  21656  umgrabi  21658  konigsberg  21662  ex-pss  21689  ex-opab  21693  ex-eprel  21694  ex-id  21695  ex-xp  21697  ex-cnv  21698  ex-dm  21700  ex-rn  21701  ex-res  21702  ex-ima  21703  ex-fv  21704  ex-1st  21705  ex-2nd  21706  hhph  22633  hlim0  22691  hsn0elch  22703  elch0  22709  choc0  22781  shintcli  22784  shincli  22817  chincli  22915  h1deoi  23004  h1de2bi  23009  h1de2ctlem  23010  spansni  23012  df0op2  23208  ho01i  23284  nmop0h  23447  opsqrlem2  23597  opsqrlem4  23599  opsqrlem5  23600  hmopidmchi  23607  atoml2i  23839  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhmeo  24275  xrge0iifhom  24276  rezh  24308  rrhre  24340  sxbrsigalem5  24591  ballotth  24748  subfacp1lem3  24821  subfacp1lem5  24823  kur14lem7  24851  kur14lem9  24853  nofv  25525  sltres  25532  noxp1o  25534  noxp2o  25535  bdayfo  25543  nobndlem3  25562  nobndlem7  25566  nobndup  25568  nobnddown  25569  axlowdimlem4  25788  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem8  25792  axlowdimlem9  25793  axlowdimlem13  25797  onsucsuccmpi  26097  mbfresfi  26152  fdc  26339  rabren3dioph  26766  pw2f1ocnv  26998  lhe4.4ex1a  27414  refsum2cnlem1  27575  wallispilem2  27682  stirlinglem14  27703  bnj1015  29038
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator