Theorem elexi 2698

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

Syntax hints:   ∈ wcel 1480  Vcvv 2686

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  onunisuci  4354  ordsoexmid  4477  1oex  6321  fnoei  6348  oeiexg  6349  endisj  6718  unfiexmid  6806  snexxph  6838  djuex  6928  0ct  6992  infnninf  7022  nnnninf  7023  ctssexmid  7024  pm54.43  7046  prarloclemarch2  7227  opelreal  7635  elreal  7636  elreal2  7638  eqresr  7644  c0ex  7760  1ex  7761  pnfex  7819  sup3exmid  8715  2ex  8792  3ex  8796  elxr  9563  setsslid  12009  setsslnid  12010  subctctexmid  13196  0nninf  13197  nninfex  13205  nninffeq  13216