Theorem elexi 2789

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

Syntax hints:   ∈ wcel 2178  Vcvv 2776

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  elpwi2  4218  onunisuci  4497  ordsoexmid  4628  funopdmsn  5787  1oex  6533  fnoei  6561  oeiexg  6562  endisj  6944  unfiexmid  7041  snexxph  7078  djuex  7171  0ct  7235  nninfex  7249  infnninfOLD  7253  nnnninf  7254  ctssexmid  7278  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemg  7303  pm54.43  7324  pw1ne3  7376  3nsssucpw1  7382  2omotaplemst  7405  prarloclemarch2  7567  opelreal  7975  elreal  7976  elreal2  7978  eqresr  7984  c0ex  8101  1ex  8102  pnfex  8161  sup3exmid  9065  2ex  9143  3ex  9147  elxr  9933  xnn0nnen  10619  lsw0  11078  setsslid  12998  setsslnid  12999  prdsex  13216  rmodislmod  14228  fnpsr  14544  lgsdir2lem3  15622  funvtxval0d  15747  funvtxvalg  15750  funiedgvalg  15751  struct2slots2dom  15752  structiedg0val  15754  edgstruct  15775  2omapen  16133  subctctexmid  16139  0nninf  16143  nninffeq  16159