Theorem elexi 2816

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

Syntax hints:   e. wcel 2202   _Vcvv 2803

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  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 2805

This theorem is referenced by:  elpwi2  4253  onunisuci  4535  ordsoexmid  4666  funopdmsn  5842  1oex  6633  fnoei  6663  oeiexg  6664  endisj  7051  unfiexmid  7153  snexxph  7192  djuex  7302  0ct  7366  nninfex  7380  infnninfOLD  7384  nnnninf  7385  ctssexmid  7409  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemg  7434  pm54.43  7455  pw1ne3  7508  3nsssucpw1  7514  2omotaplemst  7537  prarloclemarch2  7699  opelreal  8107  elreal  8108  elreal2  8110  eqresr  8116  c0ex  8233  1ex  8234  pnfex  8292  sup3exmid  9196  2ex  9274  3ex  9278  elxr  10072  xnn0nnen  10762  lsw0  11227  setsslid  13213  setsslnid  13214  bassetsnn  13219  prdsex  13432  rmodislmod  14447  fnpsr  14763  lgsdir2lem3  15849  funvtxval0d  15974  funvtxvalg  15977  funiedgvalg  15978  struct2slots2dom  15979  structiedg0val  15981  edgstruct  16005  konigsbergvtx  16423  konigsbergiedg  16424  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  konigsberglem5  16433  konigsberg  16434  3dom  16708  2omapen  16716  subctctexmid  16722  0nninf  16730  nninffeq  16746