Theorem elexi 2742

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

Syntax hints:   e. wcel 2141   _Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  elpwi2  4142  onunisuci  4415  ordsoexmid  4544  1oex  6400  fnoei  6428  oeiexg  6429  endisj  6798  unfiexmid  6891  snexxph  6923  djuex  7016  0ct  7080  nninfex  7094  infnninfOLD  7097  nnnninf  7098  ctssexmid  7122  pm54.43  7154  pw1ne3  7194  3nsssucpw1  7200  prarloclemarch2  7368  opelreal  7776  elreal  7777  elreal2  7779  eqresr  7785  c0ex  7901  1ex  7902  pnfex  7960  sup3exmid  8860  2ex  8937  3ex  8941  elxr  9720  setsslid  12453  setsslnid  12454  lgsdir2lem3  13684  subctctexmid  13994  0nninf  13997  nninffeq  14013