Theorem elexi 2750

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

Syntax hints:   ∈ wcel 2148  Vcvv 2738

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  elpwi2  4159  onunisuci  4433  ordsoexmid  4562  1oex  6425  fnoei  6453  oeiexg  6454  endisj  6824  unfiexmid  6917  snexxph  6949  djuex  7042  0ct  7106  nninfex  7120  infnninfOLD  7123  nnnninf  7124  ctssexmid  7148  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemg  7173  pm54.43  7189  pw1ne3  7229  3nsssucpw1  7235  2omotaplemst  7257  prarloclemarch2  7418  opelreal  7826  elreal  7827  elreal2  7829  eqresr  7835  c0ex  7951  1ex  7952  pnfex  8011  sup3exmid  8914  2ex  8991  3ex  8995  elxr  9776  setsslid  12513  setsslnid  12514  prdsex  12718  rmodislmod  13441  lgsdir2lem3  14434  subctctexmid  14753  0nninf  14756  nninffeq  14772