Theorem elex 2811

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 1663	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2225	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2806	. 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 1395   E.wex 1538   e. wcel 2200   _Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elexi  2812  elexd  2813  elisset  2814  vtoclgft  2851  vtoclgf  2859  vtoclg1f  2860  vtocl2gf  2863  vtocl3gf  2864  spcimgft  2879  spcimegft  2881  elab4g  2952  elrabf  2957  mob  2985  sbcex  3037  sbcel1v  3091  sbcabel  3111  csbcomg  3147  csbvarg  3152  csbiebt  3164  csbnestgf  3177  csbidmg  3181  sbcco3g  3182  csbco3g  3183  eldif  3206  ssv  3246  elun  3345  elin  3387  elif  3614  elpwb  3659  snidb  3696  snssg  3802  dfopg  3855  eluni  3891  eliun  3969  csbexga  4212  nvel  4217  class2seteq  4247  axpweq  4255  snelpwi  4297  opexg  4314  elopab  4346  epelg  4381  elon2  4467  unexg  4534  reuhypd  4562  sucexg  4590  onsucb  4595  onsucelsucr  4600  sucunielr  4602  en2lp  4646  peano2  4687  peano2b  4707  opelvvg  4768  opeliunxp  4774  opeliunxp2  4862  ideqg  4873  elrnmptg  4976  imasng  5093  iniseg  5100  opswapg  5215  elxp4  5216  elxp5  5217  dmmptg  5226  iota2  5308  fnmpt  5450  fvexg  5648  fvelimab  5692  mptfvex  5722  fvmptdf  5724  fvmptdv2  5726  mpteqb  5727  fvmptt  5728  fvmptf  5729  fvopab6  5733  fsn2  5811  fmptpr  5835  eloprabga  6097  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  ovmpox  6139  ovmpoga  6140  ovmpodf  6142  ovi3  6148  ovelrn  6160  suppssfv  6220  suppssov1  6221  offval3  6285  1stexg  6319  2ndexg  6320  elxp6  6321  elxp7  6322  releldm2  6337  fnmpo  6354  mpofvex  6357  mpoexg  6363  opeliunxp2f  6390  brtpos2  6403  rdgtfr  6526  rdgruledefgg  6527  frec0g  6549  sucinc2  6600  nntri3or  6647  relelec  6730  ecdmn0m  6732  mapvalg  6813  pmvalg  6814  elpmg  6819  elixp2  6857  mptelixpg  6889  elixpsn  6890  map1  6973  rex2dom  6979  mapdom1g  7016  mapxpen  7017  fival  7148  elfi2  7150  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djulclb  7233  inl11  7243  djuss  7248  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  ismkvnex  7333  omniwomnimkv  7345  isacnm  7396  cc4n  7468  elinp  7672  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  recexprlemell  7820  recexprlemelu  7821  wrdexg  11095  wrdsymb0  11117  lswwrd  11131  ccatfvalfi  11140  swrdval  11196  swrd00g  11197  pfxval  11222  cats1fvn  11312  cats1fvnd  11313  s2fv1g  11336  s2leng  11337  s2dmg  11338  shftfvalg  11345  clim  11808  climmpt  11827  climshft2  11833  4sqlem2  12928  isstruct2r  13059  slotex  13075  setsvalg  13078  setsfun0  13084  setscom  13088  ressvalsets  13113  ressbasid  13119  restval  13294  topnvalg  13300  tgval  13311  ptex  13313  prdsex  13318  pwsval  13340  pwsbas  13341  pwselbasb  13342  pwssnf1o  13347  imasex  13354  qusex  13374  qusaddvallemg  13382  xpsfrnel2  13395  plusffvalg  13411  grpidvalg  13422  gsum0g  13445  sgrp1  13460  issubmnd  13491  pws0g  13500  issubm  13521  grppropstrg  13568  grpinvfvalg  13591  grpinvfng  13593  grpsubfvalg  13594  grpressid  13610  mulgfvalg  13674  mulgex  13676  mulgfng  13677  issubg  13726  subgex  13729  releqgg  13773  eqgex  13774  eqgfval  13775  isghm  13796  ablressid  13888  mgpvalg  13902  mgptopng  13908  rngressid  13933  rngpropd  13934  ringidvalg  13940  dfur2g  13941  issrg  13944  iscrng2  13994  ringressid  14042  opprvalg  14048  dvdsrex  14078  unitgrp  14096  unitabl  14097  unitlinv  14106  unitrinv  14107  isnzr2  14164  issubrng  14179  issubrg  14201  subrgugrp  14220  aprap  14266  islmod  14271  scaffvalg  14286  lsssetm  14336  islssmg  14338  lspfval  14368  lspval  14370  lspcl  14371  lspex  14375  sraval  14417  rlmvalg  14434  rlmsubg  14438  rlmvnegg  14445  ixpsnbasval  14446  lidlvalg  14451  rspvalg  14452  lidlex  14453  rspex  14454  2idlvalg  14483  zrhvalg  14598  zlmval  14607  mplvalcoe  14670  mplbascoe  14671  mplplusgg  14683  toponsspwpwg  14712  eltg  14742  eltg2  14743  restbasg  14858  tgrest  14859  txvalex  14944  txval  14945  ispsmet  15013  ismet  15034  isxmet  15035  xmetunirn  15048  blfvalps  15075  vtxvalg  15833  iedgvalg  15834  vtxex  15835  edgvalg  15876  vtxdgfval  16048  wksfval  16068  iswlkg  16075  wlkvtxeledgg  16090  trlsfvalg  16127  clwwlkg  16136  clwwlkng  16148  bj-vtoclgft  16222  djucllem  16247  bj-nvel  16343  2omapen  16447  pw1mapen  16449