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

Syntax hints:   e. 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  5834  1oex  6590  fnoei  6620  oeiexg  6621  endisj  7008  unfiexmid  7110  snexxph  7149  djuex  7242  0ct  7306  nninfex  7320  infnninfOLD  7324  nnnninf  7325  ctssexmid  7349  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  pm54.43  7395  pw1ne3  7448  3nsssucpw1  7454  2omotaplemst  7477  prarloclemarch2  7639  opelreal  8047  elreal  8048  elreal2  8050  eqresr  8056  c0ex  8173  1ex  8174  pnfex  8233  sup3exmid  9137  2ex  9215  3ex  9219  elxr  10011  xnn0nnen  10700  lsw0  11165  setsslid  13151  setsslnid  13152  bassetsnn  13157  prdsex  13370  rmodislmod  14384  fnpsr  14700  lgsdir2lem3  15778  funvtxval0d  15903  funvtxvalg  15906  funiedgvalg  15907  struct2slots2dom  15908  structiedg0val  15910  edgstruct  15934  konigsbergvtx  16352  konigsbergiedg  16353  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  konigsberg  16363  3dom  16638  2omapen  16646  subctctexmid  16652  0nninf  16657  nninffeq  16673