Theorem elexi 2812

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	|- A e. B

Assertion

Ref	Expression
elexi	|- A e. _V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elisseti.1	. 2 |- A e. B
2		elex 2811	. 2 |- ( A e. B -> A e. _V )
3	1, 2	ax-mp 5	1 |- A e. _V

Syntax hints:   e. wcel 2200   _Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elpwi2  4242  onunisuci  4523  ordsoexmid  4654  funopdmsn  5819  1oex  6570  fnoei  6598  oeiexg  6599  endisj  6983  unfiexmid  7080  snexxph  7117  djuex  7210  0ct  7274  nninfex  7288  infnninfOLD  7292  nnnninf  7293  ctssexmid  7317  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemg  7342  pm54.43  7363  pw1ne3  7415  3nsssucpw1  7421  2omotaplemst  7444  prarloclemarch2  7606  opelreal  8014  elreal  8015  elreal2  8017  eqresr  8023  c0ex  8140  1ex  8141  pnfex  8200  sup3exmid  9104  2ex  9182  3ex  9186  elxr  9972  xnn0nnen  10659  lsw0  11119  setsslid  13083  setsslnid  13084  bassetsnn  13089  prdsex  13302  rmodislmod  14315  fnpsr  14631  lgsdir2lem3  15709  funvtxval0d  15834  funvtxvalg  15837  funiedgvalg  15838  struct2slots2dom  15839  structiedg0val  15841  edgstruct  15864  2omapen  16360  subctctexmid  16366  0nninf  16370  nninffeq  16386