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  5345  funopdmsn  7143  caovmo  7639  1oexOLD  8481  pwen  9146  cnfcom2  9693  cnfcom3lem  9694  cnfcom3  9695  rankxplim3  9872  mappwen  10103  ackbij1lem5  10215  alephom  10576  inar1  10766  prlem934  11024  0idsr  11088  recexsrlem  11094  supsrlem  11102  opelreal  11121  elreal  11122  elreal2  11123  eqresr  11128  axmulass  11148  ax1ne0  11151  c0ex  11204  1ex  11206  2ex  12285  3ex  12290  elxr  13092  xnegex  13183  xaddval  13198  xmulval  13200  om2uzrdg  13917  hashxplem  14389  caucvgr  15618  rpnnen  16166  rexpen  16167  phimullem  16708  prmreclem6  16850  efgval  19578  cnfldfun  20941  cnfldfunALT  20942  cnfldfunALTOLD  20943  coe1mul2  21773  dscmet  24063  dscopn  24064  icopnfhmeo  24441  iccpnfhmeo  24443  xrhmeo  24444  bndth  24456  mbfimaopnlem  25154  mdegcl  25569  pige3ALT  26011  cxpval  26154  1cubr  26327  emcllem7  26486  basellem7  26571  prmorcht  26662  sqff1o  26666  ppiublem2  26686  lgsval  26784  lgsdir2lem3  26810  nofv  27140  sltres  27145  noextend  27149  noextendgt  27153  nolesgn2ores  27155  nosepnelem  27162  nosepdmlem  27166  nolt02o  27178  nosupno  27186  nosupbnd1lem3  27193  nosupbnd1  27197  nosupbnd2lem1  27198  nosupbnd2  27199  0slt1s  27310  bday1s  27312  cuteq0  27313  cuteq1  27314  mulsrid  27549  precsexlem9  27641  precsexlem11  27643  axlowdimlem4  28183  axlowdimlem6  28185  upgrbi  28333  usgrexmpllem  28497  clwwlknon1sn  29333  uhgr3cyclex  29415  konigsberglem1  29485  konigsberglem2  29486  konigsberglem3  29487  ex-opab  29665  ex-eprel  29666  ex-id  29667  ex-xp  29669  ex-cnv  29670  ex-dm  29672  ex-rn  29673  ex-res  29674  ex-fv  29676  ex-1st  29677  ex-2nd  29678  hhph  30409  hlim0  30466  hsn0elch  30479  elch0  30485  hhssabloilem  30492  choc0  30557  shintcli  30560  shincli  30593  chincli  30691  h1deoi  30780  h1de2bi  30785  h1de2ctlem  30786  spansni  30788  df0op2  30983  ho01i  31059  nmop0h  31222  opsqrlem2  31372  opsqrlem4  31374  opsqrlem5  31375  hmopidmchi  31382  atoml2i  31614  s3clhash  32092  xrge0iifhmeo  32854  rezh  32889  rrhre  32939  sxbrsigalem5  33225  carsgclctunlem2  33256  ballotth  33474  reprsuc  33565  reprlt  33569  reprgt  33571  circlemethnat  33591  circlevma  33592  bnj1015  33911  subfacp1lem3  34111  subfacp1lem5  34113  kur14lem7  34141  kur14lem9  34143  mrsubcv  34439  mrsubrn  34442  mvhf1  34488  msubvrs  34489  onsucsuccmpi  35266  finxpreclem2  36209  poimirlem26  36452  poimirlem27  36453  poimir  36459  mbfresfi  36472  fdc  36551  rabren3dioph  41486  cllem0  42250  rclexi  42299  trclexi  42304  rtrclexi  42305  frege54cor1c  42599  dffrege76  42623  frege83  42630  frege97  42644  frege98  42645  dffrege99  42646  frege104  42651  frege109  42656  frege110  42657  frege131  42678  frege133  42680  clsk1independent  42730  rpex  43991  xrlexaddrp  43997  limsup10exlem  44423  wallispilem2  44717  stirlinglem14  44738  fourierdlem70  44827  fourierdlem83  44840  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem114  44871  fouriersw  44882  sge0tsms  45031  omeunle  45167  0ome  45180  ovn0lem  45216  hoidmvlelem3  45248  ovnhoilem1  45252  vonicclem2  45335  mbfresmf  45390  smfpimcclem  45458  nfermltl8rev  46345  nfermltlrev  46347