Theorem elexi 3463

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  elpwi2  5280  funopdmsn  7095  caovmo  7595  pwen  9078  cnfcom2  9611  cnfcom3lem  9612  cnfcom3  9613  rankxplim3  9793  mappwen  10022  ackbij1lem5  10133  alephom  10496  inar1  10686  prlem934  10944  0idsr  11008  recexsrlem  11014  supsrlem  11022  opelreal  11041  elreal  11042  elreal2  11043  eqresr  11048  axmulass  11068  ax1ne0  11071  c0ex  11126  1ex  11128  2ex  12222  3ex  12227  elxr  13030  xnegex  13123  xaddval  13138  xmulval  13140  om2uzrdg  13879  hashxplem  14356  caucvgr  15599  rpnnen  16152  rexpen  16153  phimullem  16706  prmreclem6  16849  efgval  19646  cnfldfun  21323  cnfldfunALT  21324  cnfldfunOLD  21336  cnfldfunALTOLD  21337  psdmul  22109  psdmvr  22112  coe1mul2  22211  dscmet  24516  dscopn  24517  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  bndth  24913  mbfimaopnlem  25612  mdegcl  26030  pige3ALT  26485  cxpval  26629  1cubr  26808  emcllem7  26968  basellem7  27053  prmorcht  27144  sqff1o  27148  ppiublem2  27170  lgsval  27268  lgsdir2lem3  27294  nofv  27625  ltsres  27630  noextend  27634  noextendgt  27638  nolesgn2ores  27640  nosepnelem  27647  nosepdmlem  27651  nolt02o  27663  nosupno  27671  nosupbnd1lem3  27678  nosupbnd1  27682  nosupbnd2lem1  27683  nosupbnd2  27684  0lt1s  27808  bday1  27810  cuteq0  27811  cuteq1  27813  mulsrid  28109  precsexlem9  28211  precsexlem11  28213  dfn0s2  28328  n0cut  28330  zsoring  28405  twocut  28419  expsval  28421  1reno  28493  axlowdimlem4  29018  axlowdimlem6  29020  upgrbi  29166  usgrexmpllem  29333  clwwlknon1sn  30175  uhgr3cyclex  30257  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  ex-opab  30507  ex-eprel  30508  ex-id  30509  ex-xp  30511  ex-cnv  30512  ex-dm  30514  ex-rn  30515  ex-res  30516  ex-fv  30518  ex-1st  30519  ex-2nd  30520  hhph  31253  hlim0  31310  hsn0elch  31323  elch0  31329  hhssabloilem  31336  choc0  31401  shintcli  31404  shincli  31437  chincli  31535  h1deoi  31624  h1de2bi  31629  h1de2ctlem  31630  spansni  31632  df0op2  31827  ho01i  31903  nmop0h  32066  opsqrlem2  32216  opsqrlem4  32218  opsqrlem5  32219  hmopidmchi  32226  atoml2i  32458  s3clhash  33030  xrge0iifhmeo  34093  rezh  34126  rrhre  34178  sxbrsigalem5  34445  carsgclctunlem2  34476  ballotth  34695  reprsuc  34772  reprlt  34776  reprgt  34778  circlemethnat  34798  circlevma  34799  bnj1015  35118  subfacp1lem3  35376  subfacp1lem5  35378  kur14lem7  35406  kur14lem9  35408  mrsubcv  35704  mrsubrn  35707  mvhf1  35753  msubvrs  35754  onsucsuccmpi  36637  finxpreclem2  37595  poimirlem26  37847  poimirlem27  37848  poimir  37854  mbfresfi  37867  fdc  37946  rabren3dioph  43067  cllem0  43817  rclexi  43866  trclexi  43871  rtrclexi  43872  frege54cor1c  44166  dffrege76  44190  frege83  44197  frege97  44211  frege98  44212  dffrege99  44213  frege104  44218  frege109  44223  frege110  44224  frege131  44245  frege133  44247  clsk1independent  44297  imaexi  45475  xrlexaddrp  45607  limsup10exlem  46026  wallispilem2  46320  stirlinglem14  46341  fourierdlem70  46430  fourierdlem83  46443  fourierdlem102  46462  fourierdlem103  46463  fourierdlem104  46464  fourierdlem114  46474  fouriersw  46485  sge0tsms  46634  omeunle  46770  0ome  46783  ovn0lem  46819  hoidmvlelem3  46851  ovnhoilem1  46855  vonicclem2  46938  mbfresmf  46993  smfpimcclem  47061  lamberte  47144  nfermltl8rev  47998  nfermltlrev  48000  usgrexmpl1lem  48277  usgrexmpl2lem  48282  usgrexmpl2nb0  48287  usgrexmpl2nb3  48290  usgrexmpl2nb4  48291  usgrexmpl2nb5  48292  usgrexmpl2trifr  48293