Theorem elexi 2813

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

Syntax hints:   ∈ wcel 2200  Vcvv 2800

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  elpwi2  4246  onunisuci  4527  ordsoexmid  4658  funopdmsn  5829  1oex  6585  fnoei  6615  oeiexg  6616  endisj  7003  unfiexmid  7103  snexxph  7140  djuex  7233  0ct  7297  nninfex  7311  infnninfOLD  7315  nnnninf  7316  ctssexmid  7340  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemg  7365  pm54.43  7386  pw1ne3  7438  3nsssucpw1  7444  2omotaplemst  7467  prarloclemarch2  7629  opelreal  8037  elreal  8038  elreal2  8040  eqresr  8046  c0ex  8163  1ex  8164  pnfex  8223  sup3exmid  9127  2ex  9205  3ex  9209  elxr  10001  xnn0nnen  10689  lsw0  11151  setsslid  13123  setsslnid  13124  bassetsnn  13129  prdsex  13342  rmodislmod  14355  fnpsr  14671  lgsdir2lem3  15749  funvtxval0d  15874  funvtxvalg  15877  funiedgvalg  15878  struct2slots2dom  15879  structiedg0val  15881  edgstruct  15905  3dom  16523  2omapen  16531  subctctexmid  16537  0nninf  16542  nninffeq  16558