Theorem elexi 2783

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 2782	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2175  Vcvv 2771

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  elpwi2  4201  onunisuci  4478  ordsoexmid  4609  funopdmsn  5763  1oex  6509  fnoei  6537  oeiexg  6538  endisj  6918  unfiexmid  7014  snexxph  7051  djuex  7144  0ct  7208  nninfex  7222  infnninfOLD  7226  nnnninf  7227  ctssexmid  7251  nninfdcinf  7272  nninfwlporlem  7274  nninfwlpoimlemg  7276  pm54.43  7297  pw1ne3  7341  3nsssucpw1  7347  2omotaplemst  7369  prarloclemarch2  7531  opelreal  7939  elreal  7940  elreal2  7942  eqresr  7948  c0ex  8065  1ex  8066  pnfex  8125  sup3exmid  9029  2ex  9107  3ex  9111  elxr  9897  xnn0nnen  10580  lsw0  11039  setsslid  12854  setsslnid  12855  prdsex  13072  rmodislmod  14084  fnpsr  14400  lgsdir2lem3  15478  funvtxval0d  15601  funvtxvalg  15604  funiedgvalg  15605  struct2slots2dom  15606  structiedg0val  15608  2omapen  15895  subctctexmid  15899  0nninf  15903  nninffeq  15919