Theorem elexi 2724

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 2723	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2128  Vcvv 2712

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714

This theorem is referenced by:  elpwi2  4121  onunisuci  4394  ordsoexmid  4523  1oex  6373  fnoei  6401  oeiexg  6402  endisj  6771  unfiexmid  6864  snexxph  6896  djuex  6989  0ct  7053  nninfex  7067  infnninfOLD  7070  nnnninf  7071  ctssexmid  7095  pm54.43  7127  pw1ne3  7167  3nsssucpw1  7173  prarloclemarch2  7341  opelreal  7749  elreal  7750  elreal2  7752  eqresr  7758  c0ex  7874  1ex  7875  pnfex  7933  sup3exmid  8833  2ex  8910  3ex  8914  elxr  9689  setsslid  12310  setsslnid  12311  subctctexmid  13644  0nninf  13647  nninffeq  13663