Theorem elexi 2834

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

This proof depends on syntax axioms:   e. wcel 2209   _Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elpwi2  4294  onunisuci  4577  ordsoexmid  4709  funopdmsn  5895  1oex  6695  fnoei  6725  oeiexg  6726  endisj  7122  unfiexmid  7225  snexxph  7267  2omapen  7319  djuex  7383  0ct  7447  nninfex  7461  infnninfOLD  7465  nnnninf  7466  ctssexmid  7490  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  pm54.43  7536  pw1ne3  7589  3nsssucpw1  7595  2omotaplemst  7624  prarloclemarch2  7786  opelreal  8194  elreal  8195  elreal2  8197  eqresr  8203  c0ex  8320  1ex  8321  pnfex  8379  sup3exmid  9287  indfval  9299  indconst0  9302  indconst1  9303  2ex  9376  3ex  9380  elxr  10178  xnn0nnen  10874  lsw0  11352  ballotfilem2  13228  ballotfilemsval  13252  ballotfilemrval  13261  ballotfilemth  13281  setsslid  13403  setsslnid  13404  bassetsnn  13409  prdsex  14172  rmodislmod  14688  fnpsr  15051  log2tlbndlog2  16082  lgsdir2lem3  16149  funvtxval0d  16274  funvtxvalg  16277  funiedgvalg  16278  struct2slots2dom  16279  structiedg0val  16281  edgstruct  16305  konigsbergvtx  16723  konigsbergiedg  16724  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  konigsberg  16734  3dom  17018  subctctexmid  17030  0nninf  17047  nninffeq  17063