Theorem elexi 2775

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

Syntax hints:   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elpwi2  4191  onunisuci  4467  ordsoexmid  4598  1oex  6482  fnoei  6510  oeiexg  6511  endisj  6883  unfiexmid  6979  snexxph  7016  djuex  7109  0ct  7173  nninfex  7187  infnninfOLD  7191  nnnninf  7192  ctssexmid  7216  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemg  7241  pm54.43  7257  pw1ne3  7297  3nsssucpw1  7303  2omotaplemst  7325  prarloclemarch2  7486  opelreal  7894  elreal  7895  elreal2  7897  eqresr  7903  c0ex  8020  1ex  8021  pnfex  8080  sup3exmid  8984  2ex  9062  3ex  9066  elxr  9851  xnn0nnen  10529  setsslid  12729  setsslnid  12730  prdsex  12940  rmodislmod  13907  fnpsr  14221  lgsdir2lem3  15271  subctctexmid  15645  0nninf  15648  nninffeq  15664