Theorem elexi 2738

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

Syntax hints:   ∈ wcel 2136  Vcvv 2726

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  elpwi2  4137  onunisuci  4410  ordsoexmid  4539  1oex  6392  fnoei  6420  oeiexg  6421  endisj  6790  unfiexmid  6883  snexxph  6915  djuex  7008  0ct  7072  nninfex  7086  infnninfOLD  7089  nnnninf  7090  ctssexmid  7114  pm54.43  7146  pw1ne3  7186  3nsssucpw1  7192  prarloclemarch2  7360  opelreal  7768  elreal  7769  elreal2  7771  eqresr  7777  c0ex  7893  1ex  7894  pnfex  7952  sup3exmid  8852  2ex  8929  3ex  8933  elxr  9712  setsslid  12444  setsslnid  12445  lgsdir2lem3  13571  subctctexmid  13881  0nninf  13884  nninffeq  13900