Theorem elexi 2812

Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
elisseti.1	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
elexi	⊢ 𝐴 ∈ V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elisseti.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		elex 2811	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2200  Vcvv 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elpwi2  4242  onunisuci  4523  ordsoexmid  4654  funopdmsn  5823  1oex  6576  fnoei  6606  oeiexg  6607  endisj  6991  unfiexmid  7091  snexxph  7128  djuex  7221  0ct  7285  nninfex  7299  infnninfOLD  7303  nnnninf  7304  ctssexmid  7328  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  pm54.43  7374  pw1ne3  7426  3nsssucpw1  7432  2omotaplemst  7455  prarloclemarch2  7617  opelreal  8025  elreal  8026  elreal2  8028  eqresr  8034  c0ex  8151  1ex  8152  pnfex  8211  sup3exmid  9115  2ex  9193  3ex  9197  elxr  9984  xnn0nnen  10671  lsw0  11132  setsslid  13098  setsslnid  13099  bassetsnn  13104  prdsex  13317  rmodislmod  14330  fnpsr  14646  lgsdir2lem3  15724  funvtxval0d  15849  funvtxvalg  15852  funiedgvalg  15853  struct2slots2dom  15854  structiedg0val  15856  edgstruct  15879  3dom  16411  2omapen  16419  subctctexmid  16425  0nninf  16430  nninffeq  16446