Theorem elexi 2784

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 2783	. 2 |- ( A e. B -> A e. _V )
3	1, 2	ax-mp 5	1 |- A e. _V

Syntax hints:   e. wcel 2176   _Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  elpwi2  4203  onunisuci  4480  ordsoexmid  4611  funopdmsn  5766  1oex  6512  fnoei  6540  oeiexg  6541  endisj  6921  unfiexmid  7017  snexxph  7054  djuex  7147  0ct  7211  nninfex  7225  infnninfOLD  7229  nnnninf  7230  ctssexmid  7254  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemg  7279  pm54.43  7300  pw1ne3  7344  3nsssucpw1  7350  2omotaplemst  7372  prarloclemarch2  7534  opelreal  7942  elreal  7943  elreal2  7945  eqresr  7951  c0ex  8068  1ex  8069  pnfex  8128  sup3exmid  9032  2ex  9110  3ex  9114  elxr  9900  xnn0nnen  10584  lsw0  11043  setsslid  12916  setsslnid  12917  prdsex  13134  rmodislmod  14146  fnpsr  14462  lgsdir2lem3  15540  funvtxval0d  15663  funvtxvalg  15666  funiedgvalg  15667  struct2slots2dom  15668  structiedg0val  15670  edgstruct  15691  2omapen  15970  subctctexmid  15974  0nninf  15978  nninffeq  15994