Theorem elex 2746

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 1615	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2171	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2741	. 2 |- ( A e. _V <-> E. x x = A )
4	1, 2, 3	3imtr4i 201	1 |- ( A e. B -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   E.wex 1490   e. wcel 2146   _Vcvv 2735

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-v 2737

This theorem is referenced by:  elexi  2747  elexd  2748  elisset  2749  vtoclgft  2785  vtoclgf  2793  vtoclg1f  2794  vtocl2gf  2797  vtocl3gf  2798  spcimgft  2811  spcimegft  2813  elab4g  2884  elrabf  2889  mob  2917  sbcex  2969  sbcel1v  3023  sbcabel  3042  csbcomg  3078  csbvarg  3083  csbiebt  3094  csbnestgf  3107  csbidmg  3111  sbcco3g  3112  csbco3g  3113  eldif  3136  ssv  3175  elun  3274  elin  3316  elpwb  3582  snidb  3619  snssg  3723  dfopg  3772  eluni  3808  eliun  3886  csbexga  4126  nvel  4131  class2seteq  4158  axpweq  4166  snelpwi  4206  opexg  4222  elopab  4252  epelg  4284  elon2  4370  unexg  4437  reuhypd  4465  sucexg  4491  sucelon  4496  onsucelsucr  4501  sucunielr  4503  en2lp  4547  peano2  4588  peano2b  4608  opelvvg  4669  opeliunxp  4675  opeliunxp2  4760  ideqg  4771  elrnmptg  4872  imasng  4986  iniseg  4993  opswapg  5107  elxp4  5108  elxp5  5109  dmmptg  5118  iota2  5198  fnmpt  5334  fvexg  5526  fvelimab  5564  mptfvex  5593  fvmptdf  5595  fvmptdv2  5597  mpteqb  5598  fvmptt  5599  fvmptf  5600  fvopab6  5604  fsn2  5682  fmptpr  5700  eloprabga  5952  ovmpos  5988  ov2gf  5989  ovmpodxf  5990  ovmpox  5993  ovmpoga  5994  ovmpodf  5996  ovi3  6001  ovelrn  6013  suppssfv  6069  suppssov1  6070  offval3  6125  1stexg  6158  2ndexg  6159  elxp6  6160  elxp7  6161  releldm2  6176  fnmpo  6193  mpofvex  6194  mpoexg  6202  opeliunxp2f  6229  brtpos2  6242  rdgtfr  6365  rdgruledefgg  6366  frec0g  6388  sucinc2  6437  nntri3or  6484  relelec  6565  ecdmn0m  6567  mapvalg  6648  pmvalg  6649  elpmg  6654  elixp2  6692  mptelixpg  6724  elixpsn  6725  map1  6802  mapdom1g  6837  mapxpen  6838  fival  6959  elfi2  6961  djulclr  7038  djurclr  7039  djulcl  7040  djurcl  7041  djulclb  7044  inl11  7054  djuss  7059  1stinl  7063  2ndinl  7064  1stinr  7065  2ndinr  7066  ismkvnex  7143  omniwomnimkv  7155  cc4n  7245  elinp  7448  addnqprlemfl  7533  addnqprlemfu  7534  mulnqprlemfl  7549  mulnqprlemfu  7550  recexprlemell  7596  recexprlemelu  7597  shftfvalg  10795  clim  11257  climmpt  11276  climshft2  11282  4sqlem2  12354  isstruct2r  12440  slotex  12456  setsvalg  12459  setsfun0  12465  setscom  12469  ressvalsets  12490  restval  12625  topnvalg  12631  plusffvalg  12656  grpidvalg  12667  sgrp1  12691  issubm  12735  grppropstrg  12766  grpinvfvalg  12786  grpinvfng  12788  grpsubfvalg  12789  mulgfvalg  12855  mulgfng  12857  mgpvalg  12940  mgptopng  12946  ringidvalg  12950  dfur2g  12951  issrg  12954  iscrng2  13004  opprvalg  13045  toponsspwpwg  13100  tgval  13129  eltg  13132  eltg2  13133  restbasg  13248  tgrest  13249  txvalex  13334  txval  13335  ispsmet  13403  ismet  13424  isxmet  13425  xmetunirn  13438  blfvalps  13465  bj-vtoclgft  14096  djucllem  14121  bj-nvel  14218