Theorem elexi 3485

Description: If a class is a member of another class, then it is a set. Inference associated with elex 3484. (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 3484	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  elpwi2  5306  funopdmsn  7148  caovmo  7648  pwen  9138  cnfcom2  9671  cnfcom3lem  9672  cnfcom3  9673  rankxplim3  9853  mappwen  10096  ackbij1lem5  10206  alephom  10570  inar1  10760  prlem934  11018  0idsr  11082  recexsrlem  11088  supsrlem  11096  opelreal  11115  elreal  11116  elreal2  11117  eqresr  11122  axmulass  11142  ax1ne0  11145  c0ex  11200  1ex  11203  2ex  12318  3ex  12323  elxr  13141  xnegex  13234  xaddval  13249  xmulval  13251  om2uzrdg  13992  hashxplem  14470  caucvgr  15727  rpnnen  16283  rexpen  16284  phimullem  16838  prmreclem6  16981  efgval  19787  cnfldfun  21505  cnfldfunALT  21506  psdmul  22298  psdmvr  22301  coe1mul2  22399  dscmet  24698  dscopn  24699  icopnfhmeo  25071  iccpnfhmeo  25073  xrhmeo  25074  bndth  25086  mbfimaopnlem  25783  mdegcl  26195  pige3ALT  26651  cxpval  26795  1cubr  26973  emcllem7  27132  basellem7  27217  prmorcht  27308  sqff1o  27312  ppiublem2  27333  lgsval  27431  lgsdir2lem3  27457  nofv  27787  ltsres  27792  noextend  27796  noextendgt  27800  nolesgn2ores  27802  nosepnelem  27809  nosepdmlem  27813  nolt02o  27825  nosupno  27833  nosupbnd1lem3  27840  nosupbnd1  27844  nosupbnd2lem1  27845  nosupbnd2  27846  0lt1s  27971  bday1  27973  cuteq0  27974  cuteq1  27976  mulsrid  28272  precsexlem9  28374  precsexlem11  28376  dfn0s2  28491  n0cut  28493  zsoring  28568  twocut  28582  expsval  28584  1reno  28656  axlowdimlem4  29236  axlowdimlem6  29238  upgrbi  29384  usgrexmpllem  29551  clwwlknon1sn  30392  uhgr3cyclex  30474  konigsberglem1  30544  konigsberglem2  30545  konigsberglem3  30546  ex-opab  30724  ex-eprel  30725  ex-id  30726  ex-xp  30728  ex-cnv  30729  ex-dm  30731  ex-rn  30732  ex-res  30733  ex-fv  30735  ex-1st  30736  ex-2nd  30737  hhph  31471  hlim0  31528  hsn0elch  31541  elch0  31547  hhssabloilem  31554  choc0  31619  shintcli  31622  shincli  31655  chincli  31753  h1deoi  31842  h1de2bi  31847  h1de2ctlem  31848  spansni  31850  df0op2  32045  ho01i  32121  nmop0h  32284  opsqrlem2  32434  opsqrlem4  32436  opsqrlem5  32437  hmopidmchi  32444  atoml2i  32676  s3clhash  33209  xrge0iifhmeo  34271  rezh  34304  rrhre  34356  sxbrsigalem5  34623  carsgclctunlem2  34654  ballotth  34873  reprsuc  34947  reprlt  34951  reprgt  34953  circlemethnat  34973  circlevma  34974  bnj1015  35295  subfacp1lem3  35573  subfacp1lem5  35575  kur14lem7  35603  kur14lem9  35605  mrsubcv  35901  mrsubrn  35904  mvhf1  35950  msubvrs  35951  onsucsuccmpi  36843  finxpreclem2  37924  poimirlem26  38185  poimirlem27  38186  poimir  38192  mbfresfi  38205  fdc  38284  rabren3dioph  43434  cllem0  44184  rclexi  44233  trclexi  44238  rtrclexi  44239  frege54cor1c  44533  dffrege76  44557  frege83  44564  frege97  44578  frege98  44579  dffrege99  44580  frege104  44585  frege109  44590  frege110  44591  frege131  44612  frege133  44614  clsk1independent  44664  imaexi  45829  xrlexaddrp  45960  limsup10exlem  46378  wallispilem2  46672  stirlinglem14  46693  fourierdlem70  46782  fourierdlem83  46795  fourierdlem102  46814  fourierdlem103  46815  fourierdlem104  46816  fourierdlem114  46826  fouriersw  46837  sge0tsms  46986  omeunle  47122  0ome  47135  ovn0lem  47171  hoidmvlelem3  47203  ovnhoilem1  47207  vonicclem2  47290  mbfresmf  47345  smfpimcclem  47413  lamberte  47514  nfermltl8rev  48396  nfermltlrev  48398  usgrexmpl1lem  48675  usgrexmpl2lem  48680  usgrexmpl2nb0  48685  usgrexmpl2nb3  48688  usgrexmpl2nb4  48689  usgrexmpl2nb5  48690  usgrexmpl2trifr  48691