Theorem elexi 3465

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

Syntax hints:   ∈ wcel 2106  Vcvv 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448

This theorem is referenced by:  elpwi2  5308  funopdmsn  7101  caovmo  7596  1oexOLD  8437  pwen  9101  cnfcom2  9647  cnfcom3lem  9648  cnfcom3  9649  rankxplim3  9826  mappwen  10057  ackbij1lem5  10169  alephom  10530  inar1  10720  prlem934  10978  0idsr  11042  recexsrlem  11048  supsrlem  11056  opelreal  11075  elreal  11076  elreal2  11077  eqresr  11082  axmulass  11102  ax1ne0  11105  c0ex  11158  1ex  11160  2ex  12239  3ex  12244  elxr  13046  xnegex  13137  xaddval  13152  xmulval  13154  om2uzrdg  13871  hashxplem  14343  caucvgr  15572  rpnnen  16120  rexpen  16121  phimullem  16662  prmreclem6  16804  efgval  19513  cnfldfun  20845  cnfldfunALT  20846  cnfldfunALTOLD  20847  coe1mul2  21677  dscmet  23965  dscopn  23966  icopnfhmeo  24343  iccpnfhmeo  24345  xrhmeo  24346  bndth  24358  mbfimaopnlem  25056  mdegcl  25471  pige3ALT  25913  cxpval  26056  1cubr  26229  emcllem7  26388  basellem7  26473  prmorcht  26564  sqff1o  26568  ppiublem2  26588  lgsval  26686  lgsdir2lem3  26712  nofv  27042  sltres  27047  noextend  27051  noextendgt  27055  nolesgn2ores  27057  nosepnelem  27064  nosepdmlem  27068  nolt02o  27080  nosupno  27088  nosupbnd1lem3  27095  nosupbnd1  27099  nosupbnd2lem1  27100  nosupbnd2  27101  0slt1s  27211  bday1s  27213  cuteq0  27214  mulsrid  27420  mulslid  27421  axlowdimlem4  27957  axlowdimlem6  27959  upgrbi  28107  usgrexmpllem  28271  clwwlknon1sn  29107  uhgr3cyclex  29189  konigsberglem1  29259  konigsberglem2  29260  konigsberglem3  29261  ex-opab  29439  ex-eprel  29440  ex-id  29441  ex-xp  29443  ex-cnv  29444  ex-dm  29446  ex-rn  29447  ex-res  29448  ex-fv  29450  ex-1st  29451  ex-2nd  29452  hhph  30183  hlim0  30240  hsn0elch  30253  elch0  30259  hhssabloilem  30266  choc0  30331  shintcli  30334  shincli  30367  chincli  30465  h1deoi  30554  h1de2bi  30559  h1de2ctlem  30560  spansni  30562  df0op2  30757  ho01i  30833  nmop0h  30996  opsqrlem2  31146  opsqrlem4  31148  opsqrlem5  31149  hmopidmchi  31156  atoml2i  31388  s3clhash  31874  xrge0iifhmeo  32606  rezh  32641  rrhre  32691  sxbrsigalem5  32977  carsgclctunlem2  33008  ballotth  33226  reprsuc  33317  reprlt  33321  reprgt  33323  circlemethnat  33343  circlevma  33344  bnj1015  33663  subfacp1lem3  33863  subfacp1lem5  33865  kur14lem7  33893  kur14lem9  33895  mrsubcv  34191  mrsubrn  34194  mvhf1  34240  msubvrs  34241  onsucsuccmpi  34991  finxpreclem2  35934  poimirlem26  36177  poimirlem27  36178  poimir  36184  mbfresfi  36197  fdc  36277  rabren3dioph  41196  cllem0  41960  rclexi  42009  trclexi  42014  rtrclexi  42015  frege54cor1c  42309  dffrege76  42333  frege83  42340  frege97  42354  frege98  42355  dffrege99  42356  frege104  42361  frege109  42366  frege110  42367  frege131  42388  frege133  42390  clsk1independent  42440  rpex  43701  xrlexaddrp  43707  limsup10exlem  44133  wallispilem2  44427  stirlinglem14  44448  fourierdlem70  44537  fourierdlem83  44550  fourierdlem102  44569  fourierdlem103  44570  fourierdlem104  44571  fourierdlem114  44581  fouriersw  44592  sge0tsms  44741  omeunle  44877  0ome  44890  ovn0lem  44926  hoidmvlelem3  44958  ovnhoilem1  44962  vonicclem2  45045  mbfresmf  45100  smfpimcclem  45168  nfermltl8rev  46054  nfermltlrev  46056