Theorem elexi 2612

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

Syntax hints:   ∈ wcel 1434  Vcvv 2602

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604

This theorem is referenced by:  onunisuci  4189  ordsoexmid  4307  fnoei  6090  oeiexg  6091  1domsn  6353  endisj  6358  unfiexmid  6428  pm54.43  6508  indpi  6583  prarloclemarch2  6660  prarloclemlt  6734  opelreal  7047  elreal  7048  elreal2  7050  eqresr  7055  c0ex  7164  1ex  7165  pnfex  7223  2ex  8167  3ex  8171  elxr  8917