Theorem elexi 3456

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

Syntax hints:   ∈ wcel 2081  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-v 3439

This theorem is referenced by:  onunisuci  6179  funopdmsn  6775  caovmo  7241  1oex  7961  pwen  8537  cnfcom2  9011  cnfcom3lem  9012  cnfcom3  9013  rankxplim3  9156  mappwen  9384  ackbij1lem5  9492  alephom  9853  inar1  10043  prlem934  10301  0idsr  10365  recexsrlem  10371  supsrlem  10379  opelreal  10398  elreal  10399  elreal2  10400  eqresr  10405  axmulass  10425  ax1ne0  10428  c0ex  10481  1ex  10483  pnfexOLD  10542  2ex  11562  3ex  11567  elxr  12361  xnegex  12451  xaddval  12466  xmulval  12468  om2uzrdg  13174  hashxplem  13642  caucvgr  14866  rpnnen  15413  rexpen  15414  phimullem  15945  prmreclem6  16086  efgval  18570  coe1mul2  20120  cnfldfun  20239  cnfldfunALT  20240  dscmet  22865  dscopn  22866  icopnfhmeo  23230  iccpnfhmeo  23232  xrhmeo  23233  bndth  23245  mbfimaopnlem  23939  mdegcl  24346  pige3ALT  24788  cxpval  24928  1cubr  25101  emcllem7  25261  basellem7  25346  prmorcht  25437  sqff1o  25441  ppiublem2  25461  lgsval  25559  lgsdir2lem3  25585  axlowdimlem4  26414  axlowdimlem6  26416  upgrbi  26561  usgrexmpllem  26725  clwwlknon1sn  27566  uhgr3cyclex  27648  konigsberglem1  27721  konigsberglem2  27722  konigsberglem3  27723  ex-opab  27903  ex-eprel  27904  ex-id  27905  ex-xp  27907  ex-cnv  27908  ex-dm  27910  ex-rn  27911  ex-res  27912  ex-fv  27914  ex-1st  27915  ex-2nd  27916  hhph  28646  hlim0  28703  hsn0elch  28716  elch0  28722  hhssabloilem  28729  choc0  28794  shintcli  28797  shincli  28830  chincli  28928  h1deoi  29017  h1de2bi  29022  h1de2ctlem  29023  spansni  29025  df0op2  29220  ho01i  29296  nmop0h  29459  opsqrlem2  29609  opsqrlem4  29611  opsqrlem5  29612  hmopidmchi  29619  atoml2i  29851  s3clhash  30304  xrge0iifhmeo  30796  rezh  30829  rrhre  30879  sxbrsigalem5  31163  carsgclctunlem2  31194  ballotth  31412  reprsuc  31503  reprlt  31507  reprgt  31509  circlemethnat  31529  circlevma  31530  bnj1015  31849  subfacp1lem3  32038  subfacp1lem5  32040  kur14lem7  32068  kur14lem9  32070  mrsubcv  32366  mrsubrn  32369  mvhf1  32415  msubvrs  32416  nofv  32774  sltres  32779  noextend  32783  noextendgt  32787  nolesgn2ores  32789  nosepnelem  32794  nosepdmlem  32797  nolt02o  32809  nosupno  32813  nosupbday  32815  nosupbnd1lem3  32820  nosupbnd1  32824  nosupbnd2lem1  32825  nosupbnd2  32826  onsucsuccmpi  33401  finxpreclem2  34221  poimirlem26  34468  poimirlem27  34469  poimir  34475  mbfresfi  34488  fdc  34571  rabren3dioph  38916  cllem0  39429  rclexi  39479  trclexi  39484  rtrclexi  39485  frege54cor1c  39765  dffrege76  39789  frege83  39796  frege97  39810  frege98  39811  dffrege99  39812  frege104  39817  frege109  39822  frege110  39823  frege131  39844  frege133  39846  clsk1independent  39900  rpex  41174  xrlexaddrp  41180  limsup10exlem  41614  limsup10ex  41615  wallispilem2  41913  stirlinglem14  41934  fourierdlem70  42023  fourierdlem83  42036  fourierdlem102  42055  fourierdlem103  42056  fourierdlem104  42057  fourierdlem114  42067  fouriersw  42078  sge0tsms  42224  omeunle  42360  0ome  42373  ovn0lem  42409  hoidmvlelem3  42441  ovnhoilem1  42445  vonicclem2  42528  mbfresmf  42578  smfpimcclem  42643  nfermltl8rev  43409  nfermltlrev  43411