Theorem elex 2668

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 1579	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2111	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2663	. 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 1314   E.wex 1451   e. wcel 1463   _Vcvv 2657

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2659

This theorem is referenced by:  elexi  2669  elexd  2670  elisset  2671  vtoclgft  2707  vtoclgf  2715  vtoclg1f  2716  vtocl2gf  2719  vtocl3gf  2720  spcimgft  2733  spcimegft  2735  elab4g  2802  elrabf  2807  mob  2835  sbcex  2886  sbcel1v  2939  sbcabel  2958  csbcomg  2992  csbvarg  2996  csbiebt  3005  csbnestgf  3018  csbidmg  3022  sbcco3g  3023  csbco3g  3024  eldif  3046  ssv  3085  elun  3183  elin  3225  elpwb  3486  snidb  3521  dfopg  3669  eluni  3705  eliun  3783  csbexga  4016  nvel  4021  class2seteq  4047  axpweq  4055  snelpwi  4094  opexg  4110  elopab  4140  epelg  4172  elon2  4258  unexg  4324  reuhypd  4352  sucexg  4374  sucelon  4379  onsucelsucr  4384  sucunielr  4386  en2lp  4429  peano2  4469  peano2b  4488  opelvvg  4548  opeliunxp  4554  opeliunxp2  4639  ideqg  4650  elrnmptg  4751  imasng  4862  iniseg  4869  opswapg  4983  elxp4  4984  elxp5  4985  dmmptg  4994  iota2  5072  fnmpt  5207  fvexg  5394  fvelimab  5431  mptfvex  5460  fvmptdf  5462  fvmptdv2  5464  mpteqb  5465  fvmptt  5466  fvmptf  5467  fvopab6  5471  fsn2  5548  fmptpr  5566  eloprabga  5812  ovmpos  5848  ov2gf  5849  ovmpodxf  5850  ovmpox  5853  ovmpoga  5854  ovmpodf  5856  ovi3  5861  ovelrn  5873  suppssfv  5932  suppssov1  5933  offval3  5986  1stexg  6019  2ndexg  6020  elxp6  6021  elxp7  6022  releldm2  6037  fnmpo  6054  mpofvex  6055  mpoexg  6063  opeliunxp2f  6089  brtpos2  6102  rdgtfr  6225  rdgruledefgg  6226  frec0g  6248  sucinc2  6296  nntri3or  6343  relelec  6423  ecdmn0m  6425  mapvalg  6506  pmvalg  6507  elpmg  6512  elixp2  6550  mptelixpg  6582  elixpsn  6583  map1  6660  mapdom1g  6694  mapxpen  6695  fival  6810  elfi2  6812  djulclr  6886  djurclr  6887  djulcl  6888  djurcl  6889  djulclb  6892  inl11  6902  djuss  6907  1stinl  6911  2ndinl  6912  1stinr  6913  2ndinr  6914  ismkvnex  6979  elinp  7230  addnqprlemfl  7315  addnqprlemfu  7316  mulnqprlemfl  7331  mulnqprlemfu  7332  recexprlemell  7378  recexprlemelu  7379  shftfvalg  10483  clim  10942  climmpt  10961  climshft2  10967  isstruct2r  11813  slotex  11829  setsvalg  11832  setsfun0  11838  setscom  11842  restval  11969  topnvalg  11975  toponsspwpwg  12032  tgval  12061  eltg  12064  eltg2  12065  restbasg  12180  tgrest  12181  txvalex  12265  txval  12266  ispsmet  12312  ismet  12333  isxmet  12334  xmetunirn  12347  blfvalps  12374  bj-vtoclgft  12674  djucllem  12699  bj-nvel  12787