Theorem elexi 3501

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480

This theorem is referenced by:  elpwi2  5341  funopdmsn  7170  caovmo  7670  pwen  9189  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  rankxplim3  9919  mappwen  10150  ackbij1lem5  10261  alephom  10623  inar1  10813  prlem934  11071  0idsr  11135  recexsrlem  11141  supsrlem  11149  opelreal  11168  elreal  11169  elreal2  11170  eqresr  11175  axmulass  11195  ax1ne0  11198  c0ex  11253  1ex  11255  2ex  12341  3ex  12346  elxr  13156  xnegex  13247  xaddval  13262  xmulval  13264  om2uzrdg  13994  hashxplem  14469  caucvgr  15709  rpnnen  16260  rexpen  16261  phimullem  16813  prmreclem6  16955  efgval  19750  cnfldfun  21396  cnfldfunALT  21397  cnfldfunOLD  21409  cnfldfunALTOLD  21410  cnfldfunALTOLDOLD  21411  psdmul  22188  coe1mul2  22288  dscmet  24601  dscopn  24602  icopnfhmeo  24988  iccpnfhmeo  24990  xrhmeo  24991  bndth  25004  mbfimaopnlem  25704  mdegcl  26123  pige3ALT  26577  cxpval  26721  1cubr  26900  emcllem7  27060  basellem7  27145  prmorcht  27236  sqff1o  27240  ppiublem2  27262  lgsval  27360  lgsdir2lem3  27386  nofv  27717  sltres  27722  noextend  27726  noextendgt  27730  nolesgn2ores  27732  nosepnelem  27739  nosepdmlem  27743  nolt02o  27755  nosupno  27763  nosupbnd1lem3  27770  nosupbnd1  27774  nosupbnd2lem1  27775  nosupbnd2  27776  0slt1s  27889  bday1s  27891  cuteq0  27892  cuteq1  27893  mulsrid  28154  precsexlem9  28254  precsexlem11  28256  dfn0s2  28351  n0scut  28353  1p1e2s  28415  nohalf  28422  expsval  28423  axlowdimlem4  28975  axlowdimlem6  28977  upgrbi  29125  usgrexmpllem  29292  clwwlknon1sn  30129  uhgr3cyclex  30211  konigsberglem1  30281  konigsberglem2  30282  konigsberglem3  30283  ex-opab  30461  ex-eprel  30462  ex-id  30463  ex-xp  30465  ex-cnv  30466  ex-dm  30468  ex-rn  30469  ex-res  30470  ex-fv  30472  ex-1st  30473  ex-2nd  30474  hhph  31207  hlim0  31264  hsn0elch  31277  elch0  31283  hhssabloilem  31290  choc0  31355  shintcli  31358  shincli  31391  chincli  31489  h1deoi  31578  h1de2bi  31583  h1de2ctlem  31584  spansni  31586  df0op2  31781  ho01i  31857  nmop0h  32020  opsqrlem2  32170  opsqrlem4  32172  opsqrlem5  32173  hmopidmchi  32180  atoml2i  32412  s3clhash  32917  xrge0iifhmeo  33897  rezh  33932  rrhre  33984  sxbrsigalem5  34270  carsgclctunlem2  34301  ballotth  34519  reprsuc  34609  reprlt  34613  reprgt  34615  circlemethnat  34635  circlevma  34636  bnj1015  34955  subfacp1lem3  35167  subfacp1lem5  35169  kur14lem7  35197  kur14lem9  35199  mrsubcv  35495  mrsubrn  35498  mvhf1  35544  msubvrs  35545  onsucsuccmpi  36426  finxpreclem2  37373  poimirlem26  37633  poimirlem27  37634  poimir  37640  mbfresfi  37653  fdc  37732  rabren3dioph  42803  cllem0  43556  rclexi  43605  trclexi  43610  rtrclexi  43611  frege54cor1c  43905  dffrege76  43929  frege83  43936  frege97  43950  frege98  43951  dffrege99  43952  frege104  43957  frege109  43962  frege110  43963  frege131  43984  frege133  43986  clsk1independent  44036  imaexi  45164  xrlexaddrp  45302  limsup10exlem  45728  wallispilem2  46022  stirlinglem14  46043  fourierdlem70  46132  fourierdlem83  46145  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem114  46176  fouriersw  46187  sge0tsms  46336  omeunle  46472  0ome  46485  ovn0lem  46521  hoidmvlelem3  46553  ovnhoilem1  46557  vonicclem2  46640  mbfresmf  46695  smfpimcclem  46763  nfermltl8rev  47667  nfermltlrev  47669  usgrexmpl1lem  47916  usgrexmpl2lem  47921  usgrexmpl2nb0  47926  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  usgrexmpl2trifr  47932