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  4263  nvel  4268  class2seteq  4302  axpweq  4310  snelpwi  4353  opexg  4370  elopab  4402  epelg  4437  elon2  4523  unexg  4591  reuhypd  4619  sucexg  4647  onsucb  4652  onsucelsucr  4657  sucunielr  4659  en2lp  4703  peano2  4744  peano2b  4764  opelvvg  4826  opeliunxp  4832  opeliunxp2  4922  ideqg  4933  elrnmptg  5036  imasng  5155  iniseg  5162  opswapg  5277  elxp4  5278  elxp5  5279  dmmptg  5288  iota2  5370  fnmpt  5513  fvexg  5717  fvelimab  5762  mptfvex  5794  fvmptdf  5796  fvmptdv2  5798  mpteqb  5799  fvmptt  5800  fvmptf  5801  fvopab6  5808  fsn2  5885  fmptpr  5910  eloprabga  6178  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  ovmpox  6220  ovmpoga  6221  ovmpodf  6223  ovi3  6229  ovelrn  6241  suppssov1  6302  ofovex  6311  offval3  6371  1stexg  6405  2ndexg  6406  elxp6  6407  elxp7  6408  releldm2  6423  fnmpo  6442  mpofvex  6445  mpoexg  6451  suppval  6481  opeliunxp2f  6513  brtpos2  6526  rdgtfr  6649  rdgruledefgg  6650  frec0g  6672  sucinc2  6723  nntri3or  6770  relelec  6853  ecdmn0m  6855  mapvalg  6936  pmvalg  6937  elpmg  6942  elixp2  6988  mptelixpg  7020  elixpsn  7021  map1  7105  rex2dom  7114  mapdom1g  7151  mapxpen  7152  fival  7309  elfi2  7311  2omapen  7325  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djulclb  7401  inl11  7411  djuss  7416  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  ismkvnex  7501  omniwomnimkv  7513  isacnm  7565  cc4n  7643  elinp  7847  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  recexprlemell  7995  recexprlemelu  7996  indv  9304  hashmap  11290  wrdexg  11337  wrdsymb0  11359  lswwrd  11373  ccatfvalfi  11382  swrdval  11442  swrd00g  11443  pfxval  11468  cats1fvn  11558  cats1fvnd  11559  s2fv1g  11582  s2leng  11583  s2dmg  11584  shftfvalg  11605  clim  12072  climmpt  12091  climshft2  12097  4sqlem2  13197  ballotfilemsv  13311  isstruct2r  13421  slotex  13437  setsvalg  13440  setsfun0  13446  setscom  13450  ressvalsets  13476  ressbasid  13483  restval  13658  topnvalg  13664  tgval  13675  ptex  13677  imasex  13685  qusex  13705  qusaddvallemg  13713  xpsfrnel2  13726  plusffvalg  13741  grpidvalg  13752  gzsum0  13772  sgrp1  13785  issubmnd  13814  issubm  13838  grppropstrg  13883  grpinvfvalg  13906  grpinvfng  13908  grpsubfvalg  13909  grpressid  13925  mulgfvalg  13983  mulgex  13985  mulgfng  13986  issubg  14035  subgex  14038  releqgg  14082  eqgex  14083  eqgfval  14084  isghm  14105  cntzex  14150  cntzfval  14152  ablressid  14229  prdsex  14279  pwsval  14311  pwsbas  14312  pwselbasb  14313  pwssnf1o  14318  pws0g  14320  mgpvalg  14327  mgptopng  14335  rngressid  14360  rngpropd  14361  ringidvalg  14371  dfur2g  14373  issrg  14376  iscrng2  14426  ringressid  14477  opprvalg  14483  opprringb  14495  dvdsrex  14514  unitgrp  14532  unitabl  14533  unitlinv  14542  unitrinv  14543  isnzr2  14600  issubrng  14616  issubrg  14638  subrgugrp  14657  aprap  14707  aprprop  14710  islmod  14736  scaffvalg  14752  lsssetm  14802  islssmg  14804  lspfval  14834  lspval  14836  lspcl  14837  lspex  14841  sraval  14883  rlmvalg  14900  rlmsubg  14904  rlmvnegg  14911  ixpsnbasval  14912  lidlvalg  14917  rspvalg  14918  lidlex  14919  rspex  14920  2idlvalg  14949  zrhvalg  15062  zlmval  15071  aspval  15124  mplvalcoe  15206  mplbascoe  15207  mplplusgg  15219  toponsspwpwg  15248  eltg  15278  eltg2  15279  restbasg  15394  tgrest  15395  txvalex  15480  txval  15481  ispsmet  15549  ismet  15570  isxmet  15571  xmetunirn  15584  blfvalps  15611  vtxvalg  16462  iedgvalg  16463  vtxex  16464  edgvalg  16505  vtxdgfval  16734  wksfval  16768  iswlkg  16775  wlkvtxeledgg  16790  trlsfvalg  16829  clwwlkg  16839  clwwlkng  16851  eupthsg  16891  bj-vtoclgft  17008  djucllem  17033  bj-nvel  17128  pw1mapen  17231