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 2109  Vcvv 3436

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 3438

This theorem is referenced by:  elpwi2  5274  funopdmsn  7084  caovmo  7586  pwen  9067  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  rankxplim3  9777  mappwen  10006  ackbij1lem5  10117  alephom  10479  inar1  10669  prlem934  10927  0idsr  10991  recexsrlem  10997  supsrlem  11005  opelreal  11024  elreal  11025  elreal2  11026  eqresr  11031  axmulass  11051  ax1ne0  11054  c0ex  11109  1ex  11111  2ex  12205  3ex  12210  elxr  13018  xnegex  13110  xaddval  13125  xmulval  13127  om2uzrdg  13863  hashxplem  14340  caucvgr  15583  rpnnen  16136  rexpen  16137  phimullem  16690  prmreclem6  16833  efgval  19596  cnfldfun  21275  cnfldfunALT  21276  cnfldfunOLD  21288  cnfldfunALTOLD  21289  psdmul  22051  psdmvr  22054  coe1mul2  22153  dscmet  24458  dscopn  24459  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  bndth  24855  mbfimaopnlem  25554  mdegcl  25972  pige3ALT  26427  cxpval  26571  1cubr  26750  emcllem7  26910  basellem7  26995  prmorcht  27086  sqff1o  27090  ppiublem2  27112  lgsval  27210  lgsdir2lem3  27236  nofv  27567  sltres  27572  noextend  27576  noextendgt  27580  nolesgn2ores  27582  nosepnelem  27589  nosepdmlem  27593  nolt02o  27605  nosupno  27613  nosupbnd1lem3  27620  nosupbnd1  27624  nosupbnd2lem1  27625  nosupbnd2  27626  0slt1s  27743  bday1s  27745  cuteq0  27746  cuteq1  27748  mulsrid  28021  precsexlem9  28122  precsexlem11  28124  dfn0s2  28229  n0scut  28231  zsoring  28301  1p1e2s  28308  twocut  28315  expsval  28317  axlowdimlem4  28890  axlowdimlem6  28892  upgrbi  29038  usgrexmpllem  29205  clwwlknon1sn  30044  uhgr3cyclex  30126  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  ex-opab  30376  ex-eprel  30377  ex-id  30378  ex-xp  30380  ex-cnv  30381  ex-dm  30383  ex-rn  30384  ex-res  30385  ex-fv  30387  ex-1st  30388  ex-2nd  30389  hhph  31122  hlim0  31179  hsn0elch  31192  elch0  31198  hhssabloilem  31205  choc0  31270  shintcli  31273  shincli  31306  chincli  31404  h1deoi  31493  h1de2bi  31498  h1de2ctlem  31499  spansni  31501  df0op2  31696  ho01i  31772  nmop0h  31935  opsqrlem2  32085  opsqrlem4  32087  opsqrlem5  32088  hmopidmchi  32095  atoml2i  32327  s3clhash  32889  xrge0iifhmeo  33903  rezh  33936  rrhre  33988  sxbrsigalem5  34256  carsgclctunlem2  34287  ballotth  34506  reprsuc  34583  reprlt  34587  reprgt  34589  circlemethnat  34609  circlevma  34610  bnj1015  34929  subfacp1lem3  35159  subfacp1lem5  35161  kur14lem7  35189  kur14lem9  35191  mrsubcv  35487  mrsubrn  35490  mvhf1  35536  msubvrs  35537  onsucsuccmpi  36421  finxpreclem2  37368  poimirlem26  37630  poimirlem27  37631  poimir  37637  mbfresfi  37650  fdc  37729  rabren3dioph  42792  cllem0  43543  rclexi  43592  trclexi  43597  rtrclexi  43598  frege54cor1c  43892  dffrege76  43916  frege83  43923  frege97  43937  frege98  43938  dffrege99  43939  frege104  43944  frege109  43949  frege110  43950  frege131  43971  frege133  43973  clsk1independent  44023  imaexi  45203  xrlexaddrp  45336  limsup10exlem  45757  wallispilem2  46051  stirlinglem14  46072  fourierdlem70  46161  fourierdlem83  46174  fourierdlem102  46193  fourierdlem103  46194  fourierdlem104  46195  fourierdlem114  46205  fouriersw  46216  sge0tsms  46365  omeunle  46501  0ome  46514  ovn0lem  46550  hoidmvlelem3  46582  ovnhoilem1  46586  vonicclem2  46669  mbfresmf  46724  smfpimcclem  46792  lamberte  46876  nfermltl8rev  47730  nfermltlrev  47732  usgrexmpl1lem  48009  usgrexmpl2lem  48014  usgrexmpl2nb0  48019  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  usgrexmpl2trifr  48025