Theorem elexi 3470

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447

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 3449

This theorem is referenced by:  elpwi2  5290  funopdmsn  7122  caovmo  7626  pwen  9114  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  rankxplim3  9834  mappwen  10065  ackbij1lem5  10176  alephom  10538  inar1  10728  prlem934  10986  0idsr  11050  recexsrlem  11056  supsrlem  11064  opelreal  11083  elreal  11084  elreal2  11085  eqresr  11090  axmulass  11110  ax1ne0  11113  c0ex  11168  1ex  11170  2ex  12263  3ex  12268  elxr  13076  xnegex  13168  xaddval  13183  xmulval  13185  om2uzrdg  13921  hashxplem  14398  caucvgr  15642  rpnnen  16195  rexpen  16196  phimullem  16749  prmreclem6  16892  efgval  19647  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  psdmul  22053  psdmvr  22056  coe1mul2  22155  dscmet  24460  dscopn  24461  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  bndth  24857  mbfimaopnlem  25556  mdegcl  25974  pige3ALT  26429  cxpval  26573  1cubr  26752  emcllem7  26912  basellem7  26997  prmorcht  27088  sqff1o  27092  ppiublem2  27114  lgsval  27212  lgsdir2lem3  27238  nofv  27569  sltres  27574  noextend  27578  noextendgt  27582  nolesgn2ores  27584  nosepnelem  27591  nosepdmlem  27595  nolt02o  27607  nosupno  27615  nosupbnd1lem3  27622  nosupbnd1  27626  nosupbnd2lem1  27627  nosupbnd2  27628  0slt1s  27741  bday1s  27743  cuteq0  27744  cuteq1  27746  mulsrid  28016  precsexlem9  28117  precsexlem11  28119  dfn0s2  28224  n0scut  28226  1p1e2s  28302  twocut  28309  expsval  28311  axlowdimlem4  28872  axlowdimlem6  28874  upgrbi  29020  usgrexmpllem  29187  clwwlknon1sn  30029  uhgr3cyclex  30111  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  ex-opab  30361  ex-eprel  30362  ex-id  30363  ex-xp  30365  ex-cnv  30366  ex-dm  30368  ex-rn  30369  ex-res  30370  ex-fv  30372  ex-1st  30373  ex-2nd  30374  hhph  31107  hlim0  31164  hsn0elch  31177  elch0  31183  hhssabloilem  31190  choc0  31255  shintcli  31258  shincli  31291  chincli  31389  h1deoi  31478  h1de2bi  31483  h1de2ctlem  31484  spansni  31486  df0op2  31681  ho01i  31757  nmop0h  31920  opsqrlem2  32070  opsqrlem4  32072  opsqrlem5  32073  hmopidmchi  32080  atoml2i  32312  s3clhash  32869  xrge0iifhmeo  33926  rezh  33959  rrhre  34011  sxbrsigalem5  34279  carsgclctunlem2  34310  ballotth  34529  reprsuc  34606  reprlt  34610  reprgt  34612  circlemethnat  34632  circlevma  34633  bnj1015  34952  subfacp1lem3  35169  subfacp1lem5  35171  kur14lem7  35199  kur14lem9  35201  mrsubcv  35497  mrsubrn  35500  mvhf1  35546  msubvrs  35547  onsucsuccmpi  36431  finxpreclem2  37378  poimirlem26  37640  poimirlem27  37641  poimir  37647  mbfresfi  37660  fdc  37739  rabren3dioph  42803  cllem0  43555  rclexi  43604  trclexi  43609  rtrclexi  43610  frege54cor1c  43904  dffrege76  43928  frege83  43935  frege97  43949  frege98  43950  dffrege99  43951  frege104  43956  frege109  43961  frege110  43962  frege131  43983  frege133  43985  clsk1independent  44035  imaexi  45215  xrlexaddrp  45348  limsup10exlem  45770  wallispilem2  46064  stirlinglem14  46085  fourierdlem70  46174  fourierdlem83  46187  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  fouriersw  46229  sge0tsms  46378  omeunle  46514  0ome  46527  ovn0lem  46563  hoidmvlelem3  46595  ovnhoilem1  46599  vonicclem2  46682  mbfresmf  46737  smfpimcclem  46805  lamberte  46889  nfermltl8rev  47743  nfermltlrev  47745  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028