Theorem vex 2766

Description: All setvar variables are sets (see isset 2769). 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 1715	. 2 |- x = x
2		df-v 2765	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2307	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 146	1 |- x e. _V

Syntax hints:   e. wcel 2167   _Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elv  2767  elvd  2768  isset  2769  eqvisset  2773  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rabab  2784  sbhypf  2813  ceqex  2891  ralab  2924  rexab  2926  mo2icl  2943  reu8  2960  csbvarg  3112  csbiebg  3127  sbcnestgf  3136  sbnfc2  3145  ddifnel  3295  ddifstab  3296  csbing  3371  unssdif  3399  unssin  3403  inssun  3404  invdif  3406  vn0  3462  vn0m  3463  eqv  3471  abvor0dc  3475  sbss  3559  velpw  3613  elpwg  3614  velsn  3640  vsnid  3655  exsnrex  3665  dftp2  3672  prmg  3744  prnzg  3747  snssgOLD  3759  difprsnss  3761  sneqrg  3793  preq12bg  3804  pwprss  3836  pwtpss  3837  pwv  3839  unipr  3854  uniprg  3855  unisng  3857  elintg  3883  elintrabg  3888  intss1  3890  ssint  3891  intmin  3895  intss  3896  intssunim  3897  intmin4  3903  intab  3904  intun  3906  intpr  3907  intprg  3908  uniintsnr  3911  iinconstm  3926  iuniin  3927  iinss1  3929  dfiin2g  3950  dfiunv2  3953  ssiinf  3967  iinss  3969  iinss2  3970  0iin  3976  iinab  3979  iundif2ss  3983  iindif2m  3985  iinin2m  3986  iinuniss  4000  sspwuni  4002  pwpwab  4005  iinpw  4008  iunpwss  4009  brab1  4081  csbopabg  4112  mptv  4131  trint  4147  vnex  4165  inex1g  4170  ssexg  4173  inteximm  4183  inuni  4189  repizf2  4196  axpweq  4205  bnd2  4207  pwuni  4226  exmidundif  4240  exmidundifim  4241  zfpair2  4244  rext  4249  sspwb  4250  unipw  4251  ssextss  4254  euabex  4259  mss  4260  exss  4261  opth  4271  opthg  4272  copsexg  4278  copsex4g  4281  moop2  4285  euotd  4288  opabid  4291  elopab  4293  opelopabsbALT  4294  opelopabsb  4295  opabm  4316  pwin  4318  pwunss  4319  epelg  4326  epel  4328  pofun  4348  epse  4378  tron  4418  sucel  4446  suctr  4457  vuniex  4474  uniexg  4475  unexb  4478  snnex  4484  pwnex  4485  uniuni  4487  eusvnf  4489  eusvnfb  4490  iunpw  4516  unon  4548  ordunisuc2r  4551  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsucunielexmid  4568  elirr  4578  en2lp  4591  dtruex  4596  onintexmid  4610  reg3exmidlemwe  4616  dcextest  4618  finds  4637  finds2  4638  elomssom  4642  limom  4651  0nelxp  4692  opelxp  4694  opeliunxp  4719  elvv  4726  elvvv  4727  elvvuni  4728  xpsspw  4776  relopabiv  4790  relopabi  4792  opabid2  4798  difopab  4800  xpiindim  4804  raliunxp  4808  rexiunxp  4809  ralxpf  4813  rexxpf  4814  relop  4817  cnvco  4852  dfrn2  4855  dfdm4  4859  dmss  4866  dmin  4875  dmiun  4876  dmuni  4877  dm0  4881  dmi  4882  reldm0  4885  elreldm  4893  elrnmpt1  4918  dmrnssfld  4930  dmcoss  4936  dmcosseq  4938  opelresg  4954  resieq  4957  dmres  4968  elres  4983  relssres  4985  resopab  4991  resiexg  4992  iss  4993  dfres2  4999  restidsing  5003  dfima2  5012  imadmrn  5020  imai  5026  csbima12g  5031  elimasng  5038  args  5039  epini  5041  iniseg  5042  dfse2  5043  exse2  5044  cotr  5052  issref  5053  cnvsym  5054  intasym  5055  asymref  5056  intirr  5057  brcodir  5058  codir  5059  qfto  5060  poirr2  5063  cnvopab  5072  cnv0  5074  cnvi  5075  cnvdif  5077  rniun  5081  dminss  5085  imainss  5086  inimasn  5088  xpmlem  5091  dmxpss  5101  rnxpid  5105  ssrnres  5113  rninxp  5114  dminxp  5115  cnvcnv3  5120  dfrel2  5121  dmsnm  5136  dmsnopg  5142  cnvcnvsn  5147  dmsnsnsng  5148  cnvsng  5156  elxp4  5158  elxp5  5159  cnvresima  5160  dfco2  5170  dfco2a  5171  cores  5174  resco  5175  imaco  5176  rnco  5177  coiun  5180  co02  5184  coi1  5186  coass  5189  relssdmrn  5191  unielrel  5198  ressn  5211  cnviinm  5212  cnvpom  5213  cnvsom  5214  uniabio  5230  iotaval  5231  iotass  5237  sniota  5250  csbiotag  5252  dffun2  5269  dffun7  5286  dffun8  5287  dffun9  5288  funopg  5293  funssres  5301  funun  5303  funcnvsn  5304  funinsn  5308  funcnv2  5319  funcnv  5320  funcnv3  5321  funcnveq  5322  fun2cnv  5323  funcnvuni  5328  imadif  5339  funimaexglem  5342  isarep1  5345  2elresin  5372  fnres  5377  fcnvres  5444  fconstg  5457  fun11iun  5528  f1osng  5548  dffv3g  5557  fvssunirng  5576  sefvex  5582  fv3  5584  fvres  5585  nfunsn  5596  funimass4  5614  ssimaexg  5626  dmfco  5632  fvopab6  5661  fndmdif  5670  fvelrn  5696  dffo4  5713  f1ompt  5716  fmptco  5731  fsn  5737  fsng  5738  dfmpt  5742  dfmptg  5744  fnressn  5751  fressnfv  5752  fvsng  5761  resfunexg  5786  funfvima3  5799  idref  5806  abrexco  5809  imaiun  5810  dff13  5818  foeqcnvco  5840  f1eqcocnv  5841  fliftcnv  5845  isocnv2  5862  isoini  5868  isose  5871  riotav  5886  csbriotag  5893  acexmidlem2  5922  oprabid  5957  csbov123g  5964  0neqopab  5971  brabvv  5972  dfoprab2  5973  rnoprab  6009  eloprabga  6013  mpov  6016  f1opw  6134  opabex3d  6187  opabex3  6188  ofmres  6202  uchoice  6204  op1stg  6217  op2ndg  6218  1stval2  6222  2ndval2  6223  fo1st  6224  fo2nd  6225  f1stres  6226  f2ndres  6227  fo1stresm  6228  fo2ndresm  6229  xp1st  6232  xp2nd  6233  releldm2  6252  reldm  6253  sbcopeq1a  6254  csbopeq1a  6255  dfoprab3  6258  eloprabi  6263  mpomptsx  6264  dmmpossx  6266  fmpox  6267  mpofvex  6272  mpoexxg  6277  fmpoco  6283  df1st2  6286  df2nd2  6287  1stconst  6288  2ndconst  6289  dfmpo  6290  fo2ndf  6294  f1o2ndf1  6295  xporderlem  6298  cnvoprab  6301  f1od2  6302  brtpos2  6318  reldmtpos  6320  dmtpos  6323  rntpos  6324  ovtposg  6326  dftpos3  6329  dftpos4  6330  tpostpos  6331  tpossym  6343  tfrlem3  6378  tfrlem5  6381  tfrlem8  6385  tfrlemisucfn  6391  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemibex  6396  tfrlemi14d  6400  tfrexlem  6401  tfr1onlem3  6405  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemres  6429  tfrcl  6431  rdgtfr  6441  rdgruledefgg  6442  rdgivallem  6448  rdgon  6453  rdg0g  6455  frec0g  6464  frecabex  6465  frecabcl  6466  frectfr  6467  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  oafnex  6511  sucinc  6512  fnoa  6514  oaexg  6515  omfnex  6516  fnom  6517  omexg  6518  fnoei  6519  oeiexg  6520  oeiv  6523  oacl  6527  omcl  6528  oeicl  6529  oav2  6530  nnsucelsuc  6558  nnsucuniel  6562  ercnv  6622  iserd  6627  eqerlem  6632  eqer  6633  ecdmn0m  6645  erth  6647  qsss  6662  ecid  6666  ecidg  6667  qsid  6668  iinerm  6675  qsel  6680  erovlem  6695  ecopovsym  6699  ecopover  6701  th3qlem2  6706  mapprc  6720  fnmap  6723  fnpm  6724  mapdm0  6731  mapval2  6746  mapsn  6758  mapsncnv  6763  mapsnf1o2  6764  ixpconstg  6775  ixpprc  6787  ixpin  6791  ixpiinm  6792  ixpssmap2g  6795  ixpssmapg  6796  elixpsn  6803  ixpsnf1o  6804  bren  6815  brdomg  6816  domen  6819  domeng  6820  idssen  6845  ener  6847  domtr  6853  ensn1g  6865  en1  6867  en1bg  6868  fundmen  6874  fundmeng  6875  mapsnen  6879  fiprc  6883  unen  6884  xpsnen  6889  xpsneng  6890  xpcomco  6894  xpcomeng  6896  xpassen  6898  xpdom2  6899  xpdom2g  6900  pw2f1odc  6905  xpf1o  6914  mapen  6916  mapxpen  6918  xpmapenlem  6919  ssenen  6921  phplem4  6925  phplem3g  6926  nneneq  6927  php5  6928  phpm  6935  findcard  6958  findcard2  6959  findcard2s  6960  isinfinf  6967  ac6sfi  6968  exmidpw  6978  exmidpweq  6979  exmidpw2en  6982  unfidisj  6992  fiintim  7001  xpfi  7002  fisseneq  7004  ssfirab  7006  snexxph  7025  fidcenumlemr  7030  sbthlemi10  7041  isbth  7042  ssfii  7049  fi0  7050  fiss  7052  cnvinfex  7093  eqinfti  7095  infvalti  7097  infglbti  7100  infmoti  7103  ordiso2  7110  djuf1olem  7128  djuss  7145  ctm  7184  ctssdccl  7186  ctssdclemr  7187  finomni  7215  exmidomni  7217  fodjuomnilemdc  7219  nninfwlpoimlemginf  7251  pm54.43  7269  exmidfodomrlemim  7280  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  finacn  7287  acfun  7290  ccfunen  7347  cc2lem  7349  cc3  7351  acnccim  7355  indpi  7426  dfplpq2  7438  enq0sym  7516  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  nqnq0  7525  mulnnnq0  7534  nqprm  7626  nqprrnd  7627  nqprdisj  7628  nqprloc  7629  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemrl  7657  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  ltnqpr  7677  ltnqpri  7678  archpr  7727  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlem2  7744  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemopu  7783  suplocexprlemmu  7802  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  cnm  7916  ltresr  7923  peano1nnnn  7936  peano2nnnn  7937  axcnre  7965  axpre-apti  7969  renfdisj  8103  dfinfre  9000  1nn  9018  peano2nn  9019  indstr  9684  cnref1o  9742  ioof  10063  fzpr  10169  frec2uzrand  10514  frec2uzf1od  10515  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  frecfzennn  10535  seqp1g  10575  seqclg  10581  seqf1og  10630  seqfeq4g  10640  ser3le  10646  hashinfom  10887  hashunlem  10913  hashun  10914  hashxp  10935  hashfacen  10945  zfz1isolem1  10949  zfz1iso  10950  wrdexb  10964  shftfvalg  11000  ovshftex  11001  shftfibg  11002  shftfval  11003  shftfib  11005  shftfn  11006  2shfti  11013  shftvalg  11018  shftval4g  11019  maxabslemval  11390  fimaxre2  11409  xrmaxiflemval  11432  fclim  11476  climshft  11486  zsumdc  11566  fsum3  11569  fsum2dlemstep  11616  fsumcnv  11619  fisumcom2  11620  fisum0diag2  11629  fsumconst  11636  modfsummodlemstep  11639  fsumabs  11647  fsumrelem  11653  fsumiun  11659  ntrivcvgap  11730  fprod2dlemstep  11804  fprodcnv  11807  fprodcom2fi  11808  fprodmodd  11823  nninfct  12233  algrf  12238  qredeu  12290  isprm2  12310  prmind2  12313  4sqlemafi  12589  4sqlem12  12596  ennnfonelemex  12656  ennnfonelemrn  12661  exmidunben  12668  ctinfom  12670  ctinf  12672  qnnen  12673  enctlem  12674  ctiunctlemfo  12681  slotslfn  12729  setscomd  12744  restfn  12945  elrest  12948  ptex  12966  prdsex  12971  prdsvallem  12974  prdsval  12975  prdsbaslemss  12976  prdsbas  12978  imasex  13007  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfnlemg  13016  fnpr2ob  13042  ismgm  13059  plusffng  13067  fn0g  13077  fngsum  13090  gsumsplit1r  13100  gsumprval  13101  issgrp  13105  ismnddef  13120  gsumfzz  13197  gsumfzcl  13201  mulgnngsum  13333  subgintm  13404  releqgg  13426  eqgex  13427  eqgfval  13428  eqgval  13429  isghm  13449  fnmgp  13554  isrng  13566  isring  13632  ringn0  13692  opprrngbg  13710  opprsubgg  13716  opprunitd  13742  dfrhm2  13786  rhmex  13789  opprsubrngg  13843  subrngintm  13844  subrngpropd  13848  subrgpropd  13885  isdomn  13901  opprdomnbg  13906  scaffng  13941  rmodislmodlem  13982  rmodislmod  13983  lssex  13986  lsssn0  14002  lss1d  14015  lssintclm  14016  ellspsn  14049  rlmfn  14085  isridl  14136  blfn  14183  mopnset  14184  metuex  14187  znval  14268  znleval  14285  psrval  14296  fnpsr  14297  bastg  14381  distop  14405  topnex  14406  epttop  14410  tgrest  14489  resttopon  14491  restco  14494  cnrest2  14556  cnptopresti  14558  cnptoprest  14559  cnptoprest2  14560  txuni2  14576  txbas  14578  eltx  14579  txcnp  14591  txcnmpt  14593  txrest  14596  txdis1cn  14598  txlm  14599  cnmpt1st  14608  cnmpt2nd  14609  txhmeo  14639  txswaphmeolem  14640  xmetec  14757  metrest  14826  reldvg  14999  dvfgg  15008  dvcj  15029  dvmptfsum  15045  elply2  15055  pilem3  15103  lgsquadlem1  15402  lgsquadlem2  15403  bdcvv  15587  bdsnss  15603  bdop  15605  bj-vprc  15626  bdinex1g  15631  bdssexg  15634  bj-inex  15637  bj-zfpair2  15640  bj-uniexg  15648  bdunexb  15650  bj-unexg  15651  bj-indint  15661  bj-ssom  15666  bj-om  15667  bj-2inf  15668  bj-bdfindis  15677  bj-nn0suc0  15680  bj-nnelirr  15683  bj-inf2vnlem1  15700  bj-inf2vnlem2  15701  bj-omex2  15707  bj-nn0sucALT  15708  bj-findis  15709  ss1oel2o  15722  domomsubct  15732  pw1nct  15734  nninfsellemeq  15745  exmidsbthrlem  15753