Theorem elexi 3494

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  elpwi2  5347  funopdmsn  7148  caovmo  7644  1oexOLD  8486  pwen  9150  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  rankxplim3  9876  mappwen  10107  ackbij1lem5  10219  alephom  10580  inar1  10770  prlem934  11028  0idsr  11092  recexsrlem  11098  supsrlem  11106  opelreal  11125  elreal  11126  elreal2  11127  eqresr  11132  axmulass  11152  ax1ne0  11155  c0ex  11208  1ex  11210  2ex  12289  3ex  12294  elxr  13096  xnegex  13187  xaddval  13202  xmulval  13204  om2uzrdg  13921  hashxplem  14393  caucvgr  15622  rpnnen  16170  rexpen  16171  phimullem  16712  prmreclem6  16854  efgval  19585  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  coe1mul2  21791  dscmet  24081  dscopn  24082  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  bndth  24474  mbfimaopnlem  25172  mdegcl  25587  pige3ALT  26029  cxpval  26172  1cubr  26347  emcllem7  26506  basellem7  26591  prmorcht  26682  sqff1o  26686  ppiublem2  26706  lgsval  26804  lgsdir2lem3  26830  nofv  27160  sltres  27165  noextend  27169  noextendgt  27173  nolesgn2ores  27175  nosepnelem  27182  nosepdmlem  27186  nolt02o  27198  nosupno  27206  nosupbnd1lem3  27213  nosupbnd1  27217  nosupbnd2lem1  27218  nosupbnd2  27219  0slt1s  27331  bday1s  27333  cuteq0  27334  cuteq1  27335  mulsrid  27572  precsexlem9  27664  precsexlem11  27666  dfn0s2  27705  n0scut  27707  axlowdimlem4  28234  axlowdimlem6  28236  upgrbi  28384  usgrexmpllem  28548  clwwlknon1sn  29384  uhgr3cyclex  29466  konigsberglem1  29536  konigsberglem2  29537  konigsberglem3  29538  ex-opab  29716  ex-eprel  29717  ex-id  29718  ex-xp  29720  ex-cnv  29721  ex-dm  29723  ex-rn  29724  ex-res  29725  ex-fv  29727  ex-1st  29728  ex-2nd  29729  hhph  30462  hlim0  30519  hsn0elch  30532  elch0  30538  hhssabloilem  30545  choc0  30610  shintcli  30613  shincli  30646  chincli  30744  h1deoi  30833  h1de2bi  30838  h1de2ctlem  30839  spansni  30841  df0op2  31036  ho01i  31112  nmop0h  31275  opsqrlem2  31425  opsqrlem4  31427  opsqrlem5  31428  hmopidmchi  31435  atoml2i  31667  s3clhash  32145  xrge0iifhmeo  32947  rezh  32982  rrhre  33032  sxbrsigalem5  33318  carsgclctunlem2  33349  ballotth  33567  reprsuc  33658  reprlt  33662  reprgt  33664  circlemethnat  33684  circlevma  33685  bnj1015  34004  subfacp1lem3  34204  subfacp1lem5  34206  kur14lem7  34234  kur14lem9  34236  mrsubcv  34532  mrsubrn  34535  mvhf1  34581  msubvrs  34582  gg-cnfldfun  35228  gg-cnfldfunALT  35229  onsucsuccmpi  35376  finxpreclem2  36319  poimirlem26  36562  poimirlem27  36563  poimir  36569  mbfresfi  36582  fdc  36661  rabren3dioph  41601  cllem0  42365  rclexi  42414  trclexi  42419  rtrclexi  42420  frege54cor1c  42714  dffrege76  42738  frege83  42745  frege97  42759  frege98  42760  dffrege99  42761  frege104  42766  frege109  42771  frege110  42772  frege131  42793  frege133  42795  clsk1independent  42845  rpex  44104  xrlexaddrp  44110  limsup10exlem  44536  wallispilem2  44830  stirlinglem14  44851  fourierdlem70  44940  fourierdlem83  44953  fourierdlem102  44972  fourierdlem103  44973  fourierdlem104  44974  fourierdlem114  44984  fouriersw  44995  sge0tsms  45144  omeunle  45280  0ome  45293  ovn0lem  45329  hoidmvlelem3  45361  ovnhoilem1  45365  vonicclem2  45448  mbfresmf  45503  smfpimcclem  45571  nfermltl8rev  46458  nfermltlrev  46460