Theorem elexi 3472

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  elpwi2  5300  funopdmsn  7148  caovmo  7652  pwen  9149  cnfcom2  9682  cnfcom3lem  9683  cnfcom3  9684  rankxplim3  9864  mappwen  10116  ackbij1lem5  10226  alephom  10595  inar1  10785  prlem934  11043  0idsr  11107  recexsrlem  11113  supsrlem  11121  opelreal  11140  elreal  11141  elreal2  11142  eqresr  11147  axmulass  11167  ax1ne0  11170  c0ex  11225  1ex  11228  2ex  12343  3ex  12348  elxr  13168  xnegex  13261  xaddval  13276  xmulval  13278  om2uzrdg  14021  hashxplem  14499  caucvgr  15764  rpnnen  16316  rexpen  16317  phimullem  16871  prmreclem6  17014  efgval  19845  cnfldfun  21600  cnfldfunALT  21601  psdmul  22395  psdmvr  22398  coe1mul2  22496  dscmet  24799  dscopn  24800  icopnfhmeo  25172  iccpnfhmeo  25174  xrhmeo  25175  bndth  25187  mbfimaopnlem  25884  mdegcl  26295  pige3ALT  26758  cxpval  26902  1cubr  27080  emcllem7  27239  basellem7  27324  prmorcht  27415  sqff1o  27419  ppiublem2  27440  lgsval  27538  lgsdir2lem3  27564  nofv  27894  ltsres  27899  noextend  27903  noextendgt  27907  nolesgn2ores  27909  nosepnelem  27916  nosepdmlem  27920  nolt02o  27932  nosupno  27940  nosupbnd1lem3  27947  nosupbnd1  27951  nosupbnd2lem1  27952  nosupbnd2  27953  0lt1s  28078  bday1  28080  cuteq0  28081  cuteq1  28083  mulsrid  28379  precsexlem9  28481  precsexlem11  28483  dfn0s2  28598  n0cut  28600  zsoring  28675  twocut  28689  expsval  28691  1reno  28763  axlowdimlem4  29403  axlowdimlem6  29405  upgrbi  29551  usgrexmpllem  29721  clwwlknon1sn  30571  uhgr3cyclex  30663  konigsberglem1  30733  konigsberglem2  30734  konigsberglem3  30735  ex-opab  30913  ex-eprel  30914  ex-id  30915  ex-xp  30917  ex-cnv  30918  ex-dm  30920  ex-rn  30921  ex-res  30922  ex-fv  30924  ex-1st  30925  ex-2nd  30926  hhph  31660  hlim0  31717  hsn0elch  31730  elch0  31736  hhssabloilem  31743  choc0  31808  shintcli  31811  shincli  31844  chincli  31942  h1deoi  32031  h1de2bi  32036  h1de2ctlem  32037  spansni  32039  df0op2  32234  ho01i  32310  nmop0h  32473  opsqrlem2  32623  opsqrlem4  32625  opsqrlem5  32626  hmopidmchi  32633  atoml2i  32865  s3clhash  33392  xrge0iifhmeo  34447  rezh  34480  rrhre  34532  sxbrsigalem5  34800  carsgclctunlem2  34831  ballotth  35050  reprsuc  35124  reprlt  35128  reprgt  35130  circlemethnat  35150  circlevma  35151  bnj1015  35472  subfacp1lem3  35762  subfacp1lem5  35764  kur14lem7  35792  kur14lem9  35794  mrsubcv  36090  mrsubrn  36093  mvhf1  36139  msubvrs  36140  onsucsuccmpi  37063  finxpreclem2  38145  poimirlem26  38396  poimirlem27  38397  poimir  38403  mbfresfi  38416  fdc  38496  rabren3dioph  43657  cllem0  44407  rclexi  44456  trclexi  44461  rtrclexi  44462  frege54cor1c  44756  dffrege76  44780  frege83  44787  frege97  44801  frege98  44802  dffrege99  44803  frege104  44808  frege109  44813  frege110  44814  frege131  44835  frege133  44837  clsk1independent  44887  imaexi  46052  xrlexaddrp  46183  limsup10exlem  46601  wallispilem2  46895  stirlinglem14  46916  fourierdlem70  47005  fourierdlem83  47018  fourierdlem102  47037  fourierdlem103  47038  fourierdlem104  47039  fourierdlem114  47049  fouriersw  47060  sge0tsms  47209  omeunle  47345  0ome  47358  ovn0lem  47394  hoidmvlelem3  47426  ovnhoilem1  47430  vonicclem2  47513  mbfresmf  47568  smfpimcclem  47636  lamberte  47757  nfermltl8rev  48659  nfermltlrev  48661  usgrexmpl1lem  48938  usgrexmpl2lem  48943  usgrexmpl2nb0  48948  usgrexmpl2nb3  48951  usgrexmpl2nb4  48952  usgrexmpl2nb5  48953  usgrexmpl2trifr  48954  veronesematbasd  50814  veroquadgsumlem  50817  veroquadmodzerod  50818  veroquadnolindfd  50819  veroquaddetzerod  50820