Theorem elexi 2834

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

Syntax hints:   ∈ wcel 2209  Vcvv 2821

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  elpwi2  4289  onunisuci  4572  ordsoexmid  4704  funopdmsn  5886  1oex  6685  fnoei  6715  oeiexg  6716  endisj  7112  unfiexmid  7215  snexxph  7257  2omapen  7309  djuex  7373  0ct  7437  nninfex  7451  infnninfOLD  7455  nnnninf  7456  ctssexmid  7480  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemg  7505  pm54.43  7526  pw1ne3  7579  3nsssucpw1  7585  2omotaplemst  7614  prarloclemarch2  7776  opelreal  8184  elreal  8185  elreal2  8187  eqresr  8193  c0ex  8310  1ex  8311  pnfex  8369  sup3exmid  9277  2ex  9355  3ex  9359  elxr  10157  xnn0nnen  10852  lsw0  11330  ballotfilem2  13206  ballotfilemsval  13230  ballotfilemrval  13239  ballotfilemth  13259  setsslid  13381  setsslnid  13382  bassetsnn  13387  prdsex  14149  rmodislmod  14660  fnpsr  14974  lgsdir2lem3  16063  funvtxval0d  16188  funvtxvalg  16191  funiedgvalg  16192  struct2slots2dom  16193  structiedg0val  16195  edgstruct  16219  konigsbergvtx  16637  konigsbergiedg  16638  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  konigsberg  16648  3dom  16932  subctctexmid  16944  0nninf  16952  nninffeq  16968