Theorem elex 2560

Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Assertion

Ref	Expression
elex	|- (A e. B -> A e. _V)

Proof of Theorem elex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpl 1505	. 2 |- (E.x(x = A /\ x e. B) -> E.x x = A)
2		df-clel 2033	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
3		isset 2555	. 2 |- (A e. _V <-> E.x x = A)
4	1, 2, 3	3imtr4i 190	1 |- (A e. B -> A e. _V)

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553

This theorem is referenced by:  elexi  2561  elisset  2562  vtoclgft  2598  vtoclgf  2606  vtocl2gf  2609  vtocl3gf  2610  spcimgft  2623  spcimegft  2625  elab4g  2685  elrabf  2690  mob  2717  sbcex  2766  sbcabel  2833  csbcomg  2867  csbvarg  2871  csbiebt  2880  csbnestgf  2892  csbidmg  2896  sbcco3g  2897  csbco3g  2898  eldif  2921  ssv  2959  elun  3078  elin  3120  snidb  3393  dfopg  3538  eluni  3574  eliun  3652  csbexga  3876  nvel  3880  class2seteq  3907  axpweq  3915  snelpwi  3939  prelpwi  3941  opexg  3955  elopab  3986  epelg  4018  elon2  4079  unexg  4144  reuhypd  4169  op1stbg  4176  sucexg  4190  sucelon  4195  onsucelsucr  4199  sucunielr  4201  en2lp  4232  peano2  4261  peano2b  4280  opelvvg  4332  opeliunxp  4338  opbrop  4362  opeliunxp2  4419  ideqg  4430  elrnmptg  4529  imasng  4633  iniseg  4640  opswapg  4750  elxp4  4751  elxp5  4752  dmmptg  4761  iota2  4836  fnmpt  4968  fvexg  5137  fvelimab  5172  mptfvex  5199  fvmptdf  5201  fvmptdv2  5203  mpteqb  5204  fvmptt  5205  fvmptf  5206  fvopab6  5207  fsn2  5280  fmptpr  5298  fliftel  5376  eloprabga  5533  ovmpt2s  5566  ov2gf  5567  ovmpt2dxf  5568  ovmpt2x  5571  ovmpt2ga  5572  ovmpt2df  5574  ovi3  5579  ovelrn  5591  suppssfv  5650  suppssov1  5651  offval3  5703  1stexg  5736  2ndexg  5737  elxp6  5738  elxp7  5739  releldm2  5753  fnmpt2  5770  mpt2fvex  5771  mpt2exg  5776  brtpos2  5807  rdgtfr  5901  rdgruledefgg  5902  frec0g  5922  sucinc2  5965  nntri3or  6011  relelec  6082  ecdmn0m  6084  elinp  6456  addnqprlemfl  6539  addnqprlemfu  6540  recexprlemell  6593  recexprlemelu  6594  bj-vtoclgft  9229  bj-nvel  9328