Theorem elexi 3511

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  elpwi2  5353  funopdmsn  7184  caovmo  7687  1oexOLD  8542  pwen  9216  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  rankxplim3  9950  mappwen  10181  ackbij1lem5  10292  alephom  10654  inar1  10844  prlem934  11102  0idsr  11166  recexsrlem  11172  supsrlem  11180  opelreal  11199  elreal  11200  elreal2  11201  eqresr  11206  axmulass  11226  ax1ne0  11229  c0ex  11284  1ex  11286  2ex  12370  3ex  12375  elxr  13179  xnegex  13270  xaddval  13285  xmulval  13287  om2uzrdg  14007  hashxplem  14482  caucvgr  15724  rpnnen  16275  rexpen  16276  phimullem  16826  prmreclem6  16968  efgval  19759  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  psdmul  22193  coe1mul2  22293  dscmet  24606  dscopn  24607  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  bndth  25009  mbfimaopnlem  25709  mdegcl  26128  pige3ALT  26580  cxpval  26724  1cubr  26903  emcllem7  27063  basellem7  27148  prmorcht  27239  sqff1o  27243  ppiublem2  27265  lgsval  27363  lgsdir2lem3  27389  nofv  27720  sltres  27725  noextend  27729  noextendgt  27733  nolesgn2ores  27735  nosepnelem  27742  nosepdmlem  27746  nolt02o  27758  nosupno  27766  nosupbnd1lem3  27773  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  0slt1s  27892  bday1s  27894  cuteq0  27895  cuteq1  27896  mulsrid  28157  precsexlem9  28257  precsexlem11  28259  dfn0s2  28354  n0scut  28356  1p1e2s  28418  nohalf  28425  expsval  28426  axlowdimlem4  28978  axlowdimlem6  28980  upgrbi  29128  usgrexmpllem  29295  clwwlknon1sn  30132  uhgr3cyclex  30214  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  ex-opab  30464  ex-eprel  30465  ex-id  30466  ex-xp  30468  ex-cnv  30469  ex-dm  30471  ex-rn  30472  ex-res  30473  ex-fv  30475  ex-1st  30476  ex-2nd  30477  hhph  31210  hlim0  31267  hsn0elch  31280  elch0  31286  hhssabloilem  31293  choc0  31358  shintcli  31361  shincli  31394  chincli  31492  h1deoi  31581  h1de2bi  31586  h1de2ctlem  31587  spansni  31589  df0op2  31784  ho01i  31860  nmop0h  32023  opsqrlem2  32173  opsqrlem4  32175  opsqrlem5  32176  hmopidmchi  32183  atoml2i  32415  s3clhash  32914  xrge0iifhmeo  33882  rezh  33917  rrhre  33967  sxbrsigalem5  34253  carsgclctunlem2  34284  ballotth  34502  reprsuc  34592  reprlt  34596  reprgt  34598  circlemethnat  34618  circlevma  34619  bnj1015  34938  subfacp1lem3  35150  subfacp1lem5  35152  kur14lem7  35180  kur14lem9  35182  mrsubcv  35478  mrsubrn  35481  mvhf1  35527  msubvrs  35528  onsucsuccmpi  36409  finxpreclem2  37356  poimirlem26  37606  poimirlem27  37607  poimir  37613  mbfresfi  37626  fdc  37705  rabren3dioph  42771  cllem0  43528  rclexi  43577  trclexi  43582  rtrclexi  43583  frege54cor1c  43877  dffrege76  43901  frege83  43908  frege97  43922  frege98  43923  dffrege99  43924  frege104  43929  frege109  43934  frege110  43935  frege131  43956  frege133  43958  clsk1independent  44008  imaexi  45128  rpex  45261  xrlexaddrp  45267  limsup10exlem  45693  wallispilem2  45987  stirlinglem14  46008  fourierdlem70  46097  fourierdlem83  46110  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  fouriersw  46152  sge0tsms  46301  omeunle  46437  0ome  46450  ovn0lem  46486  hoidmvlelem3  46518  ovnhoilem1  46522  vonicclem2  46605  mbfresmf  46660  smfpimcclem  46728  nfermltl8rev  47616  nfermltlrev  47618  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852