Theorem elexi 2815

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	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
elexi	⊢ 𝐴 ∈ V

Proof of Theorem elexi

Step	Hyp	Ref	Expression
1		elisseti.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		elex 2814	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elpwi2  4248  onunisuci  4529  ordsoexmid  4660  funopdmsn  5834  1oex  6590  fnoei  6620  oeiexg  6621  endisj  7008  unfiexmid  7110  snexxph  7149  djuex  7242  0ct  7306  nninfex  7320  infnninfOLD  7324  nnnninf  7325  ctssexmid  7349  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  pm54.43  7395  pw1ne3  7448  3nsssucpw1  7454  2omotaplemst  7477  prarloclemarch2  7639  opelreal  8047  elreal  8048  elreal2  8050  eqresr  8056  c0ex  8173  1ex  8174  pnfex  8233  sup3exmid  9137  2ex  9215  3ex  9219  elxr  10011  xnn0nnen  10700  lsw0  11165  setsslid  13138  setsslnid  13139  bassetsnn  13144  prdsex  13357  rmodislmod  14371  fnpsr  14687  lgsdir2lem3  15765  funvtxval0d  15890  funvtxvalg  15893  funiedgvalg  15894  struct2slots2dom  15895  structiedg0val  15897  edgstruct  15921  3dom  16613  2omapen  16621  subctctexmid  16627  0nninf  16632  nninffeq  16648