Theorem vex 2802

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

Syntax hints:   e. wcel 2200   _Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elv  2803  elvd  2804  el2v  2805  isset  2806  eqvisset  2810  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rabab  2821  sbhypf  2850  ceqex  2930  ralab  2963  rexab  2965  mo2icl  2982  reu8  2999  csbvarg  3152  csbiebg  3167  sbcnestgf  3176  sbnfc2  3185  ddifnel  3335  ddifstab  3336  csbing  3411  unssdif  3439  unssin  3443  inssun  3444  invdif  3446  vn0  3502  vn0m  3503  eqv  3511  abvor0dc  3515  sbss  3599  velpw  3656  elpwg  3657  velsn  3683  vsnid  3698  exsnrex  3708  dftp2  3715  prmg  3789  prnzg  3792  snssgOLD  3804  difprsnss  3806  sneqrg  3840  preq12bg  3851  pwprss  3884  pwtpss  3885  pwv  3887  unipr  3902  uniprg  3903  unisng  3905  elintg  3931  elintrabg  3936  intss1  3938  ssint  3939  intmin  3943  intss  3944  intssunim  3945  intmin4  3951  intab  3952  intun  3954  intpr  3955  intprg  3956  uniintsnr  3959  iinconstm  3974  iuniin  3975  iinss1  3977  dfiin2g  3998  dfiunv2  4001  ssiinf  4015  iinss  4017  iinss2  4018  0iin  4024  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iinuniss  4048  sspwuni  4050  pwpwab  4053  iinpw  4056  iunpwss  4057  brab1  4131  csbopabg  4162  mptv  4181  trint  4197  vnex  4215  inex1g  4220  ssexg  4223  inteximm  4233  inuni  4239  repizf2  4246  axpweq  4255  bnd2  4257  pwuni  4276  exmidundif  4290  exmidundifim  4291  zfpair2  4294  rext  4301  sspwb  4302  unipw  4303  ssextss  4306  euabex  4311  mss  4312  exss  4313  opth  4323  opthg  4324  copsexg  4330  copsex4g  4333  moop2  4338  euotd  4341  opabid  4344  elopab  4346  opelopabsbALT  4347  opelopabsb  4348  opabm  4369  pwin  4373  pwunss  4374  epelg  4381  epel  4383  pofun  4403  epse  4433  tron  4473  sucel  4501  suctr  4512  vuniex  4529  uniexg  4530  unexb  4533  snnex  4539  pwnex  4540  uniuni  4542  eusvnf  4544  eusvnfb  4545  iunpw  4571  unon  4603  ordunisuc2r  4606  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsucunielexmid  4623  elirr  4633  en2lp  4646  dtruex  4651  onintexmid  4665  reg3exmidlemwe  4671  dcextest  4673  finds  4692  finds2  4693  elomssom  4697  limom  4706  0nelxp  4747  opelxp  4749  opeliunxp  4774  elvv  4781  elvvv  4782  elvvuni  4783  xpsspw  4831  relopabiv  4845  relopabi  4847  opabid2  4853  difopab  4855  xpiindim  4859  raliunxp  4863  rexiunxp  4864  ralxpf  4868  rexxpf  4869  relop  4872  cnvco  4907  dfrn2  4910  dfdm4  4915  dmss  4922  dmin  4931  dmiun  4932  dmuni  4933  dm0  4937  dmi  4938  reldm0  4941  reldmm  4942  elreldm  4950  elrnmpt1  4975  dmrnssfld  4987  dmcoss  4994  dmcosseq  4996  opelresg  5012  resieq  5015  dmres  5026  elres  5041  relssres  5043  resopab  5049  resiexg  5050  iss  5051  dfres2  5057  restidsing  5061  dfima2  5070  imadmrn  5078  imai  5084  csbima12g  5089  elimasng  5096  args  5097  epini  5099  iniseg  5100  dfse2  5101  exse2  5102  cotr  5110  issref  5111  cnvsym  5112  intasym  5113  asymref  5114  intirr  5115  brcodir  5116  codir  5117  qfto  5118  poirr2  5121  cnvopab  5130  cnv0  5132  cnvi  5133  cnvdif  5135  rniun  5139  dminss  5143  imainss  5144  inimasn  5146  xpmlem  5149  dmxpss  5159  rnxpid  5163  ssrnres  5171  rninxp  5172  dminxp  5173  cnvcnv3  5178  dfrel2  5179  dmsnm  5194  dmsnopg  5200  cnvcnvsn  5205  dmsnsnsng  5206  cnvsng  5214  elxp4  5216  elxp5  5217  cnvresima  5218  dfco2  5228  dfco2a  5229  cores  5232  resco  5233  imaco  5234  rnco  5235  coiun  5238  co02  5242  coi1  5244  coass  5247  relssdmrn  5249  unielrel  5256  ressn  5269  cnviinm  5270  cnvpom  5271  cnvsom  5272  uniabio  5289  iotaval  5290  iotass  5296  sniota  5309  csbiotag  5311  dffun2  5328  dffun7  5345  dffun8  5346  dffun9  5347  funopg  5352  funssres  5360  funun  5362  funcnvsn  5366  funinsn  5370  funcnv2  5381  funcnv  5382  funcnv3  5383  funcnveq  5384  fun2cnv  5385  funcnvuni  5390  imadif  5401  funimaexglem  5404  isarep1  5407  2elresin  5434  fnres  5440  fcnvres  5511  fconstg  5524  fun11iun  5595  f1osng  5616  dffv3g  5625  fvssunirng  5644  sefvex  5650  fv3  5652  fvres  5653  nfunsn  5666  funimass4  5686  ssimaexg  5698  dmfco  5704  fvopab6  5733  fndmdif  5742  fvelrn  5768  dffo4  5785  f1ompt  5788  fmptco  5803  fsn  5809  fsng  5810  dfmpt  5814  dfmptg  5816  funopsn  5819  funop  5820  funopdmsn  5823  fnressn  5829  fressnfv  5830  fvsng  5839  resfunexg  5864  funfvima3  5877  idref  5886  abrexco  5889  imaiun  5890  dff13  5898  foeqcnvco  5920  f1eqcocnv  5921  fliftcnv  5925  isocnv2  5942  isoini  5948  isose  5951  riotav  5966  csbriotag  5974  acexmidlem2  6004  oprabid  6039  csbov123g  6046  0neqopab  6055  brabvv  6056  dfoprab2  6057  rnoprab  6093  eloprabga  6097  mpov  6100  f1opw  6219  opabex3d  6272  opabex3  6273  ofmres  6287  uchoice  6289  op1stg  6302  op2ndg  6303  1stval2  6307  2ndval2  6308  fo1st  6309  fo2nd  6310  f1stres  6311  f2ndres  6312  fo1stresm  6313  fo2ndresm  6314  xp1st  6317  xp2nd  6318  releldm2  6337  reldm  6338  sbcopeq1a  6339  csbopeq1a  6340  dfoprab3  6343  eloprabi  6348  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  mpoexxg  6362  fmpoco  6368  df1st2  6371  df2nd2  6372  1stconst  6373  2ndconst  6374  dfmpo  6375  fo2ndf  6379  f1o2ndf1  6380  xporderlem  6383  cnvoprab  6386  f1od2  6387  brtpos2  6403  reldmtpos  6405  dmtpos  6408  rntpos  6409  ovtposg  6411  dftpos3  6414  dftpos4  6415  tpostpos  6416  tpossym  6428  tfrlem3  6463  tfrlem5  6466  tfrlem8  6470  tfrlemisucfn  6476  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemibex  6481  tfrlemi14d  6485  tfrexlem  6486  tfr1onlem3  6490  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  tfrcl  6516  rdgtfr  6526  rdgruledefgg  6527  rdgivallem  6533  rdgon  6538  rdg0g  6540  frec0g  6549  frecabex  6550  frecabcl  6551  frectfr  6552  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  oafnex  6598  sucinc  6599  fnoa  6601  oaexg  6602  omfnex  6603  fnom  6604  omexg  6605  fnoei  6606  oeiexg  6607  oeiv  6610  oacl  6614  omcl  6615  oeicl  6616  oav2  6617  nnsucelsuc  6645  nnsucuniel  6649  ercnv  6709  iserd  6714  eqerlem  6719  eqer  6720  ecdmn0m  6732  erth  6734  qsss  6749  ecid  6753  ecidg  6754  qsid  6755  iinerm  6762  qsel  6767  erovlem  6782  ecopovsym  6786  ecopover  6788  th3qlem2  6793  mapprc  6807  fnmap  6810  fnpm  6811  mapdm0  6818  mapval2  6833  mapsn  6845  mapsncnv  6850  mapsnf1o2  6851  ixpconstg  6862  ixpprc  6874  ixpin  6878  ixpiinm  6879  ixpssmap2g  6882  ixpssmapg  6883  elixpsn  6890  ixpsnf1o  6891  bren  6903  brdomg  6905  domen  6908  domeng  6909  idssen  6936  domssr  6937  ener  6939  domtr  6945  ensn1g  6957  en1  6959  en1bg  6960  fundmen  6967  fundmeng  6968  mapsnen  6972  fiprc  6976  unen  6977  rex2dom  6979  en2m  6982  dom1o  6985  xpsnen  6988  xpsneng  6989  xpcomco  6993  xpcomeng  6995  xpassen  6997  xpdom2  6998  xpdom2g  6999  pw2f1odc  7004  xpf1o  7013  mapen  7015  mapxpen  7017  xpmapenlem  7018  ssenen  7020  phplem4  7024  phplem3g  7025  nneneq  7026  php5  7027  phpm  7035  findcard  7058  findcard2  7059  findcard2s  7060  isinfinf  7067  ac6sfi  7068  exmidpw  7081  exmidpweq  7082  exmidpw2en  7085  unfidisj  7095  fiintim  7104  xpfi  7105  fisseneq  7107  ssfirab  7109  snexxph  7128  fidcenumlemr  7133  sbthlemi10  7144  isbth  7145  ssfii  7152  fi0  7153  fiss  7155  cnvinfex  7196  eqinfti  7198  infvalti  7200  infglbti  7203  infmoti  7206  ordiso2  7213  djuf1olem  7231  djuss  7248  ctm  7287  ctssdccl  7289  ctssdclemr  7290  finomni  7318  exmidomni  7320  fodjuomnilemdc  7322  nninfwlpoimlemginf  7354  pm54.43  7374  pr2cv1  7379  exmidfodomrlemim  7390  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  finacn  7397  acfun  7400  ccfunen  7461  cc2lem  7463  cc3  7465  acnccim  7469  indpi  7540  dfplpq2  7552  enq0sym  7630  enq0ref  7631  enq0tr  7632  nqnq0pi  7636  nqnq0  7639  mulnnnq0  7648  nqprm  7740  nqprrnd  7741  nqprdisj  7742  nqprloc  7743  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  ltnqpr  7791  ltnqpri  7792  archpr  7841  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlem2  7858  caucvgprlemladdfu  7875  caucvgprlem2  7878  caucvgprprlemopu  7897  suplocexprlemmu  7916  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  cnm  8030  ltresr  8037  peano1nnnn  8050  peano2nnnn  8051  axcnre  8079  axpre-apti  8083  renfdisj  8217  dfinfre  9114  1nn  9132  peano2nn  9133  indstr  9800  cnref1o  9858  ioof  10179  fzpr  10285  frec2uzrand  10639  frec2uzf1od  10640  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  frecfzennn  10660  seqp1g  10700  seqclg  10706  seqf1og  10755  seqfeq4g  10765  ser3le  10771  hashinfom  11012  hashunlem  11038  hashun  11039  hashxp  11061  hashfacen  11071  zfz1isolem1  11075  zfz1iso  11076  fundm2domnop0  11080  wrdexb  11096  fnpfx  11224  cats1un  11268  wrdind  11269  wrd2ind  11270  shftfvalg  11344  ovshftex  11345  shftfibg  11346  shftfval  11347  shftfib  11349  shftfn  11350  2shfti  11357  shftvalg  11362  shftval4g  11363  maxabslemval  11734  fimaxre2  11753  xrmaxiflemval  11776  fclim  11820  climshft  11830  zsumdc  11910  fsum3  11913  fsum2dlemstep  11960  fsumcnv  11963  fisumcom2  11964  fisum0diag2  11973  fsumconst  11980  modfsummodlemstep  11983  fsumabs  11991  fsumrelem  11997  fsumiun  12003  ntrivcvgap  12074  fprod2dlemstep  12148  fprodcnv  12151  fprodcom2fi  12152  fprodmodd  12167  nninfct  12577  algrf  12582  qredeu  12634  isprm2  12654  prmind2  12657  4sqlemafi  12933  4sqlem12  12940  ennnfonelemex  13000  ennnfonelemrn  13005  exmidunben  13012  ctinfom  13014  ctinf  13016  qnnen  13017  enctlem  13018  ctiunctlemfo  13025  slotslfn  13073  setscomd  13088  restfn  13291  elrest  13294  ptex  13312  prdsex  13317  prdsvallem  13320  prdsval  13321  prdsbaslemss  13322  prdsbas  13324  imasex  13353  imasival  13354  imasbas  13355  imasplusg  13356  imasmulr  13357  imasaddfnlemg  13362  fnpr2ob  13388  ismgm  13405  plusffng  13413  fn0g  13423  fngsum  13436  gsumsplit1r  13446  gsumprval  13447  issgrp  13451  ismnddef  13466  gsumfzz  13543  gsumfzcl  13547  mulgnngsum  13679  subgintm  13750  releqgg  13772  eqgex  13773  eqgfval  13774  eqgval  13775  isghm  13795  fnmgp  13900  isrng  13912  isring  13978  ringn0  14038  opprrngbg  14056  opprsubgg  14062  opprunitd  14089  dfrhm2  14133  rhmex  14136  opprsubrngg  14190  subrngintm  14191  subrngpropd  14195  subrgpropd  14232  isdomn  14248  opprdomnbg  14253  scaffng  14288  rmodislmodlem  14329  rmodislmod  14330  lssex  14333  lsssn0  14349  lss1d  14362  lssintclm  14363  ellspsn  14396  rlmfn  14432  isridl  14483  blfn  14530  mopnset  14531  metuex  14534  znval  14615  znleval  14632  psrval  14645  fnpsr  14646  mplvalcoe  14669  fnmpl  14672  bastg  14750  distop  14774  topnex  14775  epttop  14779  tgrest  14858  resttopon  14860  restco  14863  cnrest2  14925  cnptopresti  14927  cnptoprest  14928  cnptoprest2  14929  txuni2  14945  txbas  14947  eltx  14948  txcnp  14960  txcnmpt  14962  txrest  14965  txdis1cn  14967  txlm  14968  cnmpt1st  14977  cnmpt2nd  14978  txhmeo  15008  txswaphmeolem  15009  xmetec  15126  metrest  15195  reldvg  15368  dvfgg  15377  dvcj  15398  dvmptfsum  15414  elply2  15424  pilem3  15472  lgsquadlem1  15771  lgsquadlem2  15772  upgrex  15918  umgredg  15958  umgredgnlp  15965  usgredgreu  16029  uspgredg2vtxeu  16031  ushgredgedg  16039  ushgredgedgloop  16041  wlkvtxiedg  16086  wlkvtxiedgg  16087  wlk1walkdom  16100  bdcvv  16275  bdsnss  16291  bdop  16293  bj-vprc  16314  bdinex1g  16319  bdssexg  16322  bj-inex  16325  bj-zfpair2  16328  bj-uniexg  16336  bdunexb  16338  bj-unexg  16339  bj-indint  16349  bj-ssom  16354  bj-om  16355  bj-2inf  16356  bj-bdfindis  16365  bj-nn0suc0  16368  bj-nnelirr  16371  bj-inf2vnlem1  16388  bj-inf2vnlem2  16389  bj-omex2  16395  bj-nn0sucALT  16396  bj-findis  16397  ss1oel2o  16410  domomsubct  16426  pw1nct  16428  nninfsellemeq  16440  exmidsbthrlem  16450