Theorem elexi 2834

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

This proof depends on syntax axioms:   ∈ wcel 2209  Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elpwi2  4296  onunisuci  4579  ordsoexmid  4711  funopdmsn  5898  1oex  6699  fnoei  6729  oeiexg  6730  endisj  7126  unfiexmid  7229  snexxph  7272  2omapen  7325  djuex  7389  0ct  7453  nninfex  7467  infnninfOLD  7471  nnnninf  7472  ctssexmid  7496  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  pm54.43  7542  pw1ne3  7595  3nsssucpw1  7601  2omotaplemst  7630  prarloclemarch2  7792  opelreal  8200  elreal  8201  elreal2  8203  eqresr  8209  c0ex  8326  1ex  8327  pnfex  8385  sup3exmid  9295  indfval  9308  indconst0  9311  indconst1  9312  2ex  9385  3ex  9389  elxr  10195  xnn0nnen  10895  lsw0  11374  ballotfilem2  13286  ballotfilemsval  13310  ballotfilemrval  13319  ballotfilemth  13339  setsslid  13461  setsslnid  13462  bassetsnn  13467  prdsex  14279  rmodislmod  14797  fnpsr  15160  log2tlbndlog2  16220  ppiublem2  16292  bposlem8  16318  lgsdir2lem3  16354  funvtxval0d  16479  funvtxvalg  16482  funiedgvalg  16483  struct2slots2dom  16484  structiedg0val  16486  edgstruct  16510  konigsbergvtx  16928  konigsbergiedg  16929  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  konigsberg  16939  3dom  17223  subctctexmid  17235  0nninf  17253  nninffeq  17269