Theorem elexi 3453

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 2114  Vcvv 3430

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  elpwi2  5273  funopdmsn  7098  caovmo  7598  pwen  9082  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  rankxplim3  9799  mappwen  10028  ackbij1lem5  10139  alephom  10502  inar1  10692  prlem934  10950  0idsr  11014  recexsrlem  11020  supsrlem  11028  opelreal  11047  elreal  11048  elreal2  11049  eqresr  11054  axmulass  11074  ax1ne0  11077  c0ex  11132  1ex  11134  2ex  12252  3ex  12257  elxr  13061  xnegex  13154  xaddval  13169  xmulval  13171  om2uzrdg  13912  hashxplem  14389  caucvgr  15632  rpnnen  16188  rexpen  16189  phimullem  16743  prmreclem6  16886  efgval  19686  cnfldfun  21361  cnfldfunALT  21362  cnfldfunOLD  21374  cnfldfunALTOLD  21375  psdmul  22145  psdmvr  22148  coe1mul2  22247  dscmet  24550  dscopn  24551  icopnfhmeo  24923  iccpnfhmeo  24925  xrhmeo  24926  bndth  24938  mbfimaopnlem  25635  mdegcl  26047  pige3ALT  26500  cxpval  26644  1cubr  26822  emcllem7  26982  basellem7  27067  prmorcht  27158  sqff1o  27162  ppiublem2  27183  lgsval  27281  lgsdir2lem3  27307  nofv  27638  ltsres  27643  noextend  27647  noextendgt  27651  nolesgn2ores  27653  nosepnelem  27660  nosepdmlem  27664  nolt02o  27676  nosupno  27684  nosupbnd1lem3  27691  nosupbnd1  27695  nosupbnd2lem1  27696  nosupbnd2  27697  0lt1s  27821  bday1  27823  cuteq0  27824  cuteq1  27826  mulsrid  28122  precsexlem9  28224  precsexlem11  28226  dfn0s2  28341  n0cut  28343  zsoring  28418  twocut  28432  expsval  28434  1reno  28506  axlowdimlem4  29031  axlowdimlem6  29033  upgrbi  29179  usgrexmpllem  29346  clwwlknon1sn  30188  uhgr3cyclex  30270  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  ex-opab  30520  ex-eprel  30521  ex-id  30522  ex-xp  30524  ex-cnv  30525  ex-dm  30527  ex-rn  30528  ex-res  30529  ex-fv  30531  ex-1st  30532  ex-2nd  30533  hhph  31267  hlim0  31324  hsn0elch  31337  elch0  31343  hhssabloilem  31350  choc0  31415  shintcli  31418  shincli  31451  chincli  31549  h1deoi  31638  h1de2bi  31643  h1de2ctlem  31644  spansni  31646  df0op2  31841  ho01i  31917  nmop0h  32080  opsqrlem2  32230  opsqrlem4  32232  opsqrlem5  32233  hmopidmchi  32240  atoml2i  32472  s3clhash  33026  xrge0iifhmeo  34099  rezh  34132  rrhre  34184  sxbrsigalem5  34451  carsgclctunlem2  34482  ballotth  34701  reprsuc  34778  reprlt  34782  reprgt  34784  circlemethnat  34804  circlevma  34805  bnj1015  35123  subfacp1lem3  35383  subfacp1lem5  35385  kur14lem7  35413  kur14lem9  35415  mrsubcv  35711  mrsubrn  35714  mvhf1  35760  msubvrs  35761  onsucsuccmpi  36644  finxpreclem2  37723  poimirlem26  37984  poimirlem27  37985  poimir  37991  mbfresfi  38004  fdc  38083  rabren3dioph  43264  cllem0  44014  rclexi  44063  trclexi  44068  rtrclexi  44069  frege54cor1c  44363  dffrege76  44387  frege83  44394  frege97  44408  frege98  44409  dffrege99  44410  frege104  44415  frege109  44420  frege110  44421  frege131  44442  frege133  44444  clsk1independent  44494  imaexi  45671  xrlexaddrp  45803  limsup10exlem  46221  wallispilem2  46515  stirlinglem14  46536  fourierdlem70  46625  fourierdlem83  46638  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  fouriersw  46680  sge0tsms  46829  omeunle  46965  0ome  46978  ovn0lem  47014  hoidmvlelem3  47046  ovnhoilem1  47050  vonicclem2  47133  mbfresmf  47188  smfpimcclem  47256  lamberte  47351  nfermltl8rev  48233  nfermltlrev  48235  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb0  48522  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528