Theorem elex 2824

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 1666	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2228	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2819	. 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 1398   E.wex 1541   e. wcel 2203   _Vcvv 2812

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2814

This theorem is referenced by:  elexi  2825  elexd  2826  elisset  2827  vtoclgft  2864  vtoclgf  2872  vtoclg1f  2873  vtocl2gf  2876  vtocl3gf  2877  spcimgft  2892  spcimegft  2894  elab4g  2965  elrabf  2970  mob  2998  sbcex  3050  sbcel1v  3104  sbcabel  3124  csbcomg  3160  csbvarg  3165  csbiebt  3177  csbnestgf  3190  csbidmg  3194  sbcco3g  3195  csbco3g  3196  eldif  3219  ssv  3259  elun  3359  elin  3401  elif  3633  elpwb  3678  snidb  3718  eldifvsn  3825  snssg  3827  dfopg  3880  eluni  3916  eliun  3994  csbexga  4237  nvel  4242  class2seteq  4275  axpweq  4283  snelpwi  4326  opexg  4343  elopab  4375  epelg  4410  elon2  4496  unexg  4563  reuhypd  4591  sucexg  4619  onsucb  4624  onsucelsucr  4629  sucunielr  4631  en2lp  4675  peano2  4716  peano2b  4736  opelvvg  4798  opeliunxp  4804  opeliunxp2  4894  ideqg  4905  elrnmptg  5008  imasng  5126  iniseg  5133  opswapg  5248  elxp4  5249  elxp5  5250  dmmptg  5259  iota2  5341  fnmpt  5484  fvexg  5688  fvelimab  5732  mptfvex  5762  fvmptdf  5764  fvmptdv2  5766  mpteqb  5767  fvmptt  5768  fvmptf  5769  fvopab6  5773  fsn2  5850  fmptpr  5875  eloprabga  6139  ovmpos  6176  ov2gf  6177  ovmpodxf  6178  ovmpox  6181  ovmpoga  6182  ovmpodf  6184  ovi3  6190  ovelrn  6202  suppssov1  6262  offval3  6326  1stexg  6360  2ndexg  6361  elxp6  6362  elxp7  6363  releldm2  6378  fnmpo  6397  mpofvex  6400  mpoexg  6406  suppval  6436  opeliunxp2f  6468  brtpos2  6481  rdgtfr  6604  rdgruledefgg  6605  frec0g  6627  sucinc2  6678  nntri3or  6725  relelec  6808  ecdmn0m  6810  mapvalg  6891  pmvalg  6892  elpmg  6897  elixp2  6936  mptelixpg  6968  elixpsn  6969  map1  7053  rex2dom  7062  mapdom1g  7099  mapxpen  7100  fival  7256  elfi2  7258  2omapen  7269  djulclr  7339  djurclr  7340  djulcl  7341  djurcl  7342  djulclb  7345  inl11  7355  djuss  7360  1stinl  7364  2ndinl  7365  1stinr  7366  2ndinr  7367  ismkvnex  7445  omniwomnimkv  7457  isacnm  7509  cc4n  7584  elinp  7788  addnqprlemfl  7873  addnqprlemfu  7874  mulnqprlemfl  7889  mulnqprlemfu  7890  recexprlemell  7936  recexprlemelu  7937  wrdexg  11231  wrdsymb0  11253  lswwrd  11267  ccatfvalfi  11276  swrdval  11336  swrd00g  11337  pfxval  11362  cats1fvn  11452  cats1fvnd  11453  s2fv1g  11476  s2leng  11477  s2dmg  11478  shftfvalg  11499  clim  11962  climmpt  11981  climshft2  11987  4sqlem2  13083  isstruct2r  13215  slotex  13231  setsvalg  13234  setsfun0  13240  setscom  13244  ressvalsets  13269  ressbasid  13275  restval  13450  topnvalg  13456  tgval  13467  ptex  13469  prdsex  13474  pwsval  13496  pwsbas  13497  pwselbasb  13498  pwssnf1o  13503  imasex  13510  qusex  13530  qusaddvallemg  13538  xpsfrnel2  13551  plusffvalg  13567  grpidvalg  13578  gsum0g  13601  sgrp1  13616  issubmnd  13647  pws0g  13656  issubm  13677  grppropstrg  13724  grpinvfvalg  13747  grpinvfng  13749  grpsubfvalg  13750  grpressid  13766  mulgfvalg  13830  mulgex  13832  mulgfng  13833  issubg  13882  subgex  13885  releqgg  13929  eqgex  13930  eqgfval  13931  isghm  13952  ablressid  14044  mgpvalg  14059  mgptopng  14065  rngressid  14090  rngpropd  14091  ringidvalg  14097  dfur2g  14098  issrg  14101  iscrng2  14151  ringressid  14199  opprvalg  14205  dvdsrex  14235  unitgrp  14253  unitabl  14254  unitlinv  14263  unitrinv  14264  isnzr2  14321  issubrng  14336  issubrg  14358  subrgugrp  14377  aprap  14424  islmod  14431  scaffvalg  14446  lsssetm  14496  islssmg  14498  lspfval  14528  lspval  14530  lspcl  14531  lspex  14535  sraval  14577  rlmvalg  14594  rlmsubg  14598  rlmvnegg  14605  ixpsnbasval  14606  lidlvalg  14611  rspvalg  14612  lidlex  14613  rspex  14614  2idlvalg  14643  zrhvalg  14758  zlmval  14767  mplvalcoe  14837  mplbascoe  14838  mplplusgg  14850  toponsspwpwg  14879  eltg  14909  eltg2  14910  restbasg  15025  tgrest  15026  txvalex  15111  txval  15112  ispsmet  15180  ismet  15201  isxmet  15202  xmetunirn  15215  blfvalps  15242  vtxvalg  16003  iedgvalg  16004  vtxex  16005  edgvalg  16046  vtxdgfval  16275  wksfval  16309  iswlkg  16316  wlkvtxeledgg  16331  trlsfvalg  16370  clwwlkg  16380  clwwlkng  16392  eupthsg  16432  bj-vtoclgft  16539  djucllem  16564  bj-nvel  16659  pw1mapen  16762