Theorem elexi 3476

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  elpwi2  5304  funopdmsn  7186  caovmo  7690  pwen  9207  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  rankxplim3  9935  mappwen  10230  ackbij1lem5  10340  alephom  10709  inar1  10899  prlem934  11157  0idsr  11221  recexsrlem  11227  supsrlem  11235  opelreal  11254  elreal  11255  elreal2  11256  eqresr  11261  axmulass  11281  ax1ne0  11284  c0ex  11339  1ex  11342  2ex  12460  3ex  12465  elxr  13285  xnegex  13378  xaddval  13393  xmulval  13395  om2uzrdg  14139  hashxplem  14619  caucvgr  15887  rpnnen  16439  rexpen  16440  phimullem  17000  prmreclem6  17143  efgval  19982  cnfldfun  21744  cnfldfunALT  21745  psdmul  22542  psdmvr  22545  coe1mul2  22643  dscmet  24946  dscopn  24947  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  bndth  25334  mbfimaopnlem  26031  mdegcl  26442  pige3ALT  26905  cxpval  27049  1cubr  27227  emcllem7  27386  basellem7  27471  prmorcht  27562  sqff1o  27566  ppiublem2  27587  lgsval  27685  lgsdir2lem3  27711  nofv  28071  ltsres  28076  noextend  28080  noextendgt  28084  nolesgn2ores  28086  nosepnelem  28093  nosepdmlem  28097  nolt02o  28109  nosupno  28117  nosupbnd1lem3  28124  nosupbnd1  28128  nosupbnd2lem1  28129  nosupbnd2  28130  0lt1s  28255  bday1  28257  cuteq0  28258  cuteq1  28260  mulsrid  28556  precsexlem9  28658  precsexlem11  28660  dfn0s2  28775  n0cut  28777  zsoring  28852  twocut  28866  expsval  28868  1reno  28940  axlowdimlem4  29580  axlowdimlem6  29582  upgrbi  29728  usgrexmpllem  29898  clwwlknon1sn  30748  uhgr3cyclex  30840  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  ex-opab  31090  ex-eprel  31091  ex-id  31092  ex-xp  31094  ex-cnv  31095  ex-dm  31097  ex-rn  31098  ex-res  31099  ex-fv  31101  ex-1st  31102  ex-2nd  31103  hhph  31837  hlim0  31894  hsn0elch  31907  elch0  31913  hhssabloilem  31920  choc0  31985  shintcli  31988  shincli  32021  chincli  32119  h1deoi  32208  h1de2bi  32213  h1de2ctlem  32214  spansni  32216  df0op2  32411  ho01i  32487  nmop0h  32650  opsqrlem2  32800  opsqrlem4  32802  opsqrlem5  32803  hmopidmchi  32810  atoml2i  33042  s3clhash  33608  xrge0iifhmeo  34679  rezh  34712  rrhre  34764  sxbrsigalem5  35031  carsgclctunlem2  35062  ballotth  35281  reprsuc  35355  reprlt  35359  reprgt  35361  circlemethnat  35381  circlevma  35382  bnj1015  35703  jltalephlem  36066  subfacp1lem3  36155  subfacp1lem5  36157  kur14lem7  36185  kur14lem9  36187  mrsubcv  36483  mrsubrn  36486  mvhf1  36532  msubvrs  36533  onsucsuccmpi  37446  finxpreclem2  38581  poimirlem26  38832  poimirlem27  38833  poimir  38839  mbfresfi  38852  fdc  38945  rabren3dioph  44088  cllem0  44828  rclexi  44876  trclexi  44881  rtrclexi  44882  frege54cor1c  45176  dffrege76  45200  frege83  45207  frege97  45221  frege98  45222  dffrege99  45223  frege104  45228  frege109  45233  frege110  45234  frege131  45255  frege133  45257  clsk1independent  45307  imaexi  46507  xrlexaddrp  46637  limsup10exlem  47055  wallispilem2  47349  stirlinglem14  47370  fourierdlem70  47459  fourierdlem83  47472  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  fouriersw  47514  sge0tsms  47663  omeunle  47799  0ome  47812  ovn0lem  47848  hoidmvlelem3  47880  ovnhoilem1  47884  vonicclem2  47967  mbfresmf  48022  smfpimcclem  48090  lamberte  48211  nfermltl8rev  49113  nfermltlrev  49115  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb0  49402  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  veronesematbasd  51408  veroquadgsumlem  51411  veroquadmodzerod  51412  veroquadnolindfd  51413  veroquaddetzerod  51414