Theorem elexi 3467

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  elpwi2  5285  funopdmsn  7104  caovmo  7606  pwen  9091  cnfcom2  9631  cnfcom3lem  9632  cnfcom3  9633  rankxplim3  9810  mappwen  10041  ackbij1lem5  10152  alephom  10514  inar1  10704  prlem934  10962  0idsr  11026  recexsrlem  11032  supsrlem  11040  opelreal  11059  elreal  11060  elreal2  11061  eqresr  11066  axmulass  11086  ax1ne0  11089  c0ex  11144  1ex  11146  2ex  12239  3ex  12244  elxr  13052  xnegex  13144  xaddval  13159  xmulval  13161  om2uzrdg  13897  hashxplem  14374  caucvgr  15618  rpnnen  16171  rexpen  16172  phimullem  16725  prmreclem6  16868  efgval  19631  cnfldfun  21310  cnfldfunALT  21311  cnfldfunOLD  21323  cnfldfunALTOLD  21324  psdmul  22086  psdmvr  22089  coe1mul2  22188  dscmet  24493  dscopn  24494  icopnfhmeo  24874  iccpnfhmeo  24876  xrhmeo  24877  bndth  24890  mbfimaopnlem  25589  mdegcl  26007  pige3ALT  26462  cxpval  26606  1cubr  26785  emcllem7  26945  basellem7  27030  prmorcht  27121  sqff1o  27125  ppiublem2  27147  lgsval  27245  lgsdir2lem3  27271  nofv  27602  sltres  27607  noextend  27611  noextendgt  27615  nolesgn2ores  27617  nosepnelem  27624  nosepdmlem  27628  nolt02o  27640  nosupno  27648  nosupbnd1lem3  27655  nosupbnd1  27659  nosupbnd2lem1  27660  nosupbnd2  27661  0slt1s  27778  bday1s  27780  cuteq0  27781  cuteq1  27783  mulsrid  28056  precsexlem9  28157  precsexlem11  28159  dfn0s2  28264  n0scut  28266  zsoring  28336  1p1e2s  28343  twocut  28350  expsval  28352  axlowdimlem4  28925  axlowdimlem6  28927  upgrbi  29073  usgrexmpllem  29240  clwwlknon1sn  30079  uhgr3cyclex  30161  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  ex-opab  30411  ex-eprel  30412  ex-id  30413  ex-xp  30415  ex-cnv  30416  ex-dm  30418  ex-rn  30419  ex-res  30420  ex-fv  30422  ex-1st  30423  ex-2nd  30424  hhph  31157  hlim0  31214  hsn0elch  31227  elch0  31233  hhssabloilem  31240  choc0  31305  shintcli  31308  shincli  31341  chincli  31439  h1deoi  31528  h1de2bi  31533  h1de2ctlem  31534  spansni  31536  df0op2  31731  ho01i  31807  nmop0h  31970  opsqrlem2  32120  opsqrlem4  32122  opsqrlem5  32123  hmopidmchi  32130  atoml2i  32362  s3clhash  32919  xrge0iifhmeo  33919  rezh  33952  rrhre  34004  sxbrsigalem5  34272  carsgclctunlem2  34303  ballotth  34522  reprsuc  34599  reprlt  34603  reprgt  34605  circlemethnat  34625  circlevma  34626  bnj1015  34945  subfacp1lem3  35162  subfacp1lem5  35164  kur14lem7  35192  kur14lem9  35194  mrsubcv  35490  mrsubrn  35493  mvhf1  35539  msubvrs  35540  onsucsuccmpi  36424  finxpreclem2  37371  poimirlem26  37633  poimirlem27  37634  poimir  37640  mbfresfi  37653  fdc  37732  rabren3dioph  42796  cllem0  43548  rclexi  43597  trclexi  43602  rtrclexi  43603  frege54cor1c  43897  dffrege76  43921  frege83  43928  frege97  43942  frege98  43943  dffrege99  43944  frege104  43949  frege109  43954  frege110  43955  frege131  43976  frege133  43978  clsk1independent  44028  imaexi  45208  xrlexaddrp  45341  limsup10exlem  45763  wallispilem2  46057  stirlinglem14  46078  fourierdlem70  46167  fourierdlem83  46180  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  fouriersw  46222  sge0tsms  46371  omeunle  46507  0ome  46520  ovn0lem  46556  hoidmvlelem3  46588  ovnhoilem1  46592  vonicclem2  46675  mbfresmf  46730  smfpimcclem  46798  lamberte  46882  nfermltl8rev  47736  nfermltlrev  47738  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb0  48015  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021