Theorem elexi 3213

Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
elexi.1	|- A e. B

Assertion

Ref	Expression
elexi	|- A e. _V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elexi.1	. 2 |- A e. B
2		elex 3212	. 2 |- ( A e. B -> A e. _V )
3	1, 2	ax-mp 5	1 |- A e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  onunisuci  5841  funopdmsn  6415  mptrabexOLD  6489  caovmo  6871  oev  7594  oe0  7602  oev2  7603  oneo  7661  nnneo  7731  endisj  8047  pwen  8133  sdom1  8160  1sdom  8163  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  rankxplim3  8744  pm54.43  8826  mappwen  8935  cda1dif  8998  pm110.643  8999  infcda1  9015  infmap2  9040  ackbij1lem5  9046  cfsuc  9079  isfin4-3  9137  dcomex  9269  pwcfsdom  9405  cfpwsdom  9406  alephom  9407  canthp1lem2  9475  pwxpndom2  9487  inar1  9597  indpi  9729  pinq  9749  archnq  9802  prlem934  9855  0idsr  9918  recexsrlem  9924  supsrlem  9932  opelreal  9951  elreal  9952  elreal2  9953  eqresr  9958  axmulass  9978  ax1ne0  9981  c0ex  10034  1ex  10035  pnfex  10093  2ex  11092  3ex  11096  elxr  11950  xnegex  12039  xaddval  12054  xmulval  12056  om2uzrdg  12755  hashxplem  13220  brfi1uzind  13280  brfi1uzindOLD  13286  opfi1uzindOLD  13289  caucvgr  14406  rpnnen  14956  rexpen  14957  sadcf  15175  sadcp1  15177  phimullem  15484  prmreclem6  15625  xpsc0  16220  xpsc1  16221  xpsfrnel  16223  xpsfrnel2  16225  xpsle  16241  setcepi  16738  efgval  18130  efgi1  18134  frgpuptinv  18184  dmdprdpr  18448  dprdpr  18449  coe1fval3  19578  00ply1bas  19610  ply1plusgfvi  19612  coe1z  19633  coe1mul2  19639  coe1tm  19643  cnfldfun  19758  cnfldfunALT  19759  xpstopnlem1  21612  xpstopnlem2  21614  xpsdsval  22186  dscmet  22377  dscopn  22378  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  bndth  22757  mbfimaopnlem  23422  dvef  23743  mdegcl  23829  pige3  24269  cxpval  24410  1cubr  24569  emcllem7  24728  basellem7  24813  prmorcht  24904  sqff1o  24908  ppiublem2  24928  lgsval  25026  lgsdir2lem3  25052  axlowdimlem4  25825  axlowdimlem6  25827  axlowdimlem8  25829  axlowdimlem9  25830  upgrbi  25988  usgrexmpllem  26152  uhgr3cyclex  27042  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  ex-opab  27289  ex-eprel  27290  ex-id  27291  ex-xp  27293  ex-cnv  27294  ex-dm  27296  ex-rn  27297  ex-res  27298  ex-fv  27300  ex-1st  27301  ex-2nd  27302  hhph  28035  hlim0  28092  hsn0elch  28105  elch0  28111  hhssabloilem  28118  choc0  28185  shintcli  28188  shincli  28221  chincli  28319  h1deoi  28408  h1de2bi  28413  h1de2ctlem  28414  spansni  28416  df0op2  28611  ho01i  28687  nmop0h  28850  opsqrlem2  29000  opsqrlem4  29002  opsqrlem5  29003  hmopidmchi  29010  atoml2i  29242  xrge0iifhmeo  29982  rezh  30015  rrhre  30065  sxbrsigalem5  30350  carsgclctunlem2  30381  ballotth  30599  cxpcncf1  30673  reprsuc  30693  reprlt  30697  reprgt  30699  circlemethnat  30719  circlevma  30720  bnj1015  31031  subfacp1lem3  31164  subfacp1lem5  31166  kur14lem7  31194  kur14lem9  31196  mrsubcv  31407  mrsubrn  31410  mvhf1  31456  msubvrs  31457  nofv  31810  sltres  31815  noxp1o  31816  noextend  31819  noextendlt  31822  noextendgt  31823  nolesgn2ores  31825  bdayfo  31828  nosepnelem  31830  nosep1o  31832  nosepdmlem  31833  nolt02o  31845  nosupno  31849  nosupbday  31851  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  noetalem1  31863  noetalem3  31865  noetalem4  31866  onsucsuccmpi  32442  finxpreclem2  33227  poimirlem26  33435  poimirlem27  33436  poimir  33442  mbfresfi  33456  fdc  33541  rabren3dioph  37379  pw2f1ocnv  37604  cllem0  37871  rclexi  37922  trclexi  37927  rtrclexi  37928  frege54cor1c  38209  dffrege76  38233  frege83  38240  frege97  38254  frege98  38255  dffrege99  38256  frege104  38261  frege109  38266  frege110  38267  frege131  38288  frege133  38290  clsk3nimkb  38338  clsk1indlem4  38342  clsk1indlem1  38343  clsk1independent  38344  rpex  39562  xrlexaddrp  39568  limsup10exlem  40004  limsup10ex  40005  cxpcncf2  40113  wallispilem2  40283  stirlinglem14  40304  fourierdlem70  40393  fourierdlem83  40406  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  fouriersw  40448  sge0tsms  40597  omeunle  40730  0ome  40743  ovn0lem  40779  hoidmvlelem3  40811  ovnhoilem1  40815  vonicclem2  40898  mbfresmf  40948  smfpimcclem  41013