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  6514  brtpos2  6527  rdgtfr  6650  rdgruledefgg  6651  frec0g  6673  sucinc2  6724  nntri3or  6771  relelec  6854  ecdmn0m  6856  mapvalg  6937  pmvalg  6938  elpmg  6943  elixp2  6990  mptelixpg  7022  elixpsn  7023  map1  7107  rex2dom  7116  mapdom1g  7153  mapxpen  7154  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  11289  wrdexg  11336  wrdsymb0  11358  lswwrd  11372  ccatfvalfi  11381  swrdval  11441  swrd00g  11442  pfxval  11467  cats1fvn  11557  cats1fvnd  11558  s2fv1g  11581  s2leng  11582  s2dmg  11583  shftfvalg  11604  clim  12071  climmpt  12090  climshft2  12096  4sqlem2  13196  ballotfilemsv  13310  isstruct2r  13420  slotex  13436  setsvalg  13439  setsfun0  13445  setscom  13449  ressvalsets  13475  ressbasid  13482  restval  13657  topnvalg  13663  tgval  13674  ptex  13676  imasex  13684  qusex  13704  qusaddvallemg  13712  xpsfrnel2  13725  plusffvalg  13740  grpidvalg  13751  gzsum0  13771  sgrp1  13784  issubmnd  13813  issubm  13837  grppropstrg  13882  grpinvfvalg  13905  grpinvfng  13907  grpsubfvalg  13908  grpressid  13924  mulgfvalg  13982  mulgex  13984  mulgfng  13985  issubg  14034  subgex  14037  releqgg  14081  eqgex  14082  eqgfval  14083  isghm  14104  cntzex  14149  cntzfval  14151  ablressid  14228  prdsex  14278  pwsval  14310  pwsbas  14311  pwselbasb  14312  pwssnf1o  14317  pws0g  14319  mgpvalg  14326  mgptopng  14334  rngressid  14359  rngpropd  14360  ringidvalg  14370  dfur2g  14372  issrg  14375  iscrng2  14425  ringressid  14476  opprvalg  14482  opprringb  14494  dvdsrex  14513  unitgrp  14531  unitabl  14532  unitlinv  14541  unitrinv  14542  isnzr2  14599  issubrng  14615  issubrg  14637  subrgugrp  14656  aprap  14706  aprprop  14709  islmod  14735  scaffvalg  14751  lsssetm  14801  islssmg  14803  lspfval  14833  lspval  14835  lspcl  14836  lspex  14840  sraval  14882  rlmvalg  14899  rlmsubg  14903  rlmvnegg  14910  ixpsnbasval  14911  lidlvalg  14916  rspvalg  14917  lidlex  14918  rspex  14919  2idlvalg  14948  zrhvalg  15061  zlmval  15070  aspval  15123  mplvalg  15222  mplplusgg  15236  toponsspwpwg  15265  eltg  15295  eltg2  15296  restbasg  15411  tgrest  15412  txvalex  15497  txval  15498  ispsmet  15566  ismet  15587  isxmet  15588  xmetunirn  15601  blfvalps  15628  vtxvalg  16479  iedgvalg  16480  vtxex  16481  edgvalg  16522  vtxdgfval  16751  wksfval  16785  iswlkg  16792  wlkvtxeledgg  16807  trlsfvalg  16846  clwwlkg  16856  clwwlkng  16868  eupthsg  16908  bj-vtoclgft  17025  djucllem  17050  bj-nvel  17145  pw1mapen  17248