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

Syntax hints:   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456

This theorem is referenced by:  elpwi2  5291  funopdmsn  7133  caovmo  7633  pwen  9122  cnfcom2  9657  cnfcom3lem  9658  cnfcom3  9659  rankxplim3  9839  mappwen  10068  ackbij1lem5  10179  alephom  10543  inar1  10733  prlem934  10991  0idsr  11055  recexsrlem  11061  supsrlem  11069  opelreal  11088  elreal  11089  elreal2  11090  eqresr  11095  axmulass  11115  ax1ne0  11118  c0ex  11173  1ex  11176  2ex  12295  3ex  12300  elxr  13118  xnegex  13211  xaddval  13226  xmulval  13228  om2uzrdg  13969  hashxplem  14446  caucvgr  15703  rpnnen  16259  rexpen  16260  phimullem  16814  prmreclem6  16957  efgval  19757  cnfldfun  21438  cnfldfunALT  21439  psdmul  22231  psdmvr  22234  coe1mul2  22332  dscmet  24632  dscopn  24633  icopnfhmeo  25005  iccpnfhmeo  25007  xrhmeo  25008  bndth  25020  mbfimaopnlem  25717  mdegcl  26129  pige3ALT  26585  cxpval  26729  1cubr  26907  emcllem7  27066  basellem7  27151  prmorcht  27242  sqff1o  27246  ppiublem2  27267  lgsval  27365  lgsdir2lem3  27391  nofv  27721  ltsres  27726  noextend  27730  noextendgt  27734  nolesgn2ores  27736  nosepnelem  27743  nosepdmlem  27747  nolt02o  27759  nosupno  27767  nosupbnd1lem3  27774  nosupbnd1  27778  nosupbnd2lem1  27779  nosupbnd2  27780  0lt1s  27905  bday1  27907  cuteq0  27908  cuteq1  27910  mulsrid  28206  precsexlem9  28308  precsexlem11  28310  dfn0s2  28425  n0cut  28427  zsoring  28502  twocut  28516  expsval  28518  1reno  28590  axlowdimlem4  29146  axlowdimlem6  29148  upgrbi  29294  usgrexmpllem  29461  clwwlknon1sn  30302  uhgr3cyclex  30384  konigsberglem1  30454  konigsberglem2  30455  konigsberglem3  30456  ex-opab  30634  ex-eprel  30635  ex-id  30636  ex-xp  30638  ex-cnv  30639  ex-dm  30641  ex-rn  30642  ex-res  30643  ex-fv  30645  ex-1st  30646  ex-2nd  30647  hhph  31381  hlim0  31438  hsn0elch  31451  elch0  31457  hhssabloilem  31464  choc0  31529  shintcli  31532  shincli  31565  chincli  31663  h1deoi  31752  h1de2bi  31757  h1de2ctlem  31758  spansni  31760  df0op2  31955  ho01i  32031  nmop0h  32194  opsqrlem2  32344  opsqrlem4  32346  opsqrlem5  32347  hmopidmchi  32354  atoml2i  32586  s3clhash  33126  xrge0iifhmeo  34233  rezh  34266  rrhre  34318  sxbrsigalem5  34585  carsgclctunlem2  34616  ballotth  34835  reprsuc  34909  reprlt  34913  reprgt  34915  circlemethnat  34935  circlevma  34936  bnj1015  35257  subfacp1lem3  35532  subfacp1lem5  35534  kur14lem7  35562  kur14lem9  35564  mrsubcv  35860  mrsubrn  35863  mvhf1  35909  msubvrs  35910  onsucsuccmpi  36803  finxpreclem2  37884  poimirlem26  38145  poimirlem27  38146  poimir  38152  mbfresfi  38165  fdc  38244  rabren3dioph  43392  cllem0  44142  rclexi  44191  trclexi  44196  rtrclexi  44197  frege54cor1c  44491  dffrege76  44515  frege83  44522  frege97  44536  frege98  44537  dffrege99  44538  frege104  44543  frege109  44548  frege110  44549  frege131  44570  frege133  44572  clsk1independent  44622  imaexi  45797  xrlexaddrp  45928  limsup10exlem  46346  wallispilem2  46640  stirlinglem14  46661  fourierdlem70  46750  fourierdlem83  46763  fourierdlem102  46782  fourierdlem103  46783  fourierdlem104  46784  fourierdlem114  46794  fouriersw  46805  sge0tsms  46954  omeunle  47090  0ome  47103  ovn0lem  47139  hoidmvlelem3  47171  ovnhoilem1  47175  vonicclem2  47258  mbfresmf  47313  smfpimcclem  47381  lamberte  47482  nfermltl8rev  48364  nfermltlrev  48366  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb0  48653  usgrexmpl2nb3  48656  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659