Theorem elexi 2733

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

Syntax hints:   e. wcel 2135   _Vcvv 2721

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723

This theorem is referenced by:  elpwi2  4131  onunisuci  4404  ordsoexmid  4533  1oex  6383  fnoei  6411  oeiexg  6412  endisj  6781  unfiexmid  6874  snexxph  6906  djuex  6999  0ct  7063  nninfex  7077  infnninfOLD  7080  nnnninf  7081  ctssexmid  7105  pm54.43  7137  pw1ne3  7177  3nsssucpw1  7183  prarloclemarch2  7351  opelreal  7759  elreal  7760  elreal2  7762  eqresr  7768  c0ex  7884  1ex  7885  pnfex  7943  sup3exmid  8843  2ex  8920  3ex  8924  elxr  9703  setsslid  12381  setsslnid  12382  subctctexmid  13715  0nninf  13718  nninffeq  13734