Theorem elexi 3459

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  elpwi2  5271  funopdmsn  7083  caovmo  7583  pwen  9063  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  rankxplim3  9774  mappwen  10003  ackbij1lem5  10114  alephom  10476  inar1  10666  prlem934  10924  0idsr  10988  recexsrlem  10994  supsrlem  11002  opelreal  11021  elreal  11022  elreal2  11023  eqresr  11028  axmulass  11048  ax1ne0  11051  c0ex  11106  1ex  11108  2ex  12202  3ex  12207  elxr  13015  xnegex  13107  xaddval  13122  xmulval  13124  om2uzrdg  13863  hashxplem  14340  caucvgr  15583  rpnnen  16136  rexpen  16137  phimullem  16690  prmreclem6  16833  efgval  19629  cnfldfun  21305  cnfldfunALT  21306  cnfldfunOLD  21318  cnfldfunALTOLD  21319  psdmul  22081  psdmvr  22084  coe1mul2  22183  dscmet  24487  dscopn  24488  icopnfhmeo  24868  iccpnfhmeo  24870  xrhmeo  24871  bndth  24884  mbfimaopnlem  25583  mdegcl  26001  pige3ALT  26456  cxpval  26600  1cubr  26779  emcllem7  26939  basellem7  27024  prmorcht  27115  sqff1o  27119  ppiublem2  27141  lgsval  27239  lgsdir2lem3  27265  nofv  27596  sltres  27601  noextend  27605  noextendgt  27609  nolesgn2ores  27611  nosepnelem  27618  nosepdmlem  27622  nolt02o  27634  nosupno  27642  nosupbnd1lem3  27649  nosupbnd1  27653  nosupbnd2lem1  27654  nosupbnd2  27655  0slt1s  27773  bday1s  27775  cuteq0  27776  cuteq1  27778  mulsrid  28052  precsexlem9  28153  precsexlem11  28155  dfn0s2  28260  n0scut  28262  zsoring  28332  1p1e2s  28339  twocut  28346  expsval  28348  axlowdimlem4  28923  axlowdimlem6  28925  upgrbi  29071  usgrexmpllem  29238  clwwlknon1sn  30080  uhgr3cyclex  30162  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  ex-opab  30412  ex-eprel  30413  ex-id  30414  ex-xp  30416  ex-cnv  30417  ex-dm  30419  ex-rn  30420  ex-res  30421  ex-fv  30423  ex-1st  30424  ex-2nd  30425  hhph  31158  hlim0  31215  hsn0elch  31228  elch0  31234  hhssabloilem  31241  choc0  31306  shintcli  31309  shincli  31342  chincli  31440  h1deoi  31529  h1de2bi  31534  h1de2ctlem  31535  spansni  31537  df0op2  31732  ho01i  31808  nmop0h  31971  opsqrlem2  32121  opsqrlem4  32123  opsqrlem5  32124  hmopidmchi  32131  atoml2i  32363  s3clhash  32929  xrge0iifhmeo  33949  rezh  33982  rrhre  34034  sxbrsigalem5  34301  carsgclctunlem2  34332  ballotth  34551  reprsuc  34628  reprlt  34632  reprgt  34634  circlemethnat  34654  circlevma  34655  bnj1015  34974  subfacp1lem3  35226  subfacp1lem5  35228  kur14lem7  35256  kur14lem9  35258  mrsubcv  35554  mrsubrn  35557  mvhf1  35603  msubvrs  35604  onsucsuccmpi  36487  finxpreclem2  37434  poimirlem26  37696  poimirlem27  37697  poimir  37703  mbfresfi  37716  fdc  37795  rabren3dioph  42918  cllem0  43669  rclexi  43718  trclexi  43723  rtrclexi  43724  frege54cor1c  44018  dffrege76  44042  frege83  44049  frege97  44063  frege98  44064  dffrege99  44065  frege104  44070  frege109  44075  frege110  44076  frege131  44097  frege133  44099  clsk1independent  44149  imaexi  45328  xrlexaddrp  45461  limsup10exlem  45880  wallispilem2  46174  stirlinglem14  46195  fourierdlem70  46284  fourierdlem83  46297  fourierdlem102  46316  fourierdlem103  46317  fourierdlem104  46318  fourierdlem114  46328  fouriersw  46339  sge0tsms  46488  omeunle  46624  0ome  46637  ovn0lem  46673  hoidmvlelem3  46705  ovnhoilem1  46709  vonicclem2  46792  mbfresmf  46847  smfpimcclem  46915  lamberte  46998  nfermltl8rev  47852  nfermltlrev  47854  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb0  48141  usgrexmpl2nb3  48144  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  usgrexmpl2trifr  48147