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  5823  1oex  6576  fnoei  6606  oeiexg  6607  endisj  6991  unfiexmid  7091  snexxph  7128  djuex  7221  0ct  7285  nninfex  7299  infnninfOLD  7303  nnnninf  7304  ctssexmid  7328  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  pm54.43  7374  pw1ne3  7426  3nsssucpw1  7432  2omotaplemst  7455  prarloclemarch2  7617  opelreal  8025  elreal  8026  elreal2  8028  eqresr  8034  c0ex  8151  1ex  8152  pnfex  8211  sup3exmid  9115  2ex  9193  3ex  9197  elxr  9984  xnn0nnen  10671  lsw0  11132  setsslid  13099  setsslnid  13100  bassetsnn  13105  prdsex  13318  rmodislmod  14331  fnpsr  14647  lgsdir2lem3  15725  funvtxval0d  15850  funvtxvalg  15853  funiedgvalg  15854  struct2slots2dom  15855  structiedg0val  15857  edgstruct  15880  3dom  16439  2omapen  16447  subctctexmid  16453  0nninf  16458  nninffeq  16474