Theorem vex 2816

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

Syntax hints:   e. wcel 2203   _Vcvv 2813

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 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  elv  2817  elvd  2818  el2v  2819  isset  2820  eqvisset  2824  ralv  2831  rexv  2832  reuv  2833  rmov  2834  rabab  2835  sbhypf  2864  ceqex  2944  ralab  2977  rexab  2979  mo2icl  2996  reu8  3013  csbvarg  3166  csbiebg  3181  sbcnestgf  3190  sbnfc2  3199  ddifnel  3350  ddifstab  3351  csbing  3428  unssdif  3456  unssin  3460  inssun  3461  invdif  3463  vn0  3519  vn0m  3520  eqv  3528  abvor0dc  3532  sbss  3617  velpw  3676  elpwg  3677  velsn  3706  vsnid  3721  exsnrex  3731  dftp2  3738  prmg  3814  prnzg  3817  snssgOLD  3830  difprsnss  3832  sneqrg  3866  preq12bg  3877  pwprss  3910  pwtpss  3911  pwv  3913  unipr  3928  uniprg  3929  unisng  3931  elintg  3957  elintrabg  3962  intss1  3964  ssint  3965  intmin  3969  intss  3970  intssunim  3971  intmin4  3977  intab  3978  intun  3980  intpr  3981  intprg  3982  uniintsnr  3985  iinconstm  4000  iuniin  4001  iinss1  4003  dfiin2g  4024  dfiunv2  4027  ssiinf  4041  iinss  4043  iinss2  4044  0iin  4050  iinab  4053  iundif2ss  4057  iindif2m  4059  iinin2m  4060  iinuniss  4074  sspwuni  4076  pwpwab  4079  iinpw  4082  iunpwss  4083  brab1  4157  csbopabg  4188  mptv  4207  trint  4223  vnex  4241  inex1g  4246  ssexg  4249  inteximm  4261  inuni  4267  repizf2  4275  axpweq  4284  bnd2  4286  pwuni  4305  exmidundif  4319  exmidundifim  4320  zfpair2  4323  rext  4331  sspwb  4332  unipw  4333  ssextss  4336  euabex  4341  mss  4342  exss  4343  opth  4353  opthg  4354  copsexg  4360  copsex4g  4363  moop2  4368  euotd  4371  opabid  4374  elopab  4376  opelopabsbALT  4377  opelopabsb  4378  opabm  4399  pwin  4403  pwunss  4404  epelg  4411  epel  4413  pofun  4433  epse  4463  tron  4503  sucel  4531  suctr  4542  vuniex  4559  uniexg  4560  unexb  4563  snnex  4569  pwnex  4570  uniuni  4572  eusvnf  4574  eusvnfb  4575  iunpw  4601  unon  4633  ordunisuc2r  4636  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  ordsucunielexmid  4653  elirr  4663  en2lp  4676  dtruex  4681  onintexmid  4695  reg3exmidlemwe  4701  dcextest  4703  finds  4722  finds2  4723  elomssom  4727  limom  4736  0nelxp  4777  opelxp  4779  opeliunxp  4805  elvv  4812  elvvv  4813  elvvuni  4814  xpsspw  4862  relopabiv  4878  relopabi  4880  opabid2  4886  difopab  4888  xpiindim  4892  raliunxp  4896  rexiunxp  4897  ralxpf  4901  rexxpf  4902  relop  4905  cnvco  4940  dfrn2  4943  dfdm4  4948  dmss  4955  dmin  4964  dmiun  4965  dmuni  4966  dm0  4970  dmi  4971  reldm0  4974  reldmm  4975  elreldm  4983  elrnmpt1  5008  dmrnssfld  5020  dmcoss  5027  dmcosseq  5029  opelresg  5045  resieq  5048  dmres  5059  elres  5074  relssres  5076  resopab  5082  resiexg  5083  iss  5084  dfres2  5090  restidsing  5094  dfima2  5103  imadmrn  5111  imai  5118  csbima12g  5123  elimasng  5130  args  5131  epini  5133  iniseg  5134  dfse2  5135  exse2  5136  cotr  5144  issref  5145  cnvsym  5146  intasym  5147  asymref  5148  intirr  5149  brcodir  5150  codir  5151  qfto  5152  poirr2  5155  cnvopab  5164  cnv0  5166  cnvi  5167  cnvdif  5169  rniun  5173  dminss  5177  imainss  5178  inimasn  5180  xpmlem  5183  dmxpss  5193  rnxpid  5197  ssrnres  5205  rninxp  5206  dminxp  5207  cnvcnv3  5212  dfrel2  5213  dmsnm  5228  dmsnopg  5234  cnvcnvsn  5239  dmsnsnsng  5240  cnvsng  5248  elxp4  5250  elxp5  5251  cnvresima  5252  dfco2  5262  dfco2a  5263  cores  5266  resco  5267  imaco  5268  rnco  5269  coiun  5272  co02  5276  coi1  5278  coass  5281  relssdmrn  5283  unielrel  5290  ressn  5303  cnviinm  5304  cnvpom  5305  cnvsom  5306  uniabio  5323  iotaval  5324  iotass  5330  sniota  5343  csbiotag  5345  dffun2  5362  dffun7  5379  dffun8  5380  dffun9  5381  funopg  5386  funssres  5395  funun  5397  funcnvsn  5401  funinsn  5405  funcnv2  5416  funcnv  5417  funcnv3  5418  funcnveq  5419  fun2cnv  5420  funcnvuni  5425  imadif  5436  funimaexglem  5439  isarep1  5442  2elresin  5469  fnres  5475  fcnvres  5550  fconstg  5564  fun11iun  5635  f1osng  5657  dffv3g  5666  fvssunirng  5685  sefvex  5691  fv3  5693  fvres  5694  nfunsn  5707  funimass4  5727  ssimaexg  5739  dmfco  5745  fvopab6  5774  fndmdif  5783  fvelrn  5808  dffo4  5825  f1ompt  5828  fmptco  5843  fsn  5849  fsng  5850  fsn2g  5852  dfmpt  5855  dfmptg  5857  funopsn  5860  funop  5861  funopdmsn  5864  fnressn  5870  fressnfv  5871  fvsng  5880  resfunexg  5905  funfvima3  5920  idref  5929  abrexco  5932  imaiun  5933  dff13  5941  foeqcnvco  5963  f1eqcocnv  5964  fliftcnv  5968  isocnv2  5985  isoini  5991  isose  5994  riotav  6009  csbriotag  6017  acexmidlem2  6047  oprabid  6082  csbov123g  6089  0neqopab  6098  brabvv  6099  dfoprab2  6100  rnoprab  6136  eloprabga  6140  mpov  6143  f1opw  6262  opabex3d  6314  opabex3  6315  ofmres  6329  uchoice  6331  op1stg  6344  op2ndg  6345  1stval2  6349  2ndval2  6350  fo1st  6351  fo2nd  6352  f1stres  6353  f2ndres  6354  fo1stresm  6355  fo2ndresm  6356  xp1st  6359  xp2nd  6360  releldm2  6379  reldm  6380  sbcopeq1a  6381  csbopeq1a  6382  dfoprab3  6385  opabn1stprc  6389  eloprabi  6392  mpomptsx  6393  dmmpossx  6395  fmpox  6396  mpofvex  6401  mpoexxg  6406  fmpoco  6412  df1st2  6415  df2nd2  6416  1stconst  6417  2ndconst  6418  dfmpo  6419  fo2ndf  6423  f1o2ndf1  6424  xporderlem  6427  cnvoprab  6430  f1od2  6431  suppval1  6439  cnvimadfsn  6445  suppimacnvfn  6446  brtpos2  6482  reldmtpos  6484  dmtpos  6487  rntpos  6488  ovtposg  6490  dftpos3  6493  dftpos4  6494  tpostpos  6495  tpossym  6507  tfrlem3  6542  tfrlem5  6545  tfrlem8  6549  tfrlemisucfn  6555  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrlemibex  6560  tfrlemi14d  6564  tfrexlem  6565  tfr1onlem3  6569  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemres  6580  tfri1dALT  6582  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemres  6593  tfrcl  6595  rdgtfr  6605  rdgruledefgg  6606  rdgivallem  6612  rdgon  6617  rdg0g  6619  frec0g  6628  frecabex  6629  frecabcl  6630  frectfr  6631  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecrdg  6639  oafnex  6677  sucinc  6678  fnoa  6680  oaexg  6681  omfnex  6682  fnom  6683  omexg  6684  fnoei  6685  oeiexg  6686  oeiv  6689  oacl  6693  omcl  6694  oeicl  6695  oav2  6696  nnsucelsuc  6724  nnsucuniel  6728  ercnv  6788  iserd  6793  eqerlem  6798  eqer  6799  ecdmn0m  6811  erth  6813  qsss  6828  ecid  6832  ecidg  6833  qsid  6834  iinerm  6841  qsel  6846  erovlem  6861  ecopovsym  6865  ecopover  6867  th3qlem2  6872  mapprc  6886  fnmap  6889  fnpm  6890  mapdm0  6897  mapval2  6912  mapsnd  6923  mapsn  6925  mapsncnv  6930  mapsnf1o2  6931  ixpconstg  6942  ixpprc  6954  ixpin  6958  ixpiinm  6959  ixpssmap2g  6962  ixpssmapg  6963  elixpsn  6970  ixpsnf1o  6971  bren  6983  brdomg  6985  domen  6988  domeng  6989  idssen  7016  domssr  7017  ener  7019  domtr  7025  ensn1g  7037  en1  7039  en1bg  7040  fundmen  7047  fundmeng  7048  mapsnend  7052  mapsnen  7053  fiprc  7057  unen  7058  rex2dom  7063  en2m  7066  dom1o  7069  xpsnen  7072  xpsneng  7073  xpcomco  7077  xpcomeng  7079  xpassen  7081  xpdom2  7082  xpdom2g  7083  pw2f1odc  7088  xpf1o  7097  mapen  7099  mapxpen  7101  xpmapenlem  7102  mapunen  7104  ssenen  7105  phplem4  7109  phplem3g  7110  nneneq  7111  php5  7112  phpm  7120  findcard  7145  findcard2  7146  findcard2s  7147  isinfinf  7154  ac6sfi  7155  exmidpw  7168  exmidpweq  7169  exmidpw2en  7172  unfidisj  7182  fiintim  7191  xpfi  7192  fisseneq  7195  ssfirab  7197  mapfi  7214  snexxph  7220  fidcenumlemr  7225  sbthlemi10  7236  isbth  7237  ssfii  7261  fi0  7262  fiss  7264  cnvinfex  7309  eqinfti  7311  infvalti  7313  infglbti  7316  infmoti  7319  ordiso2  7326  djuf1olem  7344  djuss  7361  ctm  7400  ctssdccl  7402  ctssdclemr  7403  finomni  7431  exmidomni  7433  fodjuomnilemdc  7435  nninfwlpoimlemginf  7467  pm54.43  7487  pr2cv1  7492  exmidfodomrlemim  7504  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  finacn  7511  acfun  7514  ccfunen  7578  cc2lem  7580  cc3  7582  acnccim  7586  indpi  7657  dfplpq2  7669  enq0sym  7747  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  nqnq0  7756  mulnnnq0  7765  nqprm  7857  nqprrnd  7858  nqprdisj  7859  nqprloc  7860  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemrl  7888  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  ltnqpr  7908  ltnqpri  7909  archpr  7958  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlem2  7975  caucvgprlemladdfu  7992  caucvgprlem2  7995  caucvgprprlemopu  8014  suplocexprlemmu  8033  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  cnm  8147  ltresr  8154  peano1nnnn  8167  peano2nnnn  8168  axcnre  8196  axpre-apti  8200  renfdisj  8333  dfinfre  9230  1nn  9248  peano2nn  9249  indstr  9925  cnref1o  9983  ioof  10304  fzpr  10411  frec2uzrand  10767  frec2uzf1od  10768  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  frecfzennn  10788  seqp1g  10828  seqclg  10834  seqf1og  10883  seqfeq4g  10893  ser3le  10899  hashinfom  11141  hashunlem  11168  hashun  11169  hashxp  11191  hashmap  11192  hashfibclem  11206  hashfacen  11208  zfz1isolem1  11212  zfz1iso  11213  fundm2domnop0  11220  wrdexb  11236  fnpfx  11369  cats1un  11413  wrdind  11414  wrd2ind  11415  shftfvalg  11503  ovshftex  11504  shftfibg  11505  shftfval  11506  shftfib  11508  shftfn  11509  2shfti  11516  shftvalg  11521  shftval4g  11522  maxabslemval  11893  fimaxre2  11912  xrmaxiflemval  11935  fclim  11979  climshft  11989  zsumdc  12070  fsum3  12073  fsum2dlemstep  12120  fsumcnv  12123  fisumcom2  12124  fisum0diag2  12133  fsumconst  12140  modfsummodlemstep  12143  fsumabs  12151  fsumrelem  12157  fsumiun  12163  ntrivcvgap  12234  fprod2dlemstep  12308  fprodcnv  12311  fprodcom2fi  12312  fprodmodd  12327  nninfct  12737  algrf  12742  qredeu  12794  isprm2  12814  prmind2  12817  4sqlemafi  13093  4sqlem12  13100  ennnfonelemex  13165  ennnfonelemrn  13170  exmidunben  13177  ctinfom  13179  ctinf  13181  qnnen  13182  enctlem  13183  ctiunctlemfo  13190  slotslfn  13238  setscomd  13253  restfn  13456  elrest  13459  ptex  13477  prdsex  13482  prdsvallem  13485  prdsval  13486  prdsbaslemss  13487  prdsbas  13489  imasex  13518  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfnlemg  13527  fnpr2ob  13553  ismgm  13570  plusffng  13578  fn0g  13588  fngsum  13601  gsumsplit1r  13611  gsumprval  13612  issgrp  13616  ismnddef  13631  gsumfzz  13708  gsumfzcl  13712  mulgnngsum  13844  subgintm  13915  releqgg  13937  eqgex  13938  eqgfval  13939  eqgval  13940  isghm  13960  fnmgp  14066  isrng  14078  isring  14144  ringn0  14204  opprrngbg  14222  opprsubgg  14228  opprunitd  14255  dfrhm2  14299  rhmex  14302  opprsubrngg  14356  subrngintm  14357  subrngpropd  14361  subrgpropd  14398  isdomn  14415  opprdomnbg  14420  scaffng  14457  rmodislmodlem  14498  rmodislmod  14499  lssex  14502  lsssn0  14518  lss1d  14531  lssintclm  14532  ellspsn  14565  rlmfn  14601  isridl  14652  blfn  14699  mopnset  14700  metuex  14703  znval  14784  znleval  14801  psrval  14814  fnpsr  14815  mplvalcoe  14845  fnmpl  14848  bastg  14926  distop  14950  topnex  14951  epttop  14955  tgrest  15034  resttopon  15036  restco  15039  cnrest2  15101  cnptopresti  15103  cnptoprest  15104  cnptoprest2  15105  txuni2  15121  txbas  15123  eltx  15124  txcnp  15136  txcnmpt  15138  txrest  15141  txdis1cn  15143  txlm  15144  cnmpt1st  15153  cnmpt2nd  15154  txhmeo  15184  txswaphmeolem  15185  xmetec  15302  metrest  15371  reldvg  15544  dvfgg  15553  dvcj  15574  dvmptfsum  15590  elply2  15600  pilem3  15648  lgsquadlem1  15950  lgsquadlem2  15951  upgrex  16098  upgr1een  16119  umgredg  16140  umgredgnlp  16147  usgredgreu  16211  uspgredg2vtxeu  16213  ushgredgedg  16221  ushgredgedgloop  16223  griedg0ssusgr  16246  uhgrspansubgrlem  16271  upgrspanop  16278  umgrspanop  16279  usgrspanop  16280  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlk1walkdom  16354  eulerpathum  16476  depindlem1  16501  bdcvv  16627  bdsnss  16643  bdop  16645  bj-vprc  16666  bdinex1g  16671  bdssexg  16674  bj-inex  16677  bj-zfpair2  16680  bj-uniexg  16688  bdunexb  16690  bj-unexg  16691  bj-indint  16701  bj-ssom  16706  bj-om  16707  bj-2inf  16708  bj-bdfindis  16717  bj-nn0suc0  16720  bj-nnelirr  16723  bj-inf2vnlem1  16740  bj-inf2vnlem2  16741  bj-omex2  16747  bj-nn0sucALT  16748  bj-findis  16749  ss1oel2o  16761  domomsubct  16775  pw1nct  16777  nninfsellemeq  16792  exmidsbthrlem  16802  gfsumval  16862