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  3294  ddifstab  3295  csbing  3370  unssdif  3398  unssin  3402  inssun  3403  invdif  3405  vn0  3461  vn0m  3462  eqv  3470  abvor0dc  3474  sbss  3558  velpw  3612  elpwg  3613  velsn  3639  vsnid  3654  exsnrex  3664  dftp2  3671  prmg  3743  prnzg  3746  snssgOLD  3758  difprsnss  3760  sneqrg  3792  preq12bg  3803  pwprss  3835  pwtpss  3836  pwv  3838  unipr  3853  uniprg  3854  unisng  3856  elintg  3882  elintrabg  3887  intss1  3889  ssint  3890  intmin  3894  intss  3895  intssunim  3896  intmin4  3902  intab  3903  intun  3905  intpr  3906  intprg  3907  uniintsnr  3910  iinconstm  3925  iuniin  3926  iinss1  3928  dfiin2g  3949  dfiunv2  3952  ssiinf  3966  iinss  3968  iinss2  3969  0iin  3975  iinab  3978  iundif2ss  3982  iindif2m  3984  iinin2m  3985  iinuniss  3999  sspwuni  4001  pwpwab  4004  iinpw  4007  iunpwss  4008  brab1  4080  csbopabg  4111  mptv  4130  trint  4146  vnex  4164  inex1g  4169  ssexg  4172  inteximm  4182  inuni  4188  repizf2  4195  axpweq  4204  bnd2  4206  pwuni  4225  exmidundif  4239  exmidundifim  4240  zfpair2  4243  rext  4248  sspwb  4249  unipw  4250  ssextss  4253  euabex  4258  mss  4259  exss  4260  opth  4270  opthg  4271  copsexg  4277  copsex4g  4280  moop2  4284  euotd  4287  opabid  4290  elopab  4292  opelopabsbALT  4293  opelopabsb  4294  opabm  4315  pwin  4317  pwunss  4318  epelg  4325  epel  4327  pofun  4347  epse  4377  tron  4417  sucel  4445  suctr  4456  vuniex  4473  uniexg  4474  unexb  4477  snnex  4483  pwnex  4484  uniuni  4486  eusvnf  4488  eusvnfb  4489  iunpw  4515  unon  4547  ordunisuc2r  4550  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  ordsucunielexmid  4567  elirr  4577  en2lp  4590  dtruex  4595  onintexmid  4609  reg3exmidlemwe  4615  dcextest  4617  finds  4636  finds2  4637  elomssom  4641  limom  4650  0nelxp  4691  opelxp  4693  opeliunxp  4718  elvv  4725  elvvv  4726  elvvuni  4727  xpsspw  4775  relopabiv  4789  relopabi  4791  opabid2  4797  difopab  4799  xpiindim  4803  raliunxp  4807  rexiunxp  4808  ralxpf  4812  rexxpf  4813  relop  4816  cnvco  4851  dfrn2  4854  dfdm4  4858  dmss  4865  dmin  4874  dmiun  4875  dmuni  4876  dm0  4880  dmi  4881  reldm0  4884  elreldm  4892  elrnmpt1  4917  dmrnssfld  4929  dmcoss  4935  dmcosseq  4937  opelresg  4953  resieq  4956  dmres  4967  elres  4982  relssres  4984  resopab  4990  resiexg  4991  iss  4992  dfres2  4998  restidsing  5002  dfima2  5011  imadmrn  5019  imai  5025  csbima12g  5030  elimasng  5037  args  5038  epini  5040  iniseg  5041  dfse2  5042  exse2  5043  cotr  5051  issref  5052  cnvsym  5053  intasym  5054  asymref  5055  intirr  5056  brcodir  5057  codir  5058  qfto  5059  poirr2  5062  cnvopab  5071  cnv0  5073  cnvi  5074  cnvdif  5076  rniun  5080  dminss  5084  imainss  5085  inimasn  5087  xpmlem  5090  dmxpss  5100  rnxpid  5104  ssrnres  5112  rninxp  5113  dminxp  5114  cnvcnv3  5119  dfrel2  5120  dmsnm  5135  dmsnopg  5141  cnvcnvsn  5146  dmsnsnsng  5147  cnvsng  5155  elxp4  5157  elxp5  5158  cnvresima  5159  dfco2  5169  dfco2a  5170  cores  5173  resco  5174  imaco  5175  rnco  5176  coiun  5179  co02  5183  coi1  5185  coass  5188  relssdmrn  5190  unielrel  5197  ressn  5210  cnviinm  5211  cnvpom  5212  cnvsom  5213  uniabio  5229  iotaval  5230  iotass  5236  sniota  5249  csbiotag  5251  dffun2  5268  dffun7  5285  dffun8  5286  dffun9  5287  funopg  5292  funssres  5300  funun  5302  funcnvsn  5303  funinsn  5307  funcnv2  5318  funcnv  5319  funcnv3  5320  funcnveq  5321  fun2cnv  5322  funcnvuni  5327  imadif  5338  funimaexglem  5341  isarep1  5344  2elresin  5369  fnres  5374  fcnvres  5441  fconstg  5454  fun11iun  5525  f1osng  5545  dffv3g  5554  fvssunirng  5573  sefvex  5579  fv3  5581  fvres  5582  nfunsn  5593  funimass4  5611  ssimaexg  5623  dmfco  5629  fvopab6  5658  fndmdif  5667  fvelrn  5693  dffo4  5710  f1ompt  5713  fmptco  5728  fsn  5734  fsng  5735  dfmpt  5739  dfmptg  5741  fnressn  5748  fressnfv  5749  fvsng  5758  resfunexg  5783  funfvima3  5796  idref  5803  abrexco  5806  imaiun  5807  dff13  5815  foeqcnvco  5837  f1eqcocnv  5838  fliftcnv  5842  isocnv2  5859  isoini  5865  isose  5868  riotav  5883  csbriotag  5890  acexmidlem2  5919  oprabid  5954  csbov123g  5960  0neqopab  5967  brabvv  5968  dfoprab2  5969  rnoprab  6005  eloprabga  6009  mpov  6012  f1opw  6130  opabex3d  6178  opabex3  6179  ofmres  6193  uchoice  6195  op1stg  6208  op2ndg  6209  1stval2  6213  2ndval2  6214  fo1st  6215  fo2nd  6216  f1stres  6217  f2ndres  6218  fo1stresm  6219  fo2ndresm  6220  xp1st  6223  xp2nd  6224  releldm2  6243  reldm  6244  sbcopeq1a  6245  csbopeq1a  6246  dfoprab3  6249  eloprabi  6254  mpomptsx  6255  dmmpossx  6257  fmpox  6258  mpofvex  6263  mpoexxg  6268  fmpoco  6274  df1st2  6277  df2nd2  6278  1stconst  6279  2ndconst  6280  dfmpo  6281  fo2ndf  6285  f1o2ndf1  6286  xporderlem  6289  cnvoprab  6292  f1od2  6293  brtpos2  6309  reldmtpos  6311  dmtpos  6314  rntpos  6315  ovtposg  6317  dftpos3  6320  dftpos4  6321  tpostpos  6322  tpossym  6334  tfrlem3  6369  tfrlem5  6372  tfrlem8  6376  tfrlemisucfn  6382  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemibex  6387  tfrlemi14d  6391  tfrexlem  6392  tfr1onlem3  6396  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemres  6407  tfri1dALT  6409  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemres  6420  tfrcl  6422  rdgtfr  6432  rdgruledefgg  6433  rdgivallem  6439  rdgon  6444  rdg0g  6446  frec0g  6455  frecabex  6456  frecabcl  6457  frectfr  6458  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecrdg  6466  oafnex  6502  sucinc  6503  fnoa  6505  oaexg  6506  omfnex  6507  fnom  6508  omexg  6509  fnoei  6510  oeiexg  6511  oeiv  6514  oacl  6518  omcl  6519  oeicl  6520  oav2  6521  nnsucelsuc  6549  nnsucuniel  6553  ercnv  6613  iserd  6618  eqerlem  6623  eqer  6624  ecdmn0m  6636  erth  6638  qsss  6653  ecid  6657  ecidg  6658  qsid  6659  iinerm  6666  qsel  6671  erovlem  6686  ecopovsym  6690  ecopover  6692  th3qlem2  6697  mapprc  6711  fnmap  6714  fnpm  6715  mapdm0  6722  mapval2  6737  mapsn  6749  mapsncnv  6754  mapsnf1o2  6755  ixpconstg  6766  ixpprc  6778  ixpin  6782  ixpiinm  6783  ixpssmap2g  6786  ixpssmapg  6787  elixpsn  6794  ixpsnf1o  6795  bren  6806  brdomg  6807  domen  6810  domeng  6811  idssen  6836  ener  6838  domtr  6844  ensn1g  6856  en1  6858  en1bg  6859  fundmen  6865  fundmeng  6866  mapsnen  6870  fiprc  6874  unen  6875  xpsnen  6880  xpsneng  6881  xpcomco  6885  xpcomeng  6887  xpassen  6889  xpdom2  6890  xpdom2g  6891  pw2f1odc  6896  xpf1o  6905  mapen  6907  mapxpen  6909  xpmapenlem  6910  ssenen  6912  phplem4  6916  phplem3g  6917  nneneq  6918  php5  6919  phpm  6926  findcard  6949  findcard2  6950  findcard2s  6951  isinfinf  6958  ac6sfi  6959  exmidpw  6969  exmidpweq  6970  exmidpw2en  6973  unfidisj  6983  fiintim  6992  xpfi  6993  fisseneq  6995  ssfirab  6997  snexxph  7016  fidcenumlemr  7021  sbthlemi10  7032  isbth  7033  ssfii  7040  fi0  7041  fiss  7043  cnvinfex  7084  eqinfti  7086  infvalti  7088  infglbti  7091  infmoti  7094  ordiso2  7101  djuf1olem  7119  djuss  7136  ctm  7175  ctssdccl  7177  ctssdclemr  7178  finomni  7206  exmidomni  7208  fodjuomnilemdc  7210  nninfwlpoimlemginf  7242  pm54.43  7257  exmidfodomrlemim  7268  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  acfun  7274  ccfunen  7331  cc2lem  7333  cc3  7335  indpi  7409  dfplpq2  7421  enq0sym  7499  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  nqnq0  7508  mulnnnq0  7517  nqprm  7609  nqprrnd  7610  nqprdisj  7611  nqprloc  7612  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  ltnqpr  7660  ltnqpri  7661  archpr  7710  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlem2  7727  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemopu  7766  suplocexprlemmu  7785  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  cnm  7899  ltresr  7906  peano1nnnn  7919  peano2nnnn  7920  axcnre  7948  axpre-apti  7952  renfdisj  8086  dfinfre  8983  1nn  9001  peano2nn  9002  indstr  9667  cnref1o  9725  ioof  10046  fzpr  10152  frec2uzrand  10497  frec2uzf1od  10498  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  frecfzennn  10518  seqp1g  10558  seqclg  10564  seqf1og  10613  seqfeq4g  10623  ser3le  10629  hashinfom  10870  hashunlem  10896  hashun  10897  hashxp  10918  hashfacen  10928  zfz1isolem1  10932  zfz1iso  10933  wrdexb  10947  shftfvalg  10983  ovshftex  10984  shftfibg  10985  shftfval  10986  shftfib  10988  shftfn  10989  2shfti  10996  shftvalg  11001  shftval4g  11002  maxabslemval  11373  fimaxre2  11392  xrmaxiflemval  11415  fclim  11459  climshft  11469  zsumdc  11549  fsum3  11552  fsum2dlemstep  11599  fsumcnv  11602  fisumcom2  11603  fisum0diag2  11612  fsumconst  11619  modfsummodlemstep  11622  fsumabs  11630  fsumrelem  11636  fsumiun  11642  ntrivcvgap  11713  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  fprodmodd  11806  nninfct  12208  algrf  12213  qredeu  12265  isprm2  12285  prmind2  12288  4sqlemafi  12564  4sqlem12  12571  ennnfonelemex  12631  ennnfonelemrn  12636  exmidunben  12643  ctinfom  12645  ctinf  12647  qnnen  12648  enctlem  12649  ctiunctlemfo  12656  slotslfn  12704  setscomd  12719  restfn  12914  elrest  12917  ptex  12935  prdsex  12940  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfnlemg  12957  fnpr2ob  12983  ismgm  13000  plusffng  13008  fn0g  13018  fngsum  13031  gsumsplit1r  13041  gsumprval  13042  issgrp  13046  ismnddef  13059  gsumfzz  13127  gsumfzcl  13131  mulgnngsum  13257  subgintm  13328  releqgg  13350  eqgex  13351  eqgfval  13352  eqgval  13353  isghm  13373  fnmgp  13478  isrng  13490  isring  13556  ringn0  13616  opprrngbg  13634  opprsubgg  13640  opprunitd  13666  dfrhm2  13710  rhmex  13713  opprsubrngg  13767  subrngintm  13768  subrngpropd  13772  subrgpropd  13809  isdomn  13825  opprdomnbg  13830  scaffng  13865  rmodislmodlem  13906  rmodislmod  13907  lssex  13910  lsssn0  13926  lss1d  13939  lssintclm  13940  ellspsn  13973  rlmfn  14009  isridl  14060  blfn  14107  mopnset  14108  metuex  14111  znval  14192  znleval  14209  psrval  14220  fnpsr  14221  bastg  14297  distop  14321  topnex  14322  epttop  14326  tgrest  14405  resttopon  14407  restco  14410  cnrest2  14472  cnptopresti  14474  cnptoprest  14475  cnptoprest2  14476  txuni2  14492  txbas  14494  eltx  14495  txcnp  14507  txcnmpt  14509  txrest  14512  txdis1cn  14514  txlm  14515  cnmpt1st  14524  cnmpt2nd  14525  txhmeo  14555  txswaphmeolem  14556  xmetec  14673  metrest  14742  reldvg  14915  dvfgg  14924  dvcj  14945  dvmptfsum  14961  elply2  14971  pilem3  15019  lgsquadlem1  15318  lgsquadlem2  15319  bdcvv  15503  bdsnss  15519  bdop  15521  bj-vprc  15542  bdinex1g  15547  bdssexg  15550  bj-inex  15553  bj-zfpair2  15556  bj-uniexg  15564  bdunexb  15566  bj-unexg  15567  bj-indint  15577  bj-ssom  15582  bj-om  15583  bj-2inf  15584  bj-bdfindis  15593  bj-nn0suc0  15596  bj-nnelirr  15599  bj-inf2vnlem1  15616  bj-inf2vnlem2  15617  bj-omex2  15623  bj-nn0sucALT  15624  bj-findis  15625  ss1oel2o  15638  pw1nct  15647  nninfsellemeq  15658  exmidsbthrlem  15666