Theorem elexi 3482

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  elpwi2  5305  funopdmsn  7140  caovmo  7644  pwen  9164  cnfcom2  9716  cnfcom3lem  9717  cnfcom3  9718  rankxplim3  9895  mappwen  10126  ackbij1lem5  10237  alephom  10599  inar1  10789  prlem934  11047  0idsr  11111  recexsrlem  11117  supsrlem  11125  opelreal  11144  elreal  11145  elreal2  11146  eqresr  11151  axmulass  11171  ax1ne0  11174  c0ex  11229  1ex  11231  2ex  12317  3ex  12322  elxr  13132  xnegex  13224  xaddval  13239  xmulval  13241  om2uzrdg  13974  hashxplem  14451  caucvgr  15692  rpnnen  16245  rexpen  16246  phimullem  16798  prmreclem6  16941  efgval  19698  cnfldfun  21329  cnfldfunALT  21330  cnfldfunOLD  21342  cnfldfunALTOLD  21343  psdmul  22104  psdmvr  22107  coe1mul2  22206  dscmet  24511  dscopn  24512  icopnfhmeo  24892  iccpnfhmeo  24894  xrhmeo  24895  bndth  24908  mbfimaopnlem  25608  mdegcl  26026  pige3ALT  26481  cxpval  26625  1cubr  26804  emcllem7  26964  basellem7  27049  prmorcht  27140  sqff1o  27144  ppiublem2  27166  lgsval  27264  lgsdir2lem3  27290  nofv  27621  sltres  27626  noextend  27630  noextendgt  27634  nolesgn2ores  27636  nosepnelem  27643  nosepdmlem  27647  nolt02o  27659  nosupno  27667  nosupbnd1lem3  27674  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  0slt1s  27793  bday1s  27795  cuteq0  27796  cuteq1  27798  mulsrid  28068  precsexlem9  28169  precsexlem11  28171  dfn0s2  28276  n0scut  28278  1p1e2s  28354  twocut  28361  expsval  28363  axlowdimlem4  28924  axlowdimlem6  28926  upgrbi  29072  usgrexmpllem  29239  clwwlknon1sn  30081  uhgr3cyclex  30163  konigsberglem1  30233  konigsberglem2  30234  konigsberglem3  30235  ex-opab  30413  ex-eprel  30414  ex-id  30415  ex-xp  30417  ex-cnv  30418  ex-dm  30420  ex-rn  30421  ex-res  30422  ex-fv  30424  ex-1st  30425  ex-2nd  30426  hhph  31159  hlim0  31216  hsn0elch  31229  elch0  31235  hhssabloilem  31242  choc0  31307  shintcli  31310  shincli  31343  chincli  31441  h1deoi  31530  h1de2bi  31535  h1de2ctlem  31536  spansni  31538  df0op2  31733  ho01i  31809  nmop0h  31972  opsqrlem2  32122  opsqrlem4  32124  opsqrlem5  32125  hmopidmchi  32132  atoml2i  32364  s3clhash  32923  xrge0iifhmeo  33967  rezh  34000  rrhre  34052  sxbrsigalem5  34320  carsgclctunlem2  34351  ballotth  34570  reprsuc  34647  reprlt  34651  reprgt  34653  circlemethnat  34673  circlevma  34674  bnj1015  34993  subfacp1lem3  35204  subfacp1lem5  35206  kur14lem7  35234  kur14lem9  35236  mrsubcv  35532  mrsubrn  35535  mvhf1  35581  msubvrs  35582  onsucsuccmpi  36461  finxpreclem2  37408  poimirlem26  37670  poimirlem27  37671  poimir  37677  mbfresfi  37690  fdc  37769  rabren3dioph  42838  cllem0  43590  rclexi  43639  trclexi  43644  rtrclexi  43645  frege54cor1c  43939  dffrege76  43963  frege83  43970  frege97  43984  frege98  43985  dffrege99  43986  frege104  43991  frege109  43996  frege110  43997  frege131  44018  frege133  44020  clsk1independent  44070  imaexi  45245  xrlexaddrp  45379  limsup10exlem  45801  wallispilem2  46095  stirlinglem14  46116  fourierdlem70  46205  fourierdlem83  46218  fourierdlem102  46237  fourierdlem103  46238  fourierdlem104  46239  fourierdlem114  46249  fouriersw  46260  sge0tsms  46409  omeunle  46545  0ome  46558  ovn0lem  46594  hoidmvlelem3  46626  ovnhoilem1  46630  vonicclem2  46713  mbfresmf  46768  smfpimcclem  46836  lamberte  46920  nfermltl8rev  47756  nfermltlrev  47758  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb0  48035  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  usgrexmpl2trifr  48041