Theorem elex 2833

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   E.wex 1545   e. wcel 2209   _Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  elexi  2834  elexd  2835  elisset  2836  vtoclgft  2873  vtoclgf  2881  vtoclg1f  2882  vtocl2gf  2885  vtocl3gf  2886  spcimgft  2901  spcimegft  2903  elab4g  2975  elrabf  2980  mob  3008  sbcex  3060  sbcel1v  3114  sbcabel  3134  csbcomg  3170  csbvarg  3175  csbiebt  3187  csbnestgf  3200  csbidmg  3204  sbcco3g  3205  csbco3g  3206  eldif  3229  ssv  3270  elun  3370  elin  3412  elif  3652  elpwb  3699  snidb  3739  eldifvsn  3847  snssg  3849  dfopg  3902  eluni  3938  eliun  4016  csbexga  4261  nvel  4266  class2seteq  4300  axpweq  4308  snelpwi  4351  opexg  4368  elopab  4400  epelg  4435  elon2  4521  unexg  4589  reuhypd  4617  sucexg  4645  onsucb  4650  onsucelsucr  4655  sucunielr  4657  en2lp  4701  peano2  4742  peano2b  4762  opelvvg  4824  opeliunxp  4830  opeliunxp2  4920  ideqg  4931  elrnmptg  5034  imasng  5152  iniseg  5159  opswapg  5274  elxp4  5275  elxp5  5276  dmmptg  5285  iota2  5367  fnmpt  5510  fvexg  5714  fvelimab  5759  mptfvex  5791  fvmptdf  5793  fvmptdv2  5795  mpteqb  5796  fvmptt  5797  fvmptf  5798  fvopab6  5805  fsn2  5882  fmptpr  5907  eloprabga  6175  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  ovmpox  6217  ovmpoga  6218  ovmpodf  6220  ovi3  6226  ovelrn  6238  suppssov1  6299  offval3  6367  1stexg  6401  2ndexg  6402  elxp6  6403  elxp7  6404  releldm2  6419  fnmpo  6438  mpofvex  6441  mpoexg  6447  suppval  6477  opeliunxp2f  6509  brtpos2  6522  rdgtfr  6645  rdgruledefgg  6646  frec0g  6668  sucinc2  6719  nntri3or  6766  relelec  6849  ecdmn0m  6851  mapvalg  6932  pmvalg  6933  elpmg  6938  elixp2  6984  mptelixpg  7016  elixpsn  7017  map1  7101  rex2dom  7110  mapdom1g  7147  mapxpen  7148  fival  7304  elfi2  7306  2omapen  7319  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djulclb  7395  inl11  7405  djuss  7410  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  ismkvnex  7495  omniwomnimkv  7507  isacnm  7559  cc4n  7637  elinp  7841  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  recexprlemell  7989  recexprlemelu  7990  indv  9295  hashmap  11268  wrdexg  11315  wrdsymb0  11337  lswwrd  11351  ccatfvalfi  11360  swrdval  11420  swrd00g  11421  pfxval  11446  cats1fvn  11536  cats1fvnd  11537  s2fv1g  11560  s2leng  11561  s2dmg  11562  shftfvalg  11583  clim  12047  climmpt  12066  climshft2  12072  4sqlem2  13168  ballotfilemsv  13253  isstruct2r  13363  slotex  13379  setsvalg  13382  setsfun0  13388  setscom  13392  ressvalsets  13418  ressbasid  13424  restval  13599  topnvalg  13605  tgval  13616  ptex  13618  imasex  13626  qusex  13646  qusaddvallemg  13654  xpsfrnel2  13667  plusffvalg  13682  grpidvalg  13693  gzsum0  13713  sgrp1  13726  issubmnd  13755  issubm  13779  grppropstrg  13824  grpinvfvalg  13847  grpinvfng  13849  grpsubfvalg  13850  grpressid  13866  mulgfvalg  13924  mulgex  13926  mulgfng  13927  issubg  13976  subgex  13979  releqgg  14023  eqgex  14024  eqgfval  14025  isghm  14046  ablressid  14139  prdsex  14172  pwsval  14204  pwsbas  14205  pwselbasb  14206  pwssnf1o  14211  pws0g  14213  mgpvalg  14220  mgptopng  14228  rngressid  14253  rngpropd  14254  ringidvalg  14264  dfur2g  14266  issrg  14269  iscrng2  14319  ringressid  14368  opprvalg  14374  opprringb  14386  dvdsrex  14405  unitgrp  14423  unitabl  14424  unitlinv  14433  unitrinv  14434  isnzr2  14491  issubrng  14507  issubrg  14529  subrgugrp  14548  aprap  14598  aprprop  14601  islmod  14627  scaffvalg  14643  lsssetm  14693  islssmg  14695  lspfval  14725  lspval  14727  lspcl  14728  lspex  14732  sraval  14774  rlmvalg  14791  rlmsubg  14795  rlmvnegg  14802  ixpsnbasval  14803  lidlvalg  14808  rspvalg  14809  lidlex  14810  rspex  14811  2idlvalg  14840  zrhvalg  14953  zlmval  14962  aspval  15015  mplvalcoe  15081  mplbascoe  15082  mplplusgg  15094  toponsspwpwg  15123  eltg  15153  eltg2  15154  restbasg  15269  tgrest  15270  txvalex  15355  txval  15356  ispsmet  15424  ismet  15445  isxmet  15446  xmetunirn  15459  blfvalps  15486  vtxvalg  16257  iedgvalg  16258  vtxex  16259  edgvalg  16300  vtxdgfval  16529  wksfval  16563  iswlkg  16570  wlkvtxeledgg  16585  trlsfvalg  16624  clwwlkg  16634  clwwlkng  16646  eupthsg  16686  bj-vtoclgft  16803  djucllem  16828  bj-nvel  16923  pw1mapen  17026