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  9289  indfval  9301  indconst0  9304  indconst1  9305  2ex  9378  3ex  9382  elxr  10188  xnn0nnen  10887  lsw0  11366  ballotfilem2  13277  ballotfilemsval  13301  ballotfilemrval  13310  ballotfilemth  13330  setsslid  13452  setsslnid  13453  bassetsnn  13458  prdsex  14221  rmodislmod  14737  fnpsr  15100  log2tlbndlog2  16139  ppiublem2  16193  lgsdir2lem3  16247  funvtxval0d  16372  funvtxvalg  16375  funiedgvalg  16376  struct2slots2dom  16377  structiedg0val  16379  edgstruct  16403  konigsbergvtx  16821  konigsbergiedg  16822  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  konigsberg  16832  3dom  17116  subctctexmid  17128  0nninf  17145  nninffeq  17161