Theorem elexi 3452

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  elpwi2  5276  funopdmsn  7104  caovmo  7604  pwen  9088  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  rankxplim3  9805  mappwen  10034  ackbij1lem5  10145  alephom  10508  inar1  10698  prlem934  10956  0idsr  11020  recexsrlem  11026  supsrlem  11034  opelreal  11053  elreal  11054  elreal2  11055  eqresr  11060  axmulass  11080  ax1ne0  11083  c0ex  11138  1ex  11140  2ex  12258  3ex  12263  elxr  13067  xnegex  13160  xaddval  13175  xmulval  13177  om2uzrdg  13918  hashxplem  14395  caucvgr  15638  rpnnen  16194  rexpen  16195  phimullem  16749  prmreclem6  16892  efgval  19692  cnfldfun  21366  cnfldfunALT  21367  psdmul  22132  psdmvr  22135  coe1mul2  22234  dscmet  24537  dscopn  24538  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  bndth  24925  mbfimaopnlem  25622  mdegcl  26034  pige3ALT  26484  cxpval  26628  1cubr  26806  emcllem7  26965  basellem7  27050  prmorcht  27141  sqff1o  27145  ppiublem2  27166  lgsval  27264  lgsdir2lem3  27290  nofv  27621  ltsres  27626  noextend  27630  noextendgt  27634  nolesgn2ores  27636  nosepnelem  27643  nosepdmlem  27647  nolt02o  27659  nosupno  27667  nosupbnd1lem3  27674  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  0lt1s  27804  bday1  27806  cuteq0  27807  cuteq1  27809  mulsrid  28105  precsexlem9  28207  precsexlem11  28209  dfn0s2  28324  n0cut  28326  zsoring  28401  twocut  28415  expsval  28417  1reno  28489  axlowdimlem4  29014  axlowdimlem6  29016  upgrbi  29162  usgrexmpllem  29329  clwwlknon1sn  30170  uhgr3cyclex  30252  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  ex-opab  30502  ex-eprel  30503  ex-id  30504  ex-xp  30506  ex-cnv  30507  ex-dm  30509  ex-rn  30510  ex-res  30511  ex-fv  30513  ex-1st  30514  ex-2nd  30515  hhph  31249  hlim0  31306  hsn0elch  31319  elch0  31325  hhssabloilem  31332  choc0  31397  shintcli  31400  shincli  31433  chincli  31531  h1deoi  31620  h1de2bi  31625  h1de2ctlem  31626  spansni  31628  df0op2  31823  ho01i  31899  nmop0h  32062  opsqrlem2  32212  opsqrlem4  32214  opsqrlem5  32215  hmopidmchi  32222  atoml2i  32454  s3clhash  33008  xrge0iifhmeo  34080  rezh  34113  rrhre  34165  sxbrsigalem5  34432  carsgclctunlem2  34463  ballotth  34682  reprsuc  34759  reprlt  34763  reprgt  34765  circlemethnat  34785  circlevma  34786  bnj1015  35104  subfacp1lem3  35364  subfacp1lem5  35366  kur14lem7  35394  kur14lem9  35396  mrsubcv  35692  mrsubrn  35695  mvhf1  35741  msubvrs  35742  onsucsuccmpi  36625  finxpreclem2  37706  poimirlem26  37967  poimirlem27  37968  poimir  37974  mbfresfi  37987  fdc  38066  rabren3dioph  43243  cllem0  43993  rclexi  44042  trclexi  44047  rtrclexi  44048  frege54cor1c  44342  dffrege76  44366  frege83  44373  frege97  44387  frege98  44388  dffrege99  44389  frege104  44394  frege109  44399  frege110  44400  frege131  44421  frege133  44423  clsk1independent  44473  imaexi  45650  xrlexaddrp  45782  limsup10exlem  46200  wallispilem2  46494  stirlinglem14  46515  fourierdlem70  46604  fourierdlem83  46617  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  fouriersw  46659  sge0tsms  46808  omeunle  46944  0ome  46957  ovn0lem  46993  hoidmvlelem3  47025  ovnhoilem1  47029  vonicclem2  47112  mbfresmf  47167  smfpimcclem  47235  lamberte  47336  nfermltl8rev  48218  nfermltlrev  48220  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513