Theorem elexi 2742

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

Syntax hints:   ∈ wcel 2141  Vcvv 2730

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  elpwi2  4144  onunisuci  4417  ordsoexmid  4546  1oex  6403  fnoei  6431  oeiexg  6432  endisj  6802  unfiexmid  6895  snexxph  6927  djuex  7020  0ct  7084  nninfex  7098  infnninfOLD  7101  nnnninf  7102  ctssexmid  7126  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemg  7151  pm54.43  7167  pw1ne3  7207  3nsssucpw1  7213  prarloclemarch2  7381  opelreal  7789  elreal  7790  elreal2  7792  eqresr  7798  c0ex  7914  1ex  7915  pnfex  7973  sup3exmid  8873  2ex  8950  3ex  8954  elxr  9733  setsslid  12466  setsslnid  12467  lgsdir2lem3  13725  subctctexmid  14034  0nninf  14037  nninffeq  14053