Theorem elex 2692

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 1596	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2133	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2687	. 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 1331   E.wex 1468   e. wcel 1480   _Vcvv 2681

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-v 2683

This theorem is referenced by:  elexi  2693  elexd  2694  elisset  2695  vtoclgft  2731  vtoclgf  2739  vtoclg1f  2740  vtocl2gf  2743  vtocl3gf  2744  spcimgft  2757  spcimegft  2759  elab4g  2828  elrabf  2833  mob  2861  sbcex  2912  sbcel1v  2966  sbcabel  2985  csbcomg  3020  csbvarg  3025  csbiebt  3034  csbnestgf  3047  csbidmg  3051  sbcco3g  3052  csbco3g  3053  eldif  3075  ssv  3114  elun  3212  elin  3254  elpwb  3515  snidb  3550  dfopg  3698  eluni  3734  eliun  3812  csbexga  4051  nvel  4056  class2seteq  4082  axpweq  4090  snelpwi  4129  opexg  4145  elopab  4175  epelg  4207  elon2  4293  unexg  4359  reuhypd  4387  sucexg  4409  sucelon  4414  onsucelsucr  4419  sucunielr  4421  en2lp  4464  peano2  4504  peano2b  4523  opelvvg  4583  opeliunxp  4589  opeliunxp2  4674  ideqg  4685  elrnmptg  4786  imasng  4899  iniseg  4906  opswapg  5020  elxp4  5021  elxp5  5022  dmmptg  5031  iota2  5109  fnmpt  5244  fvexg  5433  fvelimab  5470  mptfvex  5499  fvmptdf  5501  fvmptdv2  5503  mpteqb  5504  fvmptt  5505  fvmptf  5506  fvopab6  5510  fsn2  5587  fmptpr  5605  eloprabga  5851  ovmpos  5887  ov2gf  5888  ovmpodxf  5889  ovmpox  5892  ovmpoga  5893  ovmpodf  5895  ovi3  5900  ovelrn  5912  suppssfv  5971  suppssov1  5972  offval3  6025  1stexg  6058  2ndexg  6059  elxp6  6060  elxp7  6061  releldm2  6076  fnmpo  6093  mpofvex  6094  mpoexg  6102  opeliunxp2f  6128  brtpos2  6141  rdgtfr  6264  rdgruledefgg  6265  frec0g  6287  sucinc2  6335  nntri3or  6382  relelec  6462  ecdmn0m  6464  mapvalg  6545  pmvalg  6546  elpmg  6551  elixp2  6589  mptelixpg  6621  elixpsn  6622  map1  6699  mapdom1g  6734  mapxpen  6735  fival  6851  elfi2  6853  djulclr  6927  djurclr  6928  djulcl  6929  djurcl  6930  djulclb  6933  inl11  6943  djuss  6948  1stinl  6952  2ndinl  6953  1stinr  6954  2ndinr  6955  ismkvnex  7022  elinp  7275  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemfl  7376  mulnqprlemfu  7377  recexprlemell  7423  recexprlemelu  7424  shftfvalg  10583  clim  11043  climmpt  11062  climshft2  11068  isstruct2r  11959  slotex  11975  setsvalg  11978  setsfun0  11984  setscom  11988  restval  12115  topnvalg  12121  toponsspwpwg  12178  tgval  12207  eltg  12210  eltg2  12211  restbasg  12326  tgrest  12327  txvalex  12412  txval  12413  ispsmet  12481  ismet  12502  isxmet  12503  xmetunirn  12516  blfvalps  12543  bj-vtoclgft  12971  djucllem  12996  bj-nvel  13084