Theorem vex 2818

Description: All setvar variables are sets (see isset 2822). 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 2817	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2345	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 146	1 |- x e. _V

Syntax hints:   e. wcel 2205   _Vcvv 2815

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 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elv  2819  elvd  2820  el2v  2821  isset  2822  eqvisset  2826  ralv  2833  rexv  2834  reuv  2835  rmov  2836  rabab  2837  sbhypf  2866  ceqex  2947  ralab  2980  rexab  2982  mo2icl  2999  reu8  3016  csbvarg  3169  csbiebg  3184  sbcnestgf  3193  sbnfc2  3202  ddifnel  3354  ddifstab  3355  csbing  3432  unssdif  3460  unssin  3464  inssun  3465  invdif  3467  vn0  3523  vn0m  3524  eqv  3532  abvor0dc  3536  sbss  3621  velpw  3681  elpwg  3682  velsn  3711  vsnid  3726  exsnrex  3736  dftp2  3743  prmg  3819  prnzg  3822  snssgOLD  3835  difprsnss  3837  sneqrg  3871  preq12bg  3882  pwprss  3915  pwtpss  3916  pwv  3918  unipr  3933  uniprg  3934  unisng  3936  elintg  3962  elintrabg  3967  intss1  3969  ssint  3970  intmin  3974  intss  3975  intssunim  3976  intmin4  3982  intab  3983  intun  3985  intpr  3986  intprg  3987  uniintsnr  3990  iinconstm  4005  iuniin  4006  iinss1  4008  dfiin2g  4029  dfiunv2  4032  ssiinf  4046  iinss  4048  iinss2  4049  0iin  4055  iinab  4058  iundif2ss  4062  iindif2m  4064  iinin2m  4065  iinuniss  4079  sspwuni  4081  pwpwab  4084  iinpw  4087  iunpwss  4088  brab1  4162  csbopabg  4193  mptv  4212  trint  4228  vnex  4246  inex1g  4251  ssexg  4254  inteximm  4266  inuni  4272  repizf2  4280  axpweq  4289  bnd2  4291  pwuni  4310  exmidundif  4324  exmidundifim  4325  zfpair2  4328  rext  4336  sspwb  4337  unipw  4338  ssextss  4341  euabex  4346  mss  4347  exss  4348  opth  4358  opthg  4359  copsexg  4365  copsex4g  4368  moop2  4373  euotd  4376  opabid  4379  elopab  4381  opelopabsbALT  4382  opelopabsb  4383  opabm  4404  pwin  4408  pwunss  4409  epelg  4416  epel  4418  pofun  4438  epse  4468  tron  4508  sucel  4536  suctr  4547  vuniex  4564  uniexg  4565  unexb  4568  snnex  4574  pwnex  4575  uniuni  4577  eusvnf  4579  eusvnfb  4580  iunpw  4606  unon  4638  ordunisuc2r  4641  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordsucunielexmid  4658  elirr  4668  en2lp  4681  dtruex  4686  onintexmid  4700  reg3exmidlemwe  4706  dcextest  4708  finds  4727  finds2  4728  elomssom  4732  limom  4741  0nelxp  4782  opelxp  4784  opeliunxp  4810  elvv  4817  elvvv  4818  elvvuni  4819  xpsspw  4867  relopabiv  4883  relopabi  4885  opabid2  4891  difopab  4893  xpiindim  4897  raliunxp  4901  rexiunxp  4902  ralxpf  4906  rexxpf  4907  relop  4910  cnvco  4945  dfrn2  4948  dfdm4  4953  dmss  4960  dmin  4969  dmiun  4970  dmuni  4971  dm0  4975  dmi  4976  reldm0  4979  reldmm  4980  elreldm  4988  elrnmpt1  5013  dmrnssfld  5025  dmcoss  5032  dmcosseq  5034  opelresg  5050  resieq  5053  dmres  5064  elres  5079  relssres  5081  resopab  5087  resiexg  5088  iss  5089  dfres2  5095  restidsing  5099  dfima2  5108  imadmrn  5116  imai  5123  csbima12g  5128  elimasng  5135  args  5136  epini  5138  iniseg  5139  dfse2  5140  exse2  5141  cotr  5149  issref  5150  cnvsym  5151  intasym  5152  asymref  5153  intirr  5154  brcodir  5155  codir  5156  qfto  5157  poirr2  5160  cnvopab  5169  cnv0  5171  cnvi  5172  cnvdif  5174  rniun  5178  dminss  5182  imainss  5183  inimasn  5185  xpmlem  5188  dmxpss  5198  rnxpid  5202  ssrnres  5210  rninxp  5211  dminxp  5212  cnvcnv3  5217  dfrel2  5218  dmsnm  5233  dmsnopg  5239  cnvcnvsn  5244  dmsnsnsng  5245  cnvsng  5253  elxp4  5255  elxp5  5256  cnvresima  5257  dfco2  5267  dfco2a  5268  cores  5271  resco  5272  imaco  5273  rnco  5274  coiun  5277  co02  5281  coi1  5283  coass  5286  relssdmrn  5288  unielrel  5295  ressn  5308  cnviinm  5309  cnvpom  5310  cnvsom  5311  uniabio  5328  iotaval  5329  iotass  5335  sniota  5348  csbiotag  5350  dffun2  5367  dffun7  5384  dffun8  5385  dffun9  5386  funopg  5391  funssres  5400  funun  5402  funcnvsn  5406  funinsn  5410  funcnv2  5421  funcnv  5422  funcnv3  5423  funcnveq  5424  fun2cnv  5425  funcnvuni  5430  imadif  5441  funimaexglem  5444  isarep1  5447  2elresin  5474  fnres  5480  fcnvres  5555  fconstg  5569  fun11iun  5640  f1osng  5662  dffv3g  5671  fvssunirng  5690  sefvex  5696  fv3  5698  fvres  5699  nfunsn  5712  funimass4  5732  ssimaexg  5744  dmfco  5750  fvopab6  5779  fndmdif  5788  fvelrn  5813  dffo4  5830  f1ompt  5833  fmptco  5848  fsn  5854  fsng  5855  fsn2g  5857  dfmpt  5860  dfmptg  5862  funopsn  5865  funop  5866  funopdmsn  5869  fnressn  5875  fressnfv  5876  fvsng  5885  resfunexg  5910  funfvima3  5925  idref  5935  abrexco  5938  imaiun  5939  dff13  5947  foeqcnvco  5969  f1eqcocnv  5970  fliftcnv  5974  isocnv2  5991  isoini  5997  isose  6000  riotav  6017  csbriotag  6025  acexmidlem2  6055  oprabid  6090  csbov123g  6097  0neqopab  6106  brabvv  6107  dfoprab2  6108  rnoprab  6144  eloprabga  6148  mpov  6151  f1opw  6270  opabex3d  6323  opabex3  6324  abrexss  6331  ofmres  6342  uchoice  6344  op1stg  6357  op2ndg  6358  1stval2  6362  2ndval2  6363  fo1st  6364  fo2nd  6365  f1stres  6366  f2ndres  6367  fo1stresm  6368  fo2ndresm  6369  xp1st  6372  xp2nd  6373  releldm2  6392  reldm  6393  sbcopeq1a  6394  csbopeq1a  6395  dfoprab3  6398  opabn1stprc  6402  eloprabi  6405  mpomptsx  6406  dmmpossx  6408  fmpox  6409  mpofvex  6414  mpoexxg  6419  fmpoco  6425  df1st2  6428  df2nd2  6429  1stconst  6430  2ndconst  6431  dfmpo  6432  fo2ndf  6436  f1o2ndf1  6437  xporderlem  6440  cnvoprab  6443  f1od2  6444  suppval1  6452  cnvimadfsn  6458  suppimacnvfn  6459  brtpos2  6495  reldmtpos  6497  dmtpos  6500  rntpos  6501  ovtposg  6503  dftpos3  6506  dftpos4  6507  tpostpos  6508  tpossym  6520  tfrlem3  6555  tfrlem5  6558  tfrlem8  6562  tfrlemisucfn  6568  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemibex  6573  tfrlemi14d  6577  tfrexlem  6578  tfr1onlem3  6582  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  tfrcl  6608  rdgtfr  6618  rdgruledefgg  6619  rdgivallem  6625  rdgon  6630  rdg0g  6632  frec0g  6641  frecabex  6642  frecabcl  6643  frectfr  6644  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  oafnex  6690  sucinc  6691  fnoa  6693  oaexg  6694  omfnex  6695  fnom  6696  omexg  6697  fnoei  6698  oeiexg  6699  oeiv  6702  oacl  6706  omcl  6707  oeicl  6708  oav2  6709  nnsucelsuc  6737  nnsucuniel  6741  ercnv  6801  iserd  6806  eqerlem  6811  eqer  6812  ecdmn0m  6824  erth  6826  qsss  6841  ecid  6845  ecidg  6846  qsid  6847  iinerm  6854  qsel  6859  erovlem  6874  ecopovsym  6878  ecopover  6880  th3qlem2  6885  mapprc  6899  fnmap  6902  fnpm  6903  mapdm0  6910  mapval2  6925  mapsnd  6936  mapsn  6938  mapsncnv  6943  mapsnf1o2  6944  ixpconstg  6955  ixpprc  6967  ixpin  6971  ixpiinm  6972  ixpssmap2g  6975  ixpssmapg  6976  elixpsn  6983  ixpsnf1o  6984  bren  6996  brdomg  6998  domen  7001  domeng  7002  idssen  7029  domssr  7030  ener  7032  domtr  7038  ensn1g  7050  en1  7052  en1bg  7053  fundmen  7060  fundmeng  7061  mapsnend  7065  mapsnen  7066  fiprc  7070  unen  7071  rex2dom  7076  en2m  7079  dom1o  7082  xpsnen  7085  xpsneng  7086  xpcomco  7090  xpcomeng  7092  xpassen  7094  xpdom2  7095  xpdom2g  7096  pw2f1odc  7101  xpf1o  7110  mapen  7112  mapxpen  7114  xpmapenlem  7115  mapunen  7117  ssenen  7118  phplem4  7122  phplem3g  7123  nneneq  7124  php5  7125  phpm  7133  findcard  7158  findcard2  7159  findcard2s  7160  isinfinf  7167  ac6sfi  7168  exmidpw  7181  exmidpweq  7182  exmidpw2en  7185  unfidisj  7195  fiintim  7204  xpfi  7205  fisseneq  7208  ssfirab  7210  mapfi  7227  snexxph  7233  fidcenumlemr  7238  sbthlemi10  7249  isbth  7250  ssfii  7274  fi0  7275  fiss  7277  cnvinfex  7322  eqinfti  7324  infvalti  7326  infglbti  7329  infmoti  7332  ordiso2  7339  djuf1olem  7357  djuss  7374  ctm  7413  ctssdccl  7415  ctssdclemr  7416  finomni  7444  exmidomni  7446  fodjuomnilemdc  7448  nninfwlpoimlemginf  7480  pm54.43  7500  pr2cv1  7505  exmidfodomrlemim  7517  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  finacn  7524  acfun  7527  ccfunen  7594  cc2lem  7596  cc3  7598  acnccim  7602  indpi  7673  dfplpq2  7685  enq0sym  7763  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nqnq0  7772  mulnnnq0  7781  nqprm  7873  nqprrnd  7874  nqprdisj  7875  nqprloc  7876  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemrl  7904  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  ltnqpr  7924  ltnqpri  7925  archpr  7974  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlem2  7991  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemopu  8030  suplocexprlemmu  8049  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  cnm  8163  ltresr  8170  peano1nnnn  8183  peano2nnnn  8184  axcnre  8212  axpre-apti  8216  renfdisj  8349  dfinfre  9247  1nn  9265  peano2nn  9266  indstr  9943  cnref1o  10001  ioof  10323  fzpr  10433  frec2uzrand  10791  frec2uzf1od  10792  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  frecfzennn  10812  seqp1g  10852  seqclg  10858  seqf1og  10907  seqfeq4g  10917  ser3le  10923  hashinfom  11166  hashunlem  11193  hashun  11194  hashxp  11216  hashmap  11217  hashfibclem  11231  hashfacen  11233  zfz1isolem1  11237  zfz1iso  11238  fundm2domnop0  11245  wrdexb  11261  fnpfx  11394  cats1un  11438  wrdind  11439  wrd2ind  11440  shftfvalg  11528  ovshftex  11529  shftfibg  11530  shftfval  11531  shftfib  11533  shftfn  11534  2shfti  11541  shftvalg  11546  shftval4g  11547  maxabslemval  11918  fimaxre2  11937  xrmaxiflemval  11960  fclim  12004  climshft  12014  zsumdc  12095  fsum3  12098  fsum2dlemstep  12145  fsumcnv  12148  fisumcom2  12149  fisum0diag2  12158  fsumconst  12165  modfsummodlemstep  12168  fsumabs  12176  fsumrelem  12182  fsumiun  12188  ntrivcvgap  12259  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  fprodmodd  12352  nninfct  12762  algrf  12767  qredeu  12819  isprm2  12839  prmind2  12842  4sqlemafi  13118  4sqlem12  13125  ballotfilemcdc  13167  ballotfilemsf1o  13201  ballotfilem7  13223  ennnfonelemex  13249  ennnfonelemrn  13254  exmidunben  13261  ctinfom  13263  ctinf  13265  qnnen  13266  enctlem  13267  ctiunctlemfo  13274  slotslfn  13322  setscomd  13337  restfn  13540  elrest  13543  ptex  13561  prdsvallem  13564  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfnlemg  13578  fnpr2ob  13604  ismgm  13620  plusffng  13628  fn0g  13638  fngsum  13651  gsumsplit1r  13661  gsumprval  13662  issgrp  13666  ismnddef  13679  gsumfzz  13750  gsumfzcl  13754  mulgnngsum  13880  subgintm  13951  releqgg  13973  eqgex  13974  eqgfval  13975  eqgval  13976  isghm  13996  gfsumval  14102  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdsbas  14118  fnmgp  14161  isrng  14173  isring  14243  ringn0  14303  opprrngbg  14321  opprsubgg  14328  opprunitd  14355  dfrhm2  14399  rhmex  14402  opprsubrngg  14457  subrngintm  14458  subrngpropd  14462  subrgpropd  14499  isdomn  14516  opprdomnbg  14521  scaffng  14583  rmodislmodlem  14624  rmodislmod  14625  lssex  14628  lsssn0  14644  lss1d  14657  lssintclm  14658  ellspsn  14691  rlmfn  14727  isridl  14778  blfn  14825  mopnset  14826  metuex  14829  znval  14910  znleval  14927  psrval  14940  fnpsr  14941  mplvalcoe  14971  fnmpl  14974  bastg  15052  distop  15076  topnex  15077  epttop  15081  tgrest  15160  resttopon  15162  restco  15165  cnrest2  15227  cnptopresti  15229  cnptoprest  15230  cnptoprest2  15231  txuni2  15247  txbas  15249  eltx  15250  txcnp  15262  txcnmpt  15264  txrest  15267  txdis1cn  15269  txlm  15270  cnmpt1st  15279  cnmpt2nd  15280  txhmeo  15310  txswaphmeolem  15311  xmetec  15428  metrest  15497  reldvg  15670  dvfgg  15679  dvcj  15700  dvmptfsum  15716  elply2  15726  pilem3  15774  lgsquadlem1  16076  lgsquadlem2  16077  upgrex  16224  upgr1een  16245  umgredg  16266  umgredgnlp  16273  usgredgreu  16337  uspgredg2vtxeu  16339  ushgredgedg  16347  ushgredgedgloop  16349  griedg0ssusgr  16372  uhgrspansubgrlem  16397  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlk1walkdom  16480  eulerpathum  16602  depindlem1  16627  bdcvv  16753  bdsnss  16769  bdop  16771  bj-vprc  16792  bdinex1g  16797  bdssexg  16800  bj-inex  16803  bj-zfpair2  16806  bj-uniexg  16814  bdunexb  16816  bj-unexg  16817  bj-indint  16827  bj-ssom  16832  bj-om  16833  bj-2inf  16834  bj-bdfindis  16843  bj-nn0suc0  16846  bj-nnelirr  16849  bj-inf2vnlem1  16866  bj-inf2vnlem2  16867  bj-omex2  16873  bj-nn0sucALT  16874  bj-findis  16875  ss1oel2o  16887  domomsubct  16901  pw1nct  16903  nninfsellemeq  16918  exmidsbthrlem  16928