Theorem elexi 3453

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  elpwi2  5263  funopdmsn  7093  caovmo  7593  pwen  9078  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  rankxplim3  9796  mappwen  10025  ackbij1lem5  10136  alephom  10499  inar1  10689  prlem934  10947  0idsr  11011  recexsrlem  11017  supsrlem  11025  opelreal  11044  elreal  11045  elreal2  11046  eqresr  11051  axmulass  11071  ax1ne0  11074  c0ex  11129  1ex  11131  2ex  12249  3ex  12254  elxr  13058  xnegex  13151  xaddval  13166  xmulval  13168  om2uzrdg  13909  hashxplem  14386  caucvgr  15629  rpnnen  16185  rexpen  16186  phimullem  16740  prmreclem6  16883  efgval  19683  cnfldfun  21361  cnfldfunALT  21362  psdmul  22154  psdmvr  22157  coe1mul2  22255  dscmet  24555  dscopn  24556  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  bndth  24943  mbfimaopnlem  25640  mdegcl  26052  pige3ALT  26502  cxpval  26646  1cubr  26824  emcllem7  26983  basellem7  27068  prmorcht  27159  sqff1o  27163  ppiublem2  27184  lgsval  27282  lgsdir2lem3  27308  nofv  27639  ltsres  27644  noextend  27648  noextendgt  27652  nolesgn2ores  27654  nosepnelem  27661  nosepdmlem  27665  nolt02o  27677  nosupno  27685  nosupbnd1lem3  27692  nosupbnd1  27696  nosupbnd2lem1  27697  nosupbnd2  27698  0lt1s  27822  bday1  27824  cuteq0  27825  cuteq1  27827  mulsrid  28123  precsexlem9  28225  precsexlem11  28227  dfn0s2  28342  n0cut  28344  zsoring  28419  twocut  28433  expsval  28435  1reno  28507  axlowdimlem4  29032  axlowdimlem6  29034  upgrbi  29180  usgrexmpllem  29347  clwwlknon1sn  30188  uhgr3cyclex  30270  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  ex-opab  30520  ex-eprel  30521  ex-id  30522  ex-xp  30524  ex-cnv  30525  ex-dm  30527  ex-rn  30528  ex-res  30529  ex-fv  30531  ex-1st  30532  ex-2nd  30533  hhph  31267  hlim0  31324  hsn0elch  31337  elch0  31343  hhssabloilem  31350  choc0  31415  shintcli  31418  shincli  31451  chincli  31549  h1deoi  31638  h1de2bi  31643  h1de2ctlem  31644  spansni  31646  df0op2  31841  ho01i  31917  nmop0h  32080  opsqrlem2  32230  opsqrlem4  32232  opsqrlem5  32233  hmopidmchi  32240  atoml2i  32472  s3clhash  33027  xrge0iifhmeo  34120  rezh  34153  rrhre  34205  sxbrsigalem5  34472  carsgclctunlem2  34503  ballotth  34722  reprsuc  34799  reprlt  34803  reprgt  34805  circlemethnat  34825  circlevma  34826  bnj1015  35144  subfacp1lem3  35410  subfacp1lem5  35412  kur14lem7  35440  kur14lem9  35442  mrsubcv  35738  mrsubrn  35741  mvhf1  35787  msubvrs  35788  onsucsuccmpi  36671  finxpreclem2  37752  poimirlem26  38013  poimirlem27  38014  poimir  38020  mbfresfi  38033  fdc  38112  rabren3dioph  43260  cllem0  44010  rclexi  44059  trclexi  44064  rtrclexi  44065  frege54cor1c  44359  dffrege76  44383  frege83  44390  frege97  44404  frege98  44405  dffrege99  44406  frege104  44411  frege109  44416  frege110  44417  frege131  44438  frege133  44440  clsk1independent  44490  imaexi  45666  xrlexaddrp  45797  limsup10exlem  46215  wallispilem2  46509  stirlinglem14  46530  fourierdlem70  46619  fourierdlem83  46632  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  fouriersw  46674  sge0tsms  46823  omeunle  46959  0ome  46972  ovn0lem  47008  hoidmvlelem3  47040  ovnhoilem1  47044  vonicclem2  47127  mbfresmf  47182  smfpimcclem  47250  lamberte  47351  nfermltl8rev  48233  nfermltlrev  48235  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb0  48522  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528