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  4241  onunisuci  4522  ordsoexmid  4653  funopdmsn  5818  1oex  6568  fnoei  6596  oeiexg  6597  endisj  6979  unfiexmid  7076  snexxph  7113  djuex  7206  0ct  7270  nninfex  7284  infnninfOLD  7288  nnnninf  7289  ctssexmid  7313  nninfdcinf  7334  nninfwlporlem  7336  nninfwlpoimlemg  7338  pm54.43  7359  pw1ne3  7411  3nsssucpw1  7417  2omotaplemst  7440  prarloclemarch2  7602  opelreal  8010  elreal  8011  elreal2  8013  eqresr  8019  c0ex  8136  1ex  8137  pnfex  8196  sup3exmid  9100  2ex  9178  3ex  9182  elxr  9968  xnn0nnen  10654  lsw0  11114  setsslid  13078  setsslnid  13079  bassetsnn  13084  prdsex  13297  rmodislmod  14309  fnpsr  14625  lgsdir2lem3  15703  funvtxval0d  15828  funvtxvalg  15831  funiedgvalg  15832  struct2slots2dom  15833  structiedg0val  15835  edgstruct  15858  2omapen  16319  subctctexmid  16325  0nninf  16329  nninffeq  16345