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  4296  onunisuci  4579  ordsoexmid  4711  funopdmsn  5898  1oex  6700  fnoei  6730  oeiexg  6731  endisj  7128  unfiexmid  7231  snexxph  7274  2omapen  7325  djuex  7389  0ct  7453  nninfex  7467  infnninfOLD  7471  nnnninf  7472  ctssexmid  7496  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  pm54.43  7542  pw1ne3  7595  3nsssucpw1  7601  2omotaplemst  7630  prarloclemarch2  7792  opelreal  8200  elreal  8201  elreal2  8203  eqresr  8209  c0ex  8326  1ex  8327  pnfex  8385  sup3exmid  9295  indfval  9308  indconst0  9311  indconst1  9312  2ex  9385  3ex  9389  elxr  10194  xnn0nnen  10894  lsw0  11373  ballotfilem2  13285  ballotfilemsval  13309  ballotfilemrval  13318  ballotfilemth  13338  setsslid  13460  setsslnid  13461  bassetsnn  13466  prdsex  14278  rmodislmod  14796  fnpsr  15161  log2tlbndlog2  16237  ppiublem2  16309  bposlem8  16335  lgsdir2lem3  16371  funvtxval0d  16496  funvtxvalg  16499  funiedgvalg  16500  struct2slots2dom  16501  structiedg0val  16503  edgstruct  16527  konigsbergvtx  16945  konigsbergiedg  16946  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  konigsberg  16956  3dom  17240  subctctexmid  17252  0nninf  17270  nninffeq  17286