Theorem vex 2806

Description: All setvar variables are sets (see isset 2810). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	|- x e. _V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		equid 1749	. 2 |- x = x
2		df-v 2805	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2342	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 146	1 |- x e. _V

Syntax hints:   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:  elv  2807  elvd  2808  el2v  2809  isset  2810  eqvisset  2814  ralv  2821  rexv  2822  reuv  2823  rmov  2824  rabab  2825  sbhypf  2854  ceqex  2934  ralab  2967  rexab  2969  mo2icl  2986  reu8  3003  csbvarg  3156  csbiebg  3171  sbcnestgf  3180  sbnfc2  3189  ddifnel  3340  ddifstab  3341  csbing  3416  unssdif  3444  unssin  3448  inssun  3449  invdif  3451  vn0  3507  vn0m  3508  eqv  3516  abvor0dc  3520  sbss  3604  velpw  3663  elpwg  3664  velsn  3690  vsnid  3705  exsnrex  3715  dftp2  3722  prmg  3798  prnzg  3801  snssgOLD  3814  difprsnss  3816  sneqrg  3850  preq12bg  3861  pwprss  3894  pwtpss  3895  pwv  3897  unipr  3912  uniprg  3913  unisng  3915  elintg  3941  elintrabg  3946  intss1  3948  ssint  3949  intmin  3953  intss  3954  intssunim  3955  intmin4  3961  intab  3962  intun  3964  intpr  3965  intprg  3966  uniintsnr  3969  iinconstm  3984  iuniin  3985  iinss1  3987  dfiin2g  4008  dfiunv2  4011  ssiinf  4025  iinss  4027  iinss2  4028  0iin  4034  iinab  4037  iundif2ss  4041  iindif2m  4043  iinin2m  4044  iinuniss  4058  sspwuni  4060  pwpwab  4063  iinpw  4066  iunpwss  4067  brab1  4141  csbopabg  4172  mptv  4191  trint  4207  vnex  4225  inex1g  4230  ssexg  4233  inteximm  4244  inuni  4250  repizf2  4258  axpweq  4267  bnd2  4269  pwuni  4288  exmidundif  4302  exmidundifim  4303  zfpair2  4306  rext  4313  sspwb  4314  unipw  4315  ssextss  4318  euabex  4323  mss  4324  exss  4325  opth  4335  opthg  4336  copsexg  4342  copsex4g  4345  moop2  4350  euotd  4353  opabid  4356  elopab  4358  opelopabsbALT  4359  opelopabsb  4360  opabm  4381  pwin  4385  pwunss  4386  epelg  4393  epel  4395  pofun  4415  epse  4445  tron  4485  sucel  4513  suctr  4524  vuniex  4541  uniexg  4542  unexb  4545  snnex  4551  pwnex  4552  uniuni  4554  eusvnf  4556  eusvnfb  4557  iunpw  4583  unon  4615  ordunisuc2r  4618  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsucunielexmid  4635  elirr  4645  en2lp  4658  dtruex  4663  onintexmid  4677  reg3exmidlemwe  4683  dcextest  4685  finds  4704  finds2  4705  elomssom  4709  limom  4718  0nelxp  4759  opelxp  4761  opeliunxp  4787  elvv  4794  elvvv  4795  elvvuni  4796  xpsspw  4844  relopabiv  4859  relopabi  4861  opabid2  4867  difopab  4869  xpiindim  4873  raliunxp  4877  rexiunxp  4878  ralxpf  4882  rexxpf  4883  relop  4886  cnvco  4921  dfrn2  4924  dfdm4  4929  dmss  4936  dmin  4945  dmiun  4946  dmuni  4947  dm0  4951  dmi  4952  reldm0  4955  reldmm  4956  elreldm  4964  elrnmpt1  4989  dmrnssfld  5001  dmcoss  5008  dmcosseq  5010  opelresg  5026  resieq  5029  dmres  5040  elres  5055  relssres  5057  resopab  5063  resiexg  5064  iss  5065  dfres2  5071  restidsing  5075  dfima2  5084  imadmrn  5092  imai  5099  csbima12g  5104  elimasng  5111  args  5112  epini  5114  iniseg  5115  dfse2  5116  exse2  5117  cotr  5125  issref  5126  cnvsym  5127  intasym  5128  asymref  5129  intirr  5130  brcodir  5131  codir  5132  qfto  5133  poirr2  5136  cnvopab  5145  cnv0  5147  cnvi  5148  cnvdif  5150  rniun  5154  dminss  5158  imainss  5159  inimasn  5161  xpmlem  5164  dmxpss  5174  rnxpid  5178  ssrnres  5186  rninxp  5187  dminxp  5188  cnvcnv3  5193  dfrel2  5194  dmsnm  5209  dmsnopg  5215  cnvcnvsn  5220  dmsnsnsng  5221  cnvsng  5229  elxp4  5231  elxp5  5232  cnvresima  5233  dfco2  5243  dfco2a  5244  cores  5247  resco  5248  imaco  5249  rnco  5250  coiun  5253  co02  5257  coi1  5259  coass  5262  relssdmrn  5264  unielrel  5271  ressn  5284  cnviinm  5285  cnvpom  5286  cnvsom  5287  uniabio  5304  iotaval  5305  iotass  5311  sniota  5324  csbiotag  5326  dffun2  5343  dffun7  5360  dffun8  5361  dffun9  5362  funopg  5367  funssres  5376  funun  5378  funcnvsn  5382  funinsn  5386  funcnv2  5397  funcnv  5398  funcnv3  5399  funcnveq  5400  fun2cnv  5401  funcnvuni  5406  imadif  5417  funimaexglem  5420  isarep1  5423  2elresin  5450  fnres  5456  fcnvres  5528  fconstg  5542  fun11iun  5613  f1osng  5635  dffv3g  5644  fvssunirng  5663  sefvex  5669  fv3  5671  fvres  5672  nfunsn  5685  funimass4  5705  ssimaexg  5717  dmfco  5723  fvopab6  5752  fndmdif  5761  fvelrn  5786  dffo4  5803  f1ompt  5806  fmptco  5821  fsn  5827  fsng  5828  fsn2g  5830  dfmpt  5833  dfmptg  5835  funopsn  5838  funop  5839  funopdmsn  5842  fnressn  5848  fressnfv  5849  fvsng  5858  resfunexg  5883  funfvima3  5898  idref  5907  abrexco  5910  imaiun  5911  dff13  5919  foeqcnvco  5941  f1eqcocnv  5942  fliftcnv  5946  isocnv2  5963  isoini  5969  isose  5972  riotav  5987  csbriotag  5995  acexmidlem2  6025  oprabid  6060  csbov123g  6067  0neqopab  6076  brabvv  6077  dfoprab2  6078  rnoprab  6114  eloprabga  6118  mpov  6121  f1opw  6240  opabex3d  6292  opabex3  6293  ofmres  6307  uchoice  6309  op1stg  6322  op2ndg  6323  1stval2  6327  2ndval2  6328  fo1st  6329  fo2nd  6330  f1stres  6331  f2ndres  6332  fo1stresm  6333  fo2ndresm  6334  xp1st  6337  xp2nd  6338  releldm2  6357  reldm  6358  sbcopeq1a  6359  csbopeq1a  6360  dfoprab3  6363  opabn1stprc  6367  eloprabi  6370  mpomptsx  6371  dmmpossx  6373  fmpox  6374  mpofvex  6379  mpoexxg  6384  fmpoco  6390  df1st2  6393  df2nd2  6394  1stconst  6395  2ndconst  6396  dfmpo  6397  fo2ndf  6401  f1o2ndf1  6402  xporderlem  6405  cnvoprab  6408  f1od2  6409  suppval1  6417  cnvimadfsn  6423  suppimacnvfn  6424  brtpos2  6460  reldmtpos  6462  dmtpos  6465  rntpos  6466  ovtposg  6468  dftpos3  6471  dftpos4  6472  tpostpos  6473  tpossym  6485  tfrlem3  6520  tfrlem5  6523  tfrlem8  6527  tfrlemisucfn  6533  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemibex  6538  tfrlemi14d  6542  tfrexlem  6543  tfr1onlem3  6547  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  tfrcl  6573  rdgtfr  6583  rdgruledefgg  6584  rdgivallem  6590  rdgon  6595  rdg0g  6597  frec0g  6606  frecabex  6607  frecabcl  6608  frectfr  6609  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  oafnex  6655  sucinc  6656  fnoa  6658  oaexg  6659  omfnex  6660  fnom  6661  omexg  6662  fnoei  6663  oeiexg  6664  oeiv  6667  oacl  6671  omcl  6672  oeicl  6673  oav2  6674  nnsucelsuc  6702  nnsucuniel  6706  ercnv  6766  iserd  6771  eqerlem  6776  eqer  6777  ecdmn0m  6789  erth  6791  qsss  6806  ecid  6810  ecidg  6811  qsid  6812  iinerm  6819  qsel  6824  erovlem  6839  ecopovsym  6843  ecopover  6845  th3qlem2  6850  mapprc  6864  fnmap  6867  fnpm  6868  mapdm0  6875  mapval2  6890  mapsn  6902  mapsncnv  6907  mapsnf1o2  6908  ixpconstg  6919  ixpprc  6931  ixpin  6935  ixpiinm  6936  ixpssmap2g  6939  ixpssmapg  6940  elixpsn  6947  ixpsnf1o  6948  bren  6960  brdomg  6962  domen  6965  domeng  6966  idssen  6993  domssr  6994  ener  6996  domtr  7002  ensn1g  7014  en1  7016  en1bg  7017  fundmen  7024  fundmeng  7025  mapsnen  7029  fiprc  7033  unen  7034  rex2dom  7039  en2m  7042  dom1o  7045  xpsnen  7048  xpsneng  7049  xpcomco  7053  xpcomeng  7055  xpassen  7057  xpdom2  7058  xpdom2g  7059  pw2f1odc  7064  xpf1o  7073  mapen  7075  mapxpen  7077  xpmapenlem  7078  ssenen  7080  phplem4  7084  phplem3g  7085  nneneq  7086  php5  7087  phpm  7095  findcard  7120  findcard2  7121  findcard2s  7122  isinfinf  7129  ac6sfi  7130  exmidpw  7143  exmidpweq  7144  exmidpw2en  7147  unfidisj  7157  fiintim  7166  xpfi  7167  fisseneq  7170  ssfirab  7172  snexxph  7192  fidcenumlemr  7197  sbthlemi10  7208  isbth  7209  ssfii  7216  fi0  7217  fiss  7219  cnvinfex  7260  eqinfti  7262  infvalti  7264  infglbti  7267  infmoti  7270  ordiso2  7277  djuf1olem  7295  djuss  7312  ctm  7351  ctssdccl  7353  ctssdclemr  7354  finomni  7382  exmidomni  7384  fodjuomnilemdc  7386  nninfwlpoimlemginf  7418  pm54.43  7438  pr2cv1  7443  exmidfodomrlemim  7455  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  finacn  7462  acfun  7465  ccfunen  7526  cc2lem  7528  cc3  7530  acnccim  7534  indpi  7605  dfplpq2  7617  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nqnq0  7704  mulnnnq0  7713  nqprm  7805  nqprrnd  7806  nqprdisj  7807  nqprloc  7808  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemrl  7836  mulnqprlemru  7837  mulnqprlemfl  7838  mulnqprlemfu  7839  ltnqpr  7856  ltnqpri  7857  archpr  7906  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlem2  7923  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemopu  7962  suplocexprlemmu  7981  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  cnm  8095  ltresr  8102  peano1nnnn  8115  peano2nnnn  8116  axcnre  8144  axpre-apti  8148  renfdisj  8281  dfinfre  9178  1nn  9196  peano2nn  9197  indstr  9871  cnref1o  9929  ioof  10250  fzpr  10357  frec2uzrand  10713  frec2uzf1od  10714  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  frecfzennn  10734  seqp1g  10774  seqclg  10780  seqf1og  10829  seqfeq4g  10839  ser3le  10845  hashinfom  11086  hashunlem  11113  hashun  11114  hashxp  11136  hashfacen  11146  zfz1isolem1  11150  zfz1iso  11151  fundm2domnop0  11158  wrdexb  11174  fnpfx  11307  cats1un  11351  wrdind  11352  wrd2ind  11353  shftfvalg  11441  ovshftex  11442  shftfibg  11443  shftfval  11444  shftfib  11446  shftfn  11447  2shfti  11454  shftvalg  11459  shftval4g  11460  maxabslemval  11831  fimaxre2  11850  xrmaxiflemval  11873  fclim  11917  climshft  11927  zsumdc  12008  fsum3  12011  fsum2dlemstep  12058  fsumcnv  12061  fisumcom2  12062  fisum0diag2  12071  fsumconst  12078  modfsummodlemstep  12081  fsumabs  12089  fsumrelem  12095  fsumiun  12101  ntrivcvgap  12172  fprod2dlemstep  12246  fprodcnv  12249  fprodcom2fi  12250  fprodmodd  12265  nninfct  12675  algrf  12680  qredeu  12732  isprm2  12752  prmind2  12755  4sqlemafi  13031  4sqlem12  13038  ennnfonelemex  13098  ennnfonelemrn  13103  exmidunben  13110  ctinfom  13112  ctinf  13114  qnnen  13115  enctlem  13116  ctiunctlemfo  13123  slotslfn  13171  setscomd  13186  restfn  13389  elrest  13392  ptex  13410  prdsex  13415  prdsvallem  13418  prdsval  13419  prdsbaslemss  13420  prdsbas  13422  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfnlemg  13460  fnpr2ob  13486  ismgm  13503  plusffng  13511  fn0g  13521  fngsum  13534  gsumsplit1r  13544  gsumprval  13545  issgrp  13549  ismnddef  13564  gsumfzz  13641  gsumfzcl  13645  mulgnngsum  13777  subgintm  13848  releqgg  13870  eqgex  13871  eqgfval  13872  eqgval  13873  isghm  13893  fnmgp  13999  isrng  14011  isring  14077  ringn0  14137  opprrngbg  14155  opprsubgg  14161  opprunitd  14188  dfrhm2  14232  rhmex  14235  opprsubrngg  14289  subrngintm  14290  subrngpropd  14294  subrgpropd  14331  isdomn  14348  opprdomnbg  14353  scaffng  14388  rmodislmodlem  14429  rmodislmod  14430  lssex  14433  lsssn0  14449  lss1d  14462  lssintclm  14463  ellspsn  14496  rlmfn  14532  isridl  14583  blfn  14630  mopnset  14631  metuex  14634  znval  14715  znleval  14732  psrval  14745  fnpsr  14746  mplvalcoe  14774  fnmpl  14777  bastg  14855  distop  14879  topnex  14880  epttop  14884  tgrest  14963  resttopon  14965  restco  14968  cnrest2  15030  cnptopresti  15032  cnptoprest  15033  cnptoprest2  15034  txuni2  15050  txbas  15052  eltx  15053  txcnp  15065  txcnmpt  15067  txrest  15070  txdis1cn  15072  txlm  15073  cnmpt1st  15082  cnmpt2nd  15083  txhmeo  15113  txswaphmeolem  15114  xmetec  15231  metrest  15300  reldvg  15473  dvfgg  15482  dvcj  15503  dvmptfsum  15519  elply2  15529  pilem3  15577  lgsquadlem1  15879  lgsquadlem2  15880  upgrex  16027  upgr1een  16048  umgredg  16069  umgredgnlp  16076  usgredgreu  16140  uspgredg2vtxeu  16142  ushgredgedg  16150  ushgredgedgloop  16152  griedg0ssusgr  16175  uhgrspansubgrlem  16200  upgrspanop  16207  umgrspanop  16208  usgrspanop  16209  wlkvtxiedg  16269  wlkvtxiedgg  16270  wlk1walkdom  16283  eulerpathum  16405  depindlem1  16430  bdcvv  16556  bdsnss  16572  bdop  16574  bj-vprc  16595  bdinex1g  16600  bdssexg  16603  bj-inex  16606  bj-zfpair2  16609  bj-uniexg  16617  bdunexb  16619  bj-unexg  16620  bj-indint  16630  bj-ssom  16635  bj-om  16636  bj-2inf  16637  bj-bdfindis  16646  bj-nn0suc0  16649  bj-nnelirr  16652  bj-inf2vnlem1  16669  bj-inf2vnlem2  16670  bj-omex2  16676  bj-nn0sucALT  16677  bj-findis  16678  ss1oel2o  16690  domomsubct  16706  pw1nct  16708  nninfsellemeq  16723  exmidsbthrlem  16733  gfsumval  16792