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 )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   E.wex 1545   e. wcel 2209   _Vcvv 2821

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 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 theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced 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  3649  elpwb  3695  snidb  3735  eldifvsn  3842  snssg  3844  dfopg  3897  eluni  3933  eliun  4011  csbexga  4256  nvel  4261  class2seteq  4295  axpweq  4303  snelpwi  4346  opexg  4363  elopab  4395  epelg  4430  elon2  4516  unexg  4584  reuhypd  4612  sucexg  4640  onsucb  4645  onsucelsucr  4650  sucunielr  4652  en2lp  4696  peano2  4737  peano2b  4757  opelvvg  4819  opeliunxp  4825  opeliunxp2  4915  ideqg  4926  elrnmptg  5029  imasng  5147  iniseg  5154  opswapg  5269  elxp4  5270  elxp5  5271  dmmptg  5280  iota2  5362  fnmpt  5505  fvexg  5709  fvelimab  5753  mptfvex  5785  fvmptdf  5787  fvmptdv2  5789  mpteqb  5790  fvmptt  5791  fvmptf  5792  fvopab6  5796  fsn2  5873  fmptpr  5898  eloprabga  6165  ovmpos  6202  ov2gf  6203  ovmpodxf  6204  ovmpox  6207  ovmpoga  6208  ovmpodf  6210  ovi3  6216  ovelrn  6228  suppssov1  6289  offval3  6357  1stexg  6391  2ndexg  6392  elxp6  6393  elxp7  6394  releldm2  6409  fnmpo  6428  mpofvex  6431  mpoexg  6437  suppval  6467  opeliunxp2f  6499  brtpos2  6512  rdgtfr  6635  rdgruledefgg  6636  frec0g  6658  sucinc2  6709  nntri3or  6756  relelec  6839  ecdmn0m  6841  mapvalg  6922  pmvalg  6923  elpmg  6928  elixp2  6974  mptelixpg  7006  elixpsn  7007  map1  7091  rex2dom  7100  mapdom1g  7137  mapxpen  7138  fival  7294  elfi2  7296  2omapen  7309  djulclr  7379  djurclr  7380  djulcl  7381  djurcl  7382  djulclb  7385  inl11  7395  djuss  7400  1stinl  7404  2ndinl  7405  1stinr  7406  2ndinr  7407  ismkvnex  7485  omniwomnimkv  7497  isacnm  7549  cc4n  7627  elinp  7831  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemfl  7932  mulnqprlemfu  7933  recexprlemell  7979  recexprlemelu  7980  hashmap  11246  wrdexg  11293  wrdsymb0  11315  lswwrd  11329  ccatfvalfi  11338  swrdval  11398  swrd00g  11399  pfxval  11424  cats1fvn  11514  cats1fvnd  11515  s2fv1g  11538  s2leng  11539  s2dmg  11540  shftfvalg  11561  clim  12025  climmpt  12044  climshft2  12050  4sqlem2  13146  ballotfilemsv  13231  isstruct2r  13341  slotex  13357  setsvalg  13360  setsfun0  13366  setscom  13370  ressvalsets  13395  ressbasid  13401  restval  13576  topnvalg  13582  tgval  13593  ptex  13595  imasex  13603  qusex  13623  qusaddvallemg  13631  xpsfrnel2  13644  plusffvalg  13659  grpidvalg  13670  gzsum0  13690  sgrp1  13703  issubmnd  13732  issubm  13756  grppropstrg  13801  grpinvfvalg  13824  grpinvfng  13826  grpsubfvalg  13827  grpressid  13843  mulgfvalg  13901  mulgex  13903  mulgfng  13904  issubg  13953  subgex  13956  releqgg  14000  eqgex  14001  eqgfval  14002  isghm  14023  ablressid  14116  prdsex  14149  pwsval  14181  pwsbas  14182  pwselbasb  14183  pwssnf1o  14188  pws0g  14190  mgpvalg  14197  mgptopng  14203  rngressid  14228  rngpropd  14229  ringidvalg  14239  dfur2g  14240  issrg  14243  iscrng2  14293  ringressid  14341  opprvalg  14347  opprringb  14359  dvdsrex  14378  unitgrp  14396  unitabl  14397  unitlinv  14406  unitrinv  14407  isnzr2  14464  issubrng  14480  issubrg  14502  subrgugrp  14521  aprap  14571  aprprop  14574  islmod  14600  scaffvalg  14615  lsssetm  14665  islssmg  14667  lspfval  14697  lspval  14699  lspcl  14700  lspex  14704  sraval  14746  rlmvalg  14763  rlmsubg  14767  rlmvnegg  14774  ixpsnbasval  14775  lidlvalg  14780  rspvalg  14781  lidlex  14782  rspex  14783  2idlvalg  14812  zrhvalg  14925  zlmval  14934  mplvalcoe  15004  mplbascoe  15005  mplplusgg  15017  toponsspwpwg  15046  eltg  15076  eltg2  15077  restbasg  15192  tgrest  15193  txvalex  15278  txval  15279  ispsmet  15347  ismet  15368  isxmet  15369  xmetunirn  15382  blfvalps  15409  vtxvalg  16171  iedgvalg  16172  vtxex  16173  edgvalg  16214  vtxdgfval  16443  wksfval  16477  iswlkg  16484  wlkvtxeledgg  16499  trlsfvalg  16538  clwwlkg  16548  clwwlkng  16560  eupthsg  16600  bj-vtoclgft  16717  djucllem  16742  bj-nvel  16837  pw1mapen  16940