Theorem elexi 2701

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

Syntax hints:   ∈ wcel 1481  Vcvv 2689

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  onunisuci  4362  ordsoexmid  4485  1oex  6329  fnoei  6356  oeiexg  6357  endisj  6726  unfiexmid  6814  snexxph  6846  djuex  6936  0ct  7000  infnninf  7030  nnnninf  7031  ctssexmid  7032  pm54.43  7063  prarloclemarch2  7251  opelreal  7659  elreal  7660  elreal2  7662  eqresr  7668  c0ex  7784  1ex  7785  pnfex  7843  sup3exmid  8739  2ex  8816  3ex  8820  elxr  9593  setsslid  12048  setsslnid  12049  subctctexmid  13369  0nninf  13372  nninfex  13380  nninffeq  13391