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  5275  funopdmsn  7089  caovmo  7589  pwen  9069  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  rankxplim3  9780  mappwen  10009  ackbij1lem5  10120  alephom  10482  inar1  10672  prlem934  10930  0idsr  10994  recexsrlem  11000  supsrlem  11008  opelreal  11027  elreal  11028  elreal2  11029  eqresr  11034  axmulass  11054  ax1ne0  11057  c0ex  11112  1ex  11114  2ex  12208  3ex  12213  elxr  13021  xnegex  13113  xaddval  13128  xmulval  13130  om2uzrdg  13869  hashxplem  14346  caucvgr  15589  rpnnen  16142  rexpen  16143  phimullem  16696  prmreclem6  16839  efgval  19635  cnfldfun  21311  cnfldfunALT  21312  cnfldfunOLD  21324  cnfldfunALTOLD  21325  psdmul  22087  psdmvr  22090  coe1mul2  22189  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  27779  bday1s  27781  cuteq0  27782  cuteq1  27784  mulsrid  28058  precsexlem9  28159  precsexlem11  28161  dfn0s2  28266  n0scut  28268  zsoring  28338  1p1e2s  28345  twocut  28352  expsval  28354  axlowdimlem4  28930  axlowdimlem6  28932  upgrbi  29078  usgrexmpllem  29245  clwwlknon1sn  30087  uhgr3cyclex  30169  konigsberglem1  30239  konigsberglem2  30240  konigsberglem3  30241  ex-opab  30419  ex-eprel  30420  ex-id  30421  ex-xp  30423  ex-cnv  30424  ex-dm  30426  ex-rn  30427  ex-res  30428  ex-fv  30430  ex-1st  30431  ex-2nd  30432  hhph  31165  hlim0  31222  hsn0elch  31235  elch0  31241  hhssabloilem  31248  choc0  31313  shintcli  31316  shincli  31349  chincli  31447  h1deoi  31536  h1de2bi  31541  h1de2ctlem  31542  spansni  31544  df0op2  31739  ho01i  31815  nmop0h  31978  opsqrlem2  32128  opsqrlem4  32130  opsqrlem5  32131  hmopidmchi  32138  atoml2i  32370  s3clhash  32936  xrge0iifhmeo  33956  rezh  33989  rrhre  34041  sxbrsigalem5  34308  carsgclctunlem2  34339  ballotth  34558  reprsuc  34635  reprlt  34639  reprgt  34641  circlemethnat  34661  circlevma  34662  bnj1015  34981  subfacp1lem3  35233  subfacp1lem5  35235  kur14lem7  35263  kur14lem9  35265  mrsubcv  35561  mrsubrn  35564  mvhf1  35610  msubvrs  35611  onsucsuccmpi  36494  finxpreclem2  37441  poimirlem26  37692  poimirlem27  37693  poimir  37699  mbfresfi  37712  fdc  37791  rabren3dioph  42913  cllem0  43664  rclexi  43713  trclexi  43718  rtrclexi  43719  frege54cor1c  44013  dffrege76  44037  frege83  44044  frege97  44058  frege98  44059  dffrege99  44060  frege104  44065  frege109  44070  frege110  44071  frege131  44092  frege133  44094  clsk1independent  44144  imaexi  45323  xrlexaddrp  45456  limsup10exlem  45875  wallispilem2  46169  stirlinglem14  46190  fourierdlem70  46279  fourierdlem83  46292  fourierdlem102  46311  fourierdlem103  46312  fourierdlem104  46313  fourierdlem114  46323  fouriersw  46334  sge0tsms  46483  omeunle  46619  0ome  46632  ovn0lem  46668  hoidmvlelem3  46700  ovnhoilem1  46704  vonicclem2  46787  mbfresmf  46842  smfpimcclem  46910  lamberte  46993  nfermltl8rev  47847  nfermltlrev  47849  usgrexmpl1lem  48126  usgrexmpl2lem  48131  usgrexmpl2nb0  48136  usgrexmpl2nb3  48139  usgrexmpl2nb4  48140  usgrexmpl2nb5  48141  usgrexmpl2trifr  48142