Theorem elexi 3473

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  elpwi2  5293  funopdmsn  7125  caovmo  7629  pwen  9120  cnfcom2  9662  cnfcom3lem  9663  cnfcom3  9664  rankxplim3  9841  mappwen  10072  ackbij1lem5  10183  alephom  10545  inar1  10735  prlem934  10993  0idsr  11057  recexsrlem  11063  supsrlem  11071  opelreal  11090  elreal  11091  elreal2  11092  eqresr  11097  axmulass  11117  ax1ne0  11120  c0ex  11175  1ex  11177  2ex  12270  3ex  12275  elxr  13083  xnegex  13175  xaddval  13190  xmulval  13192  om2uzrdg  13928  hashxplem  14405  caucvgr  15649  rpnnen  16202  rexpen  16203  phimullem  16756  prmreclem6  16899  efgval  19654  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  psdmul  22060  psdmvr  22063  coe1mul2  22162  dscmet  24467  dscopn  24468  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  bndth  24864  mbfimaopnlem  25563  mdegcl  25981  pige3ALT  26436  cxpval  26580  1cubr  26759  emcllem7  26919  basellem7  27004  prmorcht  27095  sqff1o  27099  ppiublem2  27121  lgsval  27219  lgsdir2lem3  27245  nofv  27576  sltres  27581  noextend  27585  noextendgt  27589  nolesgn2ores  27591  nosepnelem  27598  nosepdmlem  27602  nolt02o  27614  nosupno  27622  nosupbnd1lem3  27629  nosupbnd1  27633  nosupbnd2lem1  27634  nosupbnd2  27635  0slt1s  27748  bday1s  27750  cuteq0  27751  cuteq1  27753  mulsrid  28023  precsexlem9  28124  precsexlem11  28126  dfn0s2  28231  n0scut  28233  1p1e2s  28309  twocut  28316  expsval  28318  axlowdimlem4  28879  axlowdimlem6  28881  upgrbi  29027  usgrexmpllem  29194  clwwlknon1sn  30036  uhgr3cyclex  30118  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  ex-opab  30368  ex-eprel  30369  ex-id  30370  ex-xp  30372  ex-cnv  30373  ex-dm  30375  ex-rn  30376  ex-res  30377  ex-fv  30379  ex-1st  30380  ex-2nd  30381  hhph  31114  hlim0  31171  hsn0elch  31184  elch0  31190  hhssabloilem  31197  choc0  31262  shintcli  31265  shincli  31298  chincli  31396  h1deoi  31485  h1de2bi  31490  h1de2ctlem  31491  spansni  31493  df0op2  31688  ho01i  31764  nmop0h  31927  opsqrlem2  32077  opsqrlem4  32079  opsqrlem5  32080  hmopidmchi  32087  atoml2i  32319  s3clhash  32876  xrge0iifhmeo  33933  rezh  33966  rrhre  34018  sxbrsigalem5  34286  carsgclctunlem2  34317  ballotth  34536  reprsuc  34613  reprlt  34617  reprgt  34619  circlemethnat  34639  circlevma  34640  bnj1015  34959  subfacp1lem3  35176  subfacp1lem5  35178  kur14lem7  35206  kur14lem9  35208  mrsubcv  35504  mrsubrn  35507  mvhf1  35553  msubvrs  35554  onsucsuccmpi  36438  finxpreclem2  37385  poimirlem26  37647  poimirlem27  37648  poimir  37654  mbfresfi  37667  fdc  37746  rabren3dioph  42810  cllem0  43562  rclexi  43611  trclexi  43616  rtrclexi  43617  frege54cor1c  43911  dffrege76  43935  frege83  43942  frege97  43956  frege98  43957  dffrege99  43958  frege104  43963  frege109  43968  frege110  43969  frege131  43990  frege133  43992  clsk1independent  44042  imaexi  45222  xrlexaddrp  45355  limsup10exlem  45777  wallispilem2  46071  stirlinglem14  46092  fourierdlem70  46181  fourierdlem83  46194  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  fouriersw  46236  sge0tsms  46385  omeunle  46521  0ome  46534  ovn0lem  46570  hoidmvlelem3  46602  ovnhoilem1  46606  vonicclem2  46689  mbfresmf  46744  smfpimcclem  46812  lamberte  46896  nfermltl8rev  47747  nfermltlrev  47749  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032