Theorem elexi 3503

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  elpwi2  5335  funopdmsn  7170  caovmo  7670  pwen  9190  cnfcom2  9742  cnfcom3lem  9743  cnfcom3  9744  rankxplim3  9921  mappwen  10152  ackbij1lem5  10263  alephom  10625  inar1  10815  prlem934  11073  0idsr  11137  recexsrlem  11143  supsrlem  11151  opelreal  11170  elreal  11171  elreal2  11172  eqresr  11177  axmulass  11197  ax1ne0  11200  c0ex  11255  1ex  11257  2ex  12343  3ex  12348  elxr  13158  xnegex  13250  xaddval  13265  xmulval  13267  om2uzrdg  13997  hashxplem  14472  caucvgr  15712  rpnnen  16263  rexpen  16264  phimullem  16816  prmreclem6  16959  efgval  19735  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  psdmul  22170  psdmvr  22173  coe1mul2  22272  dscmet  24585  dscopn  24586  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  bndth  24990  mbfimaopnlem  25690  mdegcl  26108  pige3ALT  26562  cxpval  26706  1cubr  26885  emcllem7  27045  basellem7  27130  prmorcht  27221  sqff1o  27225  ppiublem2  27247  lgsval  27345  lgsdir2lem3  27371  nofv  27702  sltres  27707  noextend  27711  noextendgt  27715  nolesgn2ores  27717  nosepnelem  27724  nosepdmlem  27728  nolt02o  27740  nosupno  27748  nosupbnd1lem3  27755  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  0slt1s  27874  bday1s  27876  cuteq0  27877  cuteq1  27878  mulsrid  28139  precsexlem9  28239  precsexlem11  28241  dfn0s2  28336  n0scut  28338  1p1e2s  28400  nohalf  28407  expsval  28408  axlowdimlem4  28960  axlowdimlem6  28962  upgrbi  29110  usgrexmpllem  29277  clwwlknon1sn  30119  uhgr3cyclex  30201  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  ex-opab  30451  ex-eprel  30452  ex-id  30453  ex-xp  30455  ex-cnv  30456  ex-dm  30458  ex-rn  30459  ex-res  30460  ex-fv  30462  ex-1st  30463  ex-2nd  30464  hhph  31197  hlim0  31254  hsn0elch  31267  elch0  31273  hhssabloilem  31280  choc0  31345  shintcli  31348  shincli  31381  chincli  31479  h1deoi  31568  h1de2bi  31573  h1de2ctlem  31574  spansni  31576  df0op2  31771  ho01i  31847  nmop0h  32010  opsqrlem2  32160  opsqrlem4  32162  opsqrlem5  32163  hmopidmchi  32170  atoml2i  32402  s3clhash  32932  xrge0iifhmeo  33935  rezh  33970  rrhre  34022  sxbrsigalem5  34290  carsgclctunlem2  34321  ballotth  34540  reprsuc  34630  reprlt  34634  reprgt  34636  circlemethnat  34656  circlevma  34657  bnj1015  34976  subfacp1lem3  35187  subfacp1lem5  35189  kur14lem7  35217  kur14lem9  35219  mrsubcv  35515  mrsubrn  35518  mvhf1  35564  msubvrs  35565  onsucsuccmpi  36444  finxpreclem2  37391  poimirlem26  37653  poimirlem27  37654  poimir  37660  mbfresfi  37673  fdc  37752  rabren3dioph  42826  cllem0  43579  rclexi  43628  trclexi  43633  rtrclexi  43634  frege54cor1c  43928  dffrege76  43952  frege83  43959  frege97  43973  frege98  43974  dffrege99  43975  frege104  43980  frege109  43985  frege110  43986  frege131  44007  frege133  44009  clsk1independent  44059  imaexi  45226  xrlexaddrp  45363  limsup10exlem  45787  wallispilem2  46081  stirlinglem14  46102  fourierdlem70  46191  fourierdlem83  46204  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  fouriersw  46246  sge0tsms  46395  omeunle  46531  0ome  46544  ovn0lem  46580  hoidmvlelem3  46612  ovnhoilem1  46616  vonicclem2  46699  mbfresmf  46754  smfpimcclem  46822  nfermltl8rev  47729  nfermltlrev  47731  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996