Theorem elex 2827

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 2230	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2822	. 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 2205   _Vcvv 2815

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 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elexi  2828  elexd  2829  elisset  2830  vtoclgft  2867  vtoclgf  2875  vtoclg1f  2876  vtocl2gf  2879  vtocl3gf  2880  spcimgft  2895  spcimegft  2897  elab4g  2968  elrabf  2973  mob  3001  sbcex  3053  sbcel1v  3107  sbcabel  3127  csbcomg  3163  csbvarg  3168  csbiebt  3180  csbnestgf  3193  csbidmg  3197  sbcco3g  3198  csbco3g  3199  eldif  3222  ssv  3262  elun  3362  elin  3404  elif  3636  elpwb  3681  snidb  3721  eldifvsn  3828  snssg  3830  dfopg  3883  eluni  3919  eliun  3997  csbexga  4240  nvel  4245  class2seteq  4278  axpweq  4286  snelpwi  4329  opexg  4346  elopab  4378  epelg  4413  elon2  4499  unexg  4566  reuhypd  4594  sucexg  4622  onsucb  4627  onsucelsucr  4632  sucunielr  4634  en2lp  4678  peano2  4719  peano2b  4739  opelvvg  4801  opeliunxp  4807  opeliunxp2  4897  ideqg  4908  elrnmptg  5011  imasng  5129  iniseg  5136  opswapg  5251  elxp4  5252  elxp5  5253  dmmptg  5262  iota2  5344  fnmpt  5487  fvexg  5691  fvelimab  5735  mptfvex  5765  fvmptdf  5767  fvmptdv2  5769  mpteqb  5770  fvmptt  5771  fvmptf  5772  fvopab6  5776  fsn2  5853  fmptpr  5878  eloprabga  6142  ovmpos  6179  ov2gf  6180  ovmpodxf  6181  ovmpox  6184  ovmpoga  6185  ovmpodf  6187  ovi3  6193  ovelrn  6205  suppssov1  6265  offval3  6329  1stexg  6363  2ndexg  6364  elxp6  6365  elxp7  6366  releldm2  6381  fnmpo  6400  mpofvex  6403  mpoexg  6409  suppval  6439  opeliunxp2f  6471  brtpos2  6484  rdgtfr  6607  rdgruledefgg  6608  frec0g  6630  sucinc2  6681  nntri3or  6728  relelec  6811  ecdmn0m  6813  mapvalg  6894  pmvalg  6895  elpmg  6900  elixp2  6939  mptelixpg  6971  elixpsn  6972  map1  7056  rex2dom  7065  mapdom1g  7102  mapxpen  7103  fival  7259  elfi2  7261  2omapen  7272  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djulclb  7348  inl11  7358  djuss  7363  1stinl  7367  2ndinl  7368  1stinr  7369  2ndinr  7370  ismkvnex  7448  omniwomnimkv  7460  isacnm  7512  cc4n  7587  elinp  7791  addnqprlemfl  7876  addnqprlemfu  7877  mulnqprlemfl  7892  mulnqprlemfu  7893  recexprlemell  7939  recexprlemelu  7940  hashmap  11196  wrdexg  11239  wrdsymb0  11261  lswwrd  11275  ccatfvalfi  11284  swrdval  11344  swrd00g  11345  pfxval  11370  cats1fvn  11460  cats1fvnd  11461  s2fv1g  11484  s2leng  11485  s2dmg  11486  shftfvalg  11507  clim  11970  climmpt  11989  climshft2  11995  4sqlem2  13091  isstruct2r  13240  slotex  13256  setsvalg  13259  setsfun0  13265  setscom  13269  ressvalsets  13294  ressbasid  13300  restval  13475  topnvalg  13481  tgval  13492  ptex  13494  prdsex  13499  pwsval  13521  pwsbas  13522  pwselbasb  13523  pwssnf1o  13528  imasex  13535  qusex  13555  qusaddvallemg  13563  xpsfrnel2  13576  plusffvalg  13592  grpidvalg  13603  gsum0g  13626  sgrp1  13641  issubmnd  13672  pws0g  13681  issubm  13702  grppropstrg  13749  grpinvfvalg  13772  grpinvfng  13774  grpsubfvalg  13775  grpressid  13791  mulgfvalg  13855  mulgex  13857  mulgfng  13858  issubg  13907  subgex  13910  releqgg  13954  eqgex  13955  eqgfval  13956  isghm  13977  ablressid  14069  mgpvalg  14084  mgptopng  14090  rngressid  14115  rngpropd  14116  ringidvalg  14122  dfur2g  14123  issrg  14126  iscrng2  14176  ringressid  14224  opprvalg  14230  dvdsrex  14260  unitgrp  14278  unitabl  14279  unitlinv  14288  unitrinv  14289  isnzr2  14346  issubrng  14361  issubrg  14383  subrgugrp  14402  aprap  14449  islmod  14456  scaffvalg  14471  lsssetm  14521  islssmg  14523  lspfval  14553  lspval  14555  lspcl  14556  lspex  14560  sraval  14602  rlmvalg  14619  rlmsubg  14623  rlmvnegg  14630  ixpsnbasval  14631  lidlvalg  14636  rspvalg  14637  lidlex  14638  rspex  14639  2idlvalg  14668  zrhvalg  14783  zlmval  14792  mplvalcoe  14862  mplbascoe  14863  mplplusgg  14875  toponsspwpwg  14904  eltg  14934  eltg2  14935  restbasg  15050  tgrest  15051  txvalex  15136  txval  15137  ispsmet  15205  ismet  15226  isxmet  15227  xmetunirn  15240  blfvalps  15267  vtxvalg  16028  iedgvalg  16029  vtxex  16030  edgvalg  16071  vtxdgfval  16300  wksfval  16334  iswlkg  16341  wlkvtxeledgg  16356  trlsfvalg  16395  clwwlkg  16405  clwwlkng  16417  eupthsg  16457  bj-vtoclgft  16564  djucllem  16589  bj-nvel  16684  pw1mapen  16787