Theorem elexi 2815

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

Syntax hints:   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elpwi2  4248  onunisuci  4529  ordsoexmid  4660  funopdmsn  5833  1oex  6589  fnoei  6619  oeiexg  6620  endisj  7007  unfiexmid  7109  snexxph  7148  djuex  7241  0ct  7305  nninfex  7319  infnninfOLD  7323  nnnninf  7324  ctssexmid  7348  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemg  7373  pm54.43  7394  pw1ne3  7447  3nsssucpw1  7453  2omotaplemst  7476  prarloclemarch2  7638  opelreal  8046  elreal  8047  elreal2  8049  eqresr  8055  c0ex  8172  1ex  8173  pnfex  8232  sup3exmid  9136  2ex  9214  3ex  9218  elxr  10010  xnn0nnen  10698  lsw0  11160  setsslid  13132  setsslnid  13133  bassetsnn  13138  prdsex  13351  rmodislmod  14364  fnpsr  14680  lgsdir2lem3  15758  funvtxval0d  15883  funvtxvalg  15886  funiedgvalg  15887  struct2slots2dom  15888  structiedg0val  15890  edgstruct  15914  3dom  16587  2omapen  16595  subctctexmid  16601  0nninf  16606  nninffeq  16622