Theorem elex 2732

Description: If a class is a member of another class, then 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 1604	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2160	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2727	. 2 |- ( A e. _V <-> E. x x = A )
4	1, 2, 3	3imtr4i 200	1 |- ( A e. B -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1342   E.wex 1479   e. wcel 2135   _Vcvv 2721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723

This theorem is referenced by:  elexi  2733  elexd  2734  elisset  2735  vtoclgft  2771  vtoclgf  2779  vtoclg1f  2780  vtocl2gf  2783  vtocl3gf  2784  spcimgft  2797  spcimegft  2799  elab4g  2870  elrabf  2875  mob  2903  sbcex  2954  sbcel1v  3008  sbcabel  3027  csbcomg  3063  csbvarg  3068  csbiebt  3079  csbnestgf  3092  csbidmg  3096  sbcco3g  3097  csbco3g  3098  eldif  3120  ssv  3159  elun  3258  elin  3300  elpwb  3563  snidb  3600  dfopg  3750  eluni  3786  eliun  3864  csbexga  4104  nvel  4109  class2seteq  4136  axpweq  4144  snelpwi  4184  opexg  4200  elopab  4230  epelg  4262  elon2  4348  unexg  4415  reuhypd  4443  sucexg  4469  sucelon  4474  onsucelsucr  4479  sucunielr  4481  en2lp  4525  peano2  4566  peano2b  4586  opelvvg  4647  opeliunxp  4653  opeliunxp2  4738  ideqg  4749  elrnmptg  4850  imasng  4963  iniseg  4970  opswapg  5084  elxp4  5085  elxp5  5086  dmmptg  5095  iota2  5173  fnmpt  5308  fvexg  5499  fvelimab  5536  mptfvex  5565  fvmptdf  5567  fvmptdv2  5569  mpteqb  5570  fvmptt  5571  fvmptf  5572  fvopab6  5576  fsn2  5653  fmptpr  5671  eloprabga  5920  ovmpos  5956  ov2gf  5957  ovmpodxf  5958  ovmpox  5961  ovmpoga  5962  ovmpodf  5964  ovi3  5969  ovelrn  5981  suppssfv  6040  suppssov1  6041  offval3  6094  1stexg  6127  2ndexg  6128  elxp6  6129  elxp7  6130  releldm2  6145  fnmpo  6162  mpofvex  6163  mpoexg  6171  opeliunxp2f  6197  brtpos2  6210  rdgtfr  6333  rdgruledefgg  6334  frec0g  6356  sucinc2  6405  nntri3or  6452  relelec  6532  ecdmn0m  6534  mapvalg  6615  pmvalg  6616  elpmg  6621  elixp2  6659  mptelixpg  6691  elixpsn  6692  map1  6769  mapdom1g  6804  mapxpen  6805  fival  6926  elfi2  6928  djulclr  7005  djurclr  7006  djulcl  7007  djurcl  7008  djulclb  7011  inl11  7021  djuss  7026  1stinl  7030  2ndinl  7031  1stinr  7032  2ndinr  7033  ismkvnex  7110  omniwomnimkv  7122  cc4n  7203  elinp  7406  addnqprlemfl  7491  addnqprlemfu  7492  mulnqprlemfl  7507  mulnqprlemfu  7508  recexprlemell  7554  recexprlemelu  7555  shftfvalg  10746  clim  11208  climmpt  11227  climshft2  11233  isstruct2r  12342  slotex  12358  setsvalg  12361  setsfun0  12367  setscom  12371  restval  12498  topnvalg  12504  toponsspwpwg  12561  tgval  12590  eltg  12593  eltg2  12594  restbasg  12709  tgrest  12710  txvalex  12795  txval  12796  ispsmet  12864  ismet  12885  isxmet  12886  xmetunirn  12899  blfvalps  12926  bj-vtoclgft  13491  djucllem  13516  bj-nvel  13614