Theorem elexi 3465

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444

This theorem is referenced by:  elpwi2  5282  funopdmsn  7105  caovmo  7605  pwen  9090  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  rankxplim3  9805  mappwen  10034  ackbij1lem5  10145  alephom  10508  inar1  10698  prlem934  10956  0idsr  11020  recexsrlem  11026  supsrlem  11034  opelreal  11053  elreal  11054  elreal2  11055  eqresr  11060  axmulass  11080  ax1ne0  11083  c0ex  11138  1ex  11140  2ex  12234  3ex  12239  elxr  13042  xnegex  13135  xaddval  13150  xmulval  13152  om2uzrdg  13891  hashxplem  14368  caucvgr  15611  rpnnen  16164  rexpen  16165  phimullem  16718  prmreclem6  16861  efgval  19658  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  psdmul  22121  psdmvr  22124  coe1mul2  22223  dscmet  24528  dscopn  24529  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  bndth  24925  mbfimaopnlem  25624  mdegcl  26042  pige3ALT  26497  cxpval  26641  1cubr  26820  emcllem7  26980  basellem7  27065  prmorcht  27156  sqff1o  27160  ppiublem2  27182  lgsval  27280  lgsdir2lem3  27306  nofv  27637  ltsres  27642  noextend  27646  noextendgt  27650  nolesgn2ores  27652  nosepnelem  27659  nosepdmlem  27663  nolt02o  27675  nosupno  27683  nosupbnd1lem3  27690  nosupbnd1  27694  nosupbnd2lem1  27695  nosupbnd2  27696  0lt1s  27820  bday1  27822  cuteq0  27823  cuteq1  27825  mulsrid  28121  precsexlem9  28223  precsexlem11  28225  dfn0s2  28340  n0cut  28342  zsoring  28417  twocut  28431  expsval  28433  1reno  28505  axlowdimlem4  29030  axlowdimlem6  29032  upgrbi  29178  usgrexmpllem  29345  clwwlknon1sn  30187  uhgr3cyclex  30269  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  ex-opab  30519  ex-eprel  30520  ex-id  30521  ex-xp  30523  ex-cnv  30524  ex-dm  30526  ex-rn  30527  ex-res  30528  ex-fv  30530  ex-1st  30531  ex-2nd  30532  hhph  31266  hlim0  31323  hsn0elch  31336  elch0  31342  hhssabloilem  31349  choc0  31414  shintcli  31417  shincli  31450  chincli  31548  h1deoi  31637  h1de2bi  31642  h1de2ctlem  31643  spansni  31645  df0op2  31840  ho01i  31916  nmop0h  32079  opsqrlem2  32229  opsqrlem4  32231  opsqrlem5  32232  hmopidmchi  32239  atoml2i  32471  s3clhash  33041  xrge0iifhmeo  34114  rezh  34147  rrhre  34199  sxbrsigalem5  34466  carsgclctunlem2  34497  ballotth  34716  reprsuc  34793  reprlt  34797  reprgt  34799  circlemethnat  34819  circlevma  34820  bnj1015  35138  subfacp1lem3  35398  subfacp1lem5  35400  kur14lem7  35428  kur14lem9  35430  mrsubcv  35726  mrsubrn  35729  mvhf1  35775  msubvrs  35776  onsucsuccmpi  36659  finxpreclem2  37645  poimirlem26  37897  poimirlem27  37898  poimir  37904  mbfresfi  37917  fdc  37996  rabren3dioph  43172  cllem0  43922  rclexi  43971  trclexi  43976  rtrclexi  43977  frege54cor1c  44271  dffrege76  44295  frege83  44302  frege97  44316  frege98  44317  dffrege99  44318  frege104  44323  frege109  44328  frege110  44329  frege131  44350  frege133  44352  clsk1independent  44402  imaexi  45579  xrlexaddrp  45711  limsup10exlem  46130  wallispilem2  46424  stirlinglem14  46445  fourierdlem70  46534  fourierdlem83  46547  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  fouriersw  46589  sge0tsms  46738  omeunle  46874  0ome  46887  ovn0lem  46923  hoidmvlelem3  46955  ovnhoilem1  46959  vonicclem2  47042  mbfresmf  47097  smfpimcclem  47165  lamberte  47248  nfermltl8rev  48102  nfermltlrev  48104  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb0  48391  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397