Theorem elexi 2772

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

Syntax hints:   e. wcel 2164   _Vcvv 2760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elpwi2  4188  onunisuci  4464  ordsoexmid  4595  1oex  6479  fnoei  6507  oeiexg  6508  endisj  6880  unfiexmid  6976  snexxph  7011  djuex  7104  0ct  7168  nninfex  7182  infnninfOLD  7186  nnnninf  7187  ctssexmid  7211  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemg  7236  pm54.43  7252  pw1ne3  7292  3nsssucpw1  7298  2omotaplemst  7320  prarloclemarch2  7481  opelreal  7889  elreal  7890  elreal2  7892  eqresr  7898  c0ex  8015  1ex  8016  pnfex  8075  sup3exmid  8978  2ex  9056  3ex  9060  elxr  9845  xnn0nnen  10511  setsslid  12672  setsslnid  12673  prdsex  12883  rmodislmod  13850  fnpsr  14164  lgsdir2lem3  15187  subctctexmid  15561  0nninf  15564  nninffeq  15580