Theorem elexi 3461

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  elpwi2  5278  funopdmsn  7093  caovmo  7593  pwen  9076  cnfcom2  9609  cnfcom3lem  9610  cnfcom3  9611  rankxplim3  9791  mappwen  10020  ackbij1lem5  10131  alephom  10494  inar1  10684  prlem934  10942  0idsr  11006  recexsrlem  11012  supsrlem  11020  opelreal  11039  elreal  11040  elreal2  11041  eqresr  11046  axmulass  11066  ax1ne0  11069  c0ex  11124  1ex  11126  2ex  12220  3ex  12225  elxr  13028  xnegex  13121  xaddval  13136  xmulval  13138  om2uzrdg  13877  hashxplem  14354  caucvgr  15597  rpnnen  16150  rexpen  16151  phimullem  16704  prmreclem6  16847  efgval  19644  cnfldfun  21321  cnfldfunALT  21322  cnfldfunOLD  21334  cnfldfunALTOLD  21335  psdmul  22107  psdmvr  22110  coe1mul2  22209  dscmet  24514  dscopn  24515  icopnfhmeo  24895  iccpnfhmeo  24897  xrhmeo  24898  bndth  24911  mbfimaopnlem  25610  mdegcl  26028  pige3ALT  26483  cxpval  26627  1cubr  26806  emcllem7  26966  basellem7  27051  prmorcht  27142  sqff1o  27146  ppiublem2  27168  lgsval  27266  lgsdir2lem3  27292  nofv  27623  sltres  27628  noextend  27632  noextendgt  27636  nolesgn2ores  27638  nosepnelem  27645  nosepdmlem  27649  nolt02o  27661  nosupno  27669  nosupbnd1lem3  27676  nosupbnd1  27680  nosupbnd2lem1  27681  nosupbnd2  27682  0slt1s  27800  bday1s  27802  cuteq0  27803  cuteq1  27805  mulsrid  28082  precsexlem9  28183  precsexlem11  28185  dfn0s2  28292  n0scut  28294  zsoring  28367  1p1e2s  28374  twocut  28381  expsval  28383  1reno  28442  axlowdimlem4  28967  axlowdimlem6  28969  upgrbi  29115  usgrexmpllem  29282  clwwlknon1sn  30124  uhgr3cyclex  30206  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  ex-opab  30456  ex-eprel  30457  ex-id  30458  ex-xp  30460  ex-cnv  30461  ex-dm  30463  ex-rn  30464  ex-res  30465  ex-fv  30467  ex-1st  30468  ex-2nd  30469  hhph  31202  hlim0  31259  hsn0elch  31272  elch0  31278  hhssabloilem  31285  choc0  31350  shintcli  31353  shincli  31386  chincli  31484  h1deoi  31573  h1de2bi  31578  h1de2ctlem  31579  spansni  31581  df0op2  31776  ho01i  31852  nmop0h  32015  opsqrlem2  32165  opsqrlem4  32167  opsqrlem5  32168  hmopidmchi  32175  atoml2i  32407  s3clhash  32979  xrge0iifhmeo  34042  rezh  34075  rrhre  34127  sxbrsigalem5  34394  carsgclctunlem2  34425  ballotth  34644  reprsuc  34721  reprlt  34725  reprgt  34727  circlemethnat  34747  circlevma  34748  bnj1015  35067  subfacp1lem3  35325  subfacp1lem5  35327  kur14lem7  35355  kur14lem9  35357  mrsubcv  35653  mrsubrn  35656  mvhf1  35702  msubvrs  35703  onsucsuccmpi  36586  finxpreclem2  37534  poimirlem26  37786  poimirlem27  37787  poimir  37793  mbfresfi  37806  fdc  37885  rabren3dioph  42999  cllem0  43749  rclexi  43798  trclexi  43803  rtrclexi  43804  frege54cor1c  44098  dffrege76  44122  frege83  44129  frege97  44143  frege98  44144  dffrege99  44145  frege104  44150  frege109  44155  frege110  44156  frege131  44177  frege133  44179  clsk1independent  44229  imaexi  45407  xrlexaddrp  45539  limsup10exlem  45958  wallispilem2  46252  stirlinglem14  46273  fourierdlem70  46362  fourierdlem83  46375  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  fouriersw  46417  sge0tsms  46566  omeunle  46702  0ome  46715  ovn0lem  46751  hoidmvlelem3  46783  ovnhoilem1  46787  vonicclem2  46870  mbfresmf  46925  smfpimcclem  46993  lamberte  47076  nfermltl8rev  47930  nfermltlrev  47932  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb0  48219  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225