Theorem elexi 2826

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

Syntax hints:   ∈ wcel 2203  Vcvv 2813

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  elpwi2  4270  onunisuci  4553  ordsoexmid  4684  funopdmsn  5864  1oex  6655  fnoei  6685  oeiexg  6686  endisj  7075  unfiexmid  7178  snexxph  7220  2omapen  7270  djuex  7334  0ct  7398  nninfex  7412  infnninfOLD  7416  nnnninf  7417  ctssexmid  7441  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemg  7466  pm54.43  7487  pw1ne3  7540  3nsssucpw1  7546  2omotaplemst  7572  prarloclemarch2  7734  opelreal  8142  elreal  8143  elreal2  8145  eqresr  8151  c0ex  8268  1ex  8269  pnfex  8327  sup3exmid  9231  2ex  9309  3ex  9313  elxr  10109  xnn0nnen  10799  lsw0  11272  ballotfilem2  13142  setsslid  13263  setsslnid  13264  bassetsnn  13269  prdsex  13482  rmodislmod  14499  fnpsr  14815  lgsdir2lem3  15903  funvtxval0d  16028  funvtxvalg  16031  funiedgvalg  16032  struct2slots2dom  16033  structiedg0val  16035  edgstruct  16059  konigsbergvtx  16477  konigsbergiedg  16478  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  konigsberg  16488  3dom  16762  subctctexmid  16774  0nninf  16782  nninffeq  16798