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  5646  fvelimab  5690  mptfvex  5720  fvmptdf  5722  fvmptdv2  5724  mpteqb  5725  fvmptt  5726  fvmptf  5727  fvopab6  5731  fsn2  5809  fmptpr  5831  eloprabga  6091  ovmpos  6128  ov2gf  6129  ovmpodxf  6130  ovmpox  6133  ovmpoga  6134  ovmpodf  6136  ovi3  6142  ovelrn  6154  suppssfv  6214  suppssov1  6215  offval3  6279  1stexg  6313  2ndexg  6314  elxp6  6315  elxp7  6316  releldm2  6331  fnmpo  6348  mpofvex  6351  mpoexg  6357  opeliunxp2f  6384  brtpos2  6397  rdgtfr  6520  rdgruledefgg  6521  frec0g  6543  sucinc2  6592  nntri3or  6639  relelec  6722  ecdmn0m  6724  mapvalg  6805  pmvalg  6806  elpmg  6811  elixp2  6849  mptelixpg  6881  elixpsn  6882  map1  6965  rex2dom  6971  mapdom1g  7008  mapxpen  7009  fival  7137  elfi2  7139  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  djulclb  7222  inl11  7232  djuss  7237  1stinl  7241  2ndinl  7242  1stinr  7243  2ndinr  7244  ismkvnex  7322  omniwomnimkv  7334  isacnm  7385  cc4n  7457  elinp  7661  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemfl  7762  mulnqprlemfu  7763  recexprlemell  7809  recexprlemelu  7810  wrdexg  11082  wrdsymb0  11104  lswwrd  11118  ccatfvalfi  11127  swrdval  11180  swrd00g  11181  pfxval  11206  cats1fvn  11296  cats1fvnd  11297  s2fv1g  11320  s2leng  11321  s2dmg  11322  shftfvalg  11329  clim  11792  climmpt  11811  climshft2  11817  4sqlem2  12912  isstruct2r  13043  slotex  13059  setsvalg  13062  setsfun0  13068  setscom  13072  ressvalsets  13097  ressbasid  13103  restval  13278  topnvalg  13284  tgval  13295  ptex  13297  prdsex  13302  pwsval  13324  pwsbas  13325  pwselbasb  13326  pwssnf1o  13331  imasex  13338  qusex  13358  qusaddvallemg  13366  xpsfrnel2  13379  plusffvalg  13395  grpidvalg  13406  gsum0g  13429  sgrp1  13444  issubmnd  13475  pws0g  13484  issubm  13505  grppropstrg  13552  grpinvfvalg  13575  grpinvfng  13577  grpsubfvalg  13578  grpressid  13594  mulgfvalg  13658  mulgex  13660  mulgfng  13661  issubg  13710  subgex  13713  releqgg  13757  eqgex  13758  eqgfval  13759  isghm  13780  ablressid  13872  mgpvalg  13886  mgptopng  13892  rngressid  13917  rngpropd  13918  ringidvalg  13924  dfur2g  13925  issrg  13928  iscrng2  13978  ringressid  14026  opprvalg  14032  dvdsrex  14062  unitgrp  14080  unitabl  14081  unitlinv  14090  unitrinv  14091  isnzr2  14148  issubrng  14163  issubrg  14185  subrgugrp  14204  aprap  14250  islmod  14255  scaffvalg  14270  lsssetm  14320  islssmg  14322  lspfval  14352  lspval  14354  lspcl  14355  lspex  14359  sraval  14401  rlmvalg  14418  rlmsubg  14422  rlmvnegg  14429  ixpsnbasval  14430  lidlvalg  14435  rspvalg  14436  lidlex  14437  rspex  14438  2idlvalg  14467  zrhvalg  14582  zlmval  14591  mplvalcoe  14654  mplbascoe  14655  mplplusgg  14667  toponsspwpwg  14696  eltg  14726  eltg2  14727  restbasg  14842  tgrest  14843  txvalex  14928  txval  14929  ispsmet  14997  ismet  15018  isxmet  15019  xmetunirn  15032  blfvalps  15059  vtxvalg  15817  iedgvalg  15818  vtxex  15819  edgvalg  15860  wksfval  16035  iswlkg  16041  wlkvtxeledgg  16055  bj-vtoclgft  16139  djucllem  16164  bj-nvel  16260  2omapen  16360  pw1mapen  16362