Theorem elexi 2764

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

Syntax hints:   ∈ wcel 2160  Vcvv 2752

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 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  elpwi2  4176  onunisuci  4450  ordsoexmid  4579  1oex  6450  fnoei  6478  oeiexg  6479  endisj  6851  unfiexmid  6947  snexxph  6980  djuex  7073  0ct  7137  nninfex  7151  infnninfOLD  7154  nnnninf  7155  ctssexmid  7179  nninfdcinf  7200  nninfwlporlem  7202  nninfwlpoimlemg  7204  pm54.43  7220  pw1ne3  7260  3nsssucpw1  7266  2omotaplemst  7288  prarloclemarch2  7449  opelreal  7857  elreal  7858  elreal2  7860  eqresr  7866  c0ex  7982  1ex  7983  pnfex  8042  sup3exmid  8945  2ex  9022  3ex  9026  elxr  9808  setsslid  12566  setsslnid  12567  prdsex  12777  rmodislmod  13684  fnpsr  13962  lgsdir2lem3  14909  subctctexmid  15229  0nninf  15232  nninffeq  15248