Theorem elexi 3186

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	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
elexi	⊢ 𝐴 ∈ V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elexi.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		elex 3185	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  onunisuci  5758  mptrabexOLD  6393  caovmo  6769  oev  7481  oe0  7489  oev2  7490  oneo  7548  nnneo  7618  endisj  7932  pwen  8018  sdom1  8045  1sdom  8048  cnfcom2  8482  cnfcom3lem  8483  cnfcom3  8484  rankxplim3  8627  pm54.43  8709  mappwen  8818  cda1dif  8881  pm110.643  8882  infcda1  8898  infmap2  8923  ackbij1lem5  8929  cfsuc  8962  isfin4-3  9020  dcomex  9152  pwcfsdom  9284  cfpwsdom  9285  alephom  9286  canthp1lem2  9354  pwxpndom2  9366  inar1  9476  indpi  9608  pinq  9628  archnq  9681  prlem934  9734  0idsr  9797  recexsrlem  9803  supsrlem  9811  opelreal  9830  elreal  9831  elreal2  9832  eqresr  9837  axmulass  9857  ax1ne0  9860  c0ex  9913  1ex  9914  pnfex  9972  2ex  10969  3ex  10973  elxr  11826  xnegex  11913  xaddval  11928  xmulval  11930  om2uzrdg  12617  hashxplem  13080  brfi1uzind  13135  opfi1uzind  13138  brfi1uzindOLD  13141  opfi1uzindOLD  13144  caucvgr  14254  rpnnen  14795  rexpen  14796  sadcf  15013  sadcp1  15015  phimullem  15322  prmreclem6  15463  xpsc0  16043  xpsc1  16044  xpsfrnel  16046  xpsfrnel2  16048  xpsle  16064  setcepi  16561  efgval  17953  efgi1  17957  frgpuptinv  18007  dmdprdpr  18271  dprdpr  18272  coe1fval3  19399  00ply1bas  19431  ply1plusgfvi  19433  coe1z  19454  coe1mul2  19460  coe1tm  19464  xpstopnlem1  21422  xpstopnlem2  21424  xpsdsval  21996  dscmet  22187  dscopn  22188  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  bndth  22565  mbfimaopnlem  23228  dvef  23547  mdegcl  23633  pige3  24073  cxpval  24210  1cubr  24369  emcllem7  24528  basellem7  24613  prmorcht  24704  sqff1o  24708  ppiublem2  24728  lgsval  24826  lgsdir2lem3  24852  axlowdimlem4  25625  axlowdimlem6  25627  axlowdimlem8  25629  axlowdimlem9  25630  structvtxval  25698  structiedg0val  25699  upgrbi  25760  usgraexmpl  25930  usgra2adedgwlkonALT  26144  umgrabi  26510  ex-opab  26681  ex-eprel  26682  ex-id  26683  ex-xp  26685  ex-cnv  26686  ex-dm  26688  ex-rn  26689  ex-res  26690  ex-fv  26692  ex-1st  26693  ex-2nd  26694  hhph  27419  hlim0  27476  hsn0elch  27489  elch0  27495  hhssabloilem  27502  choc0  27569  shintcli  27572  shincli  27605  chincli  27703  h1deoi  27792  h1de2bi  27797  h1de2ctlem  27798  spansni  27800  df0op2  27995  ho01i  28071  nmop0h  28234  opsqrlem2  28384  opsqrlem4  28386  opsqrlem5  28387  hmopidmchi  28394  atoml2i  28626  xrge0iifhmeo  29310  rezh  29343  rrhre  29393  sxbrsigalem5  29677  carsgclctunlem2  29708  ballotth  29926  bnj1015  30285  subfacp1lem3  30418  subfacp1lem5  30420  kur14lem7  30448  kur14lem9  30450  mrsubcv  30661  mrsubrn  30664  mvhf1  30710  msubvrs  30711  nofv  31054  sltres  31061  noxp1o  31063  noxp2o  31064  bdayfo  31074  nobndlem3  31093  nobndlem7  31097  nobndup  31099  nobnddown  31100  onsucsuccmpi  31612  finxpreclem2  32403  poimirlem26  32605  poimirlem27  32606  poimir  32612  mbfresfi  32626  fdc  32711  rabren3dioph  36397  pw2f1ocnv  36622  cllem0  36890  rclexi  36941  trclexi  36946  rtrclexi  36947  frege54cor1c  37229  dffrege76  37253  frege83  37260  frege97  37274  frege98  37275  dffrege99  37276  frege104  37281  frege109  37286  frege110  37287  frege131  37308  frege133  37310  clsk3nimkb  37358  clsk1indlem4  37362  clsk1indlem1  37363  clsk1independent  37364  rpex  38503  xrlexaddrp  38509  cxpcncf2  38786  wallispilem2  38959  stirlinglem14  38980  fourierdlem70  39069  fourierdlem83  39082  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  fouriersw  39124  sge0tsms  39273  omeunle  39406  0ome  39419  ovn0lem  39455  hoidmvlelem3  39487  ovnhoilem1  39491  vonicclem2  39575  mbfresmf  39626  usgrexmpllem  40484  1wlk2v2e  41324  uhgr3cyclex  41349  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424