Theorem elexi 2772

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

Syntax hints:   ∈ wcel 2164  Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elpwi2  4187  onunisuci  4463  ordsoexmid  4594  1oex  6477  fnoei  6505  oeiexg  6506  endisj  6878  unfiexmid  6974  snexxph  7009  djuex  7102  0ct  7166  nninfex  7180  infnninfOLD  7184  nnnninf  7185  ctssexmid  7209  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemg  7234  pm54.43  7250  pw1ne3  7290  3nsssucpw1  7296  2omotaplemst  7318  prarloclemarch2  7479  opelreal  7887  elreal  7888  elreal2  7890  eqresr  7896  c0ex  8013  1ex  8014  pnfex  8073  sup3exmid  8976  2ex  9054  3ex  9058  elxr  9842  xnn0nnen  10508  setsslid  12669  setsslnid  12670  prdsex  12880  rmodislmod  13847  fnpsr  14153  lgsdir2lem3  15146  subctctexmid  15491  0nninf  15494  nninffeq  15510