Theorem elexi 2784

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

Syntax hints:   ∈ wcel 2176  Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  elpwi2  4202  onunisuci  4479  ordsoexmid  4610  funopdmsn  5764  1oex  6510  fnoei  6538  oeiexg  6539  endisj  6919  unfiexmid  7015  snexxph  7052  djuex  7145  0ct  7209  nninfex  7223  infnninfOLD  7227  nnnninf  7228  ctssexmid  7252  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemg  7277  pm54.43  7298  pw1ne3  7342  3nsssucpw1  7348  2omotaplemst  7370  prarloclemarch2  7532  opelreal  7940  elreal  7941  elreal2  7943  eqresr  7949  c0ex  8066  1ex  8067  pnfex  8126  sup3exmid  9030  2ex  9108  3ex  9112  elxr  9898  xnn0nnen  10582  lsw0  11041  setsslid  12883  setsslnid  12884  prdsex  13101  rmodislmod  14113  fnpsr  14429  lgsdir2lem3  15507  funvtxval0d  15630  funvtxvalg  15633  funiedgvalg  15634  struct2slots2dom  15635  structiedg0val  15637  edgstruct  15656  2omapen  15933  subctctexmid  15937  0nninf  15941  nninffeq  15957