Theorem elex 2815

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 2227	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2810	. 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 2202   _Vcvv 2803

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 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805

This theorem is referenced by:  elexi  2816  elexd  2817  elisset  2818  vtoclgft  2855  vtoclgf  2863  vtoclg1f  2864  vtocl2gf  2867  vtocl3gf  2868  spcimgft  2883  spcimegft  2885  elab4g  2956  elrabf  2961  mob  2989  sbcex  3041  sbcel1v  3095  sbcabel  3115  csbcomg  3151  csbvarg  3156  csbiebt  3168  csbnestgf  3181  csbidmg  3185  sbcco3g  3186  csbco3g  3187  eldif  3210  ssv  3250  elun  3350  elin  3392  elif  3621  elpwb  3666  snidb  3703  eldifvsn  3810  snssg  3812  dfopg  3865  eluni  3901  eliun  3979  csbexga  4222  nvel  4227  class2seteq  4259  axpweq  4267  snelpwi  4309  opexg  4326  elopab  4358  epelg  4393  elon2  4479  unexg  4546  reuhypd  4574  sucexg  4602  onsucb  4607  onsucelsucr  4612  sucunielr  4614  en2lp  4658  peano2  4699  peano2b  4719  opelvvg  4781  opeliunxp  4787  opeliunxp2  4876  ideqg  4887  elrnmptg  4990  imasng  5108  iniseg  5115  opswapg  5230  elxp4  5231  elxp5  5232  dmmptg  5241  iota2  5323  fnmpt  5466  fvexg  5667  fvelimab  5711  mptfvex  5741  fvmptdf  5743  fvmptdv2  5745  mpteqb  5746  fvmptt  5747  fvmptf  5748  fvopab6  5752  fsn2  5829  fmptpr  5854  eloprabga  6118  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  ovmpox  6160  ovmpoga  6161  ovmpodf  6163  ovi3  6169  ovelrn  6181  suppssov1  6241  offval3  6305  1stexg  6339  2ndexg  6340  elxp6  6341  elxp7  6342  releldm2  6357  fnmpo  6376  mpofvex  6379  mpoexg  6385  suppval  6415  opeliunxp2f  6447  brtpos2  6460  rdgtfr  6583  rdgruledefgg  6584  frec0g  6606  sucinc2  6657  nntri3or  6704  relelec  6787  ecdmn0m  6789  mapvalg  6870  pmvalg  6871  elpmg  6876  elixp2  6914  mptelixpg  6946  elixpsn  6947  map1  7030  rex2dom  7039  mapdom1g  7076  mapxpen  7077  fival  7229  elfi2  7231  djulclr  7308  djurclr  7309  djulcl  7310  djurcl  7311  djulclb  7314  inl11  7324  djuss  7329  1stinl  7333  2ndinl  7334  1stinr  7335  2ndinr  7336  ismkvnex  7414  omniwomnimkv  7426  isacnm  7478  cc4n  7550  elinp  7754  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprlemfl  7855  mulnqprlemfu  7856  recexprlemell  7902  recexprlemelu  7903  wrdexg  11190  wrdsymb0  11212  lswwrd  11226  ccatfvalfi  11235  swrdval  11295  swrd00g  11296  pfxval  11321  cats1fvn  11411  cats1fvnd  11412  s2fv1g  11435  s2leng  11436  s2dmg  11437  shftfvalg  11458  clim  11921  climmpt  11940  climshft2  11946  4sqlem2  13042  isstruct2r  13173  slotex  13189  setsvalg  13192  setsfun0  13198  setscom  13202  ressvalsets  13227  ressbasid  13233  restval  13408  topnvalg  13414  tgval  13425  ptex  13427  prdsex  13432  pwsval  13454  pwsbas  13455  pwselbasb  13456  pwssnf1o  13461  imasex  13468  qusex  13488  qusaddvallemg  13496  xpsfrnel2  13509  plusffvalg  13525  grpidvalg  13536  gsum0g  13559  sgrp1  13574  issubmnd  13605  pws0g  13614  issubm  13635  grppropstrg  13682  grpinvfvalg  13705  grpinvfng  13707  grpsubfvalg  13708  grpressid  13724  mulgfvalg  13788  mulgex  13790  mulgfng  13791  issubg  13840  subgex  13843  releqgg  13887  eqgex  13888  eqgfval  13889  isghm  13910  ablressid  14002  mgpvalg  14017  mgptopng  14023  rngressid  14048  rngpropd  14049  ringidvalg  14055  dfur2g  14056  issrg  14059  iscrng2  14109  ringressid  14157  opprvalg  14163  dvdsrex  14193  unitgrp  14211  unitabl  14212  unitlinv  14221  unitrinv  14222  isnzr2  14279  issubrng  14294  issubrg  14316  subrgugrp  14335  aprap  14382  islmod  14387  scaffvalg  14402  lsssetm  14452  islssmg  14454  lspfval  14484  lspval  14486  lspcl  14487  lspex  14491  sraval  14533  rlmvalg  14550  rlmsubg  14554  rlmvnegg  14561  ixpsnbasval  14562  lidlvalg  14567  rspvalg  14568  lidlex  14569  rspex  14570  2idlvalg  14599  zrhvalg  14714  zlmval  14723  mplvalcoe  14791  mplbascoe  14792  mplplusgg  14804  toponsspwpwg  14833  eltg  14863  eltg2  14864  restbasg  14979  tgrest  14980  txvalex  15065  txval  15066  ispsmet  15134  ismet  15155  isxmet  15156  xmetunirn  15169  blfvalps  15196  vtxvalg  15957  iedgvalg  15958  vtxex  15959  edgvalg  16000  vtxdgfval  16229  wksfval  16263  iswlkg  16270  wlkvtxeledgg  16285  trlsfvalg  16324  clwwlkg  16334  clwwlkng  16346  eupthsg  16386  bj-vtoclgft  16493  djucllem  16518  bj-nvel  16613  2omapen  16716  pw1mapen  16718