Theorem elexi 3452

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

Syntax hints:   ∈ wcel 2107  Vcvv 3433

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  elpwi2  5271  onunisuci  6384  funopdmsn  7031  caovmo  7518  1oexOLD  8325  pwen  8946  cnfcom2  9469  cnfcom3lem  9470  cnfcom3  9471  rankxplim3  9648  mappwen  9877  ackbij1lem5  9989  alephom  10350  inar1  10540  prlem934  10798  0idsr  10862  recexsrlem  10868  supsrlem  10876  opelreal  10895  elreal  10896  elreal2  10897  eqresr  10902  axmulass  10922  ax1ne0  10925  c0ex  10978  1ex  10980  2ex  12059  3ex  12064  elxr  12861  xnegex  12951  xaddval  12966  xmulval  12968  om2uzrdg  13685  hashxplem  14157  caucvgr  15396  rpnnen  15945  rexpen  15946  phimullem  16489  prmreclem6  16631  efgval  19332  cnfldfun  20618  cnfldfunALT  20619  cnfldfunALTOLD  20620  coe1mul2  21449  dscmet  23737  dscopn  23738  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  bndth  24130  mbfimaopnlem  24828  mdegcl  25243  pige3ALT  25685  cxpval  25828  1cubr  26001  emcllem7  26160  basellem7  26245  prmorcht  26336  sqff1o  26340  ppiublem2  26360  lgsval  26458  lgsdir2lem3  26484  axlowdimlem4  27322  axlowdimlem6  27324  upgrbi  27472  usgrexmpllem  27636  clwwlknon1sn  28473  uhgr3cyclex  28555  konigsberglem1  28625  konigsberglem2  28626  konigsberglem3  28627  ex-opab  28805  ex-eprel  28806  ex-id  28807  ex-xp  28809  ex-cnv  28810  ex-dm  28812  ex-rn  28813  ex-res  28814  ex-fv  28816  ex-1st  28817  ex-2nd  28818  hhph  29549  hlim0  29606  hsn0elch  29619  elch0  29625  hhssabloilem  29632  choc0  29697  shintcli  29700  shincli  29733  chincli  29831  h1deoi  29920  h1de2bi  29925  h1de2ctlem  29926  spansni  29928  df0op2  30123  ho01i  30199  nmop0h  30362  opsqrlem2  30512  opsqrlem4  30514  opsqrlem5  30515  hmopidmchi  30522  atoml2i  30754  s3clhash  31231  xrge0iifhmeo  31895  rezh  31930  rrhre  31980  sxbrsigalem5  32264  carsgclctunlem2  32295  ballotth  32513  reprsuc  32604  reprlt  32608  reprgt  32610  circlemethnat  32630  circlevma  32631  bnj1015  32951  subfacp1lem3  33153  subfacp1lem5  33155  kur14lem7  33183  kur14lem9  33185  mrsubcv  33481  mrsubrn  33484  mvhf1  33530  msubvrs  33531  nofv  33869  sltres  33874  noextend  33878  noextendgt  33882  nolesgn2ores  33884  nosepnelem  33891  nosepdmlem  33895  nolt02o  33907  nosupno  33915  nosupbnd1lem3  33922  nosupbnd1  33926  nosupbnd2lem1  33927  nosupbnd2  33928  0slt1s  34032  bday1s  34034  onsucsuccmpi  34641  finxpreclem2  35570  poimirlem26  35812  poimirlem27  35813  poimir  35819  mbfresfi  35832  fdc  35912  rabren3dioph  40644  cllem0  41180  rclexi  41230  trclexi  41235  rtrclexi  41236  frege54cor1c  41530  dffrege76  41554  frege83  41561  frege97  41575  frege98  41576  dffrege99  41577  frege104  41582  frege109  41587  frege110  41588  frege131  41609  frege133  41611  clsk1independent  41663  rpex  42892  xrlexaddrp  42898  limsup10exlem  43320  wallispilem2  43614  stirlinglem14  43635  fourierdlem70  43724  fourierdlem83  43737  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  fouriersw  43779  sge0tsms  43925  omeunle  44061  0ome  44074  ovn0lem  44110  hoidmvlelem3  44142  ovnhoilem1  44146  vonicclem2  44229  mbfresmf  44284  smfpimcclem  44351  nfermltl8rev  45205  nfermltlrev  45207