Theorem vex 2824

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

Syntax hints:   e. wcel 2209   _Vcvv 2821

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  elv  2825  elvd  2826  el2v  2827  isset  2828  eqvisset  2832  ralv  2839  rexv  2840  reuv  2841  rmov  2842  rabab  2843  sbhypf  2872  ceqex  2953  ralab  2986  rexab  2988  mo2icl  3005  reu8  3022  csbvarg  3175  csbiebg  3190  sbcnestgf  3199  sbnfc2  3208  ddifnel  3360  ddifstab  3361  csbing  3438  unssdif  3466  unssin  3470  inssun  3471  invdif  3473  vn0  3532  vn0m  3533  eqv  3541  abvor0dc  3545  sbss  3632  velpw  3692  elpwg  3693  velsn  3722  vsnid  3737  exsnrex  3747  dftp2  3754  prmg  3830  prnzg  3833  snssgOLD  3846  difprsnss  3848  sneqrg  3882  preq12bg  3893  pwprss  3926  pwtpss  3927  pwv  3929  unipr  3944  uniprg  3945  unisng  3947  elintg  3973  elintrabg  3978  intss1  3980  ssint  3981  intmin  3985  intss  3986  intssunim  3987  intmin4  3993  intab  3994  intun  3996  intpr  3997  intprg  3998  uniintsnr  4001  iinconstm  4016  iuniin  4017  iinss1  4019  dfiin2g  4040  dfiunv2  4043  ssiinf  4057  iinss  4059  iinss2  4060  0iin  4066  iinab  4069  iundif2ss  4073  iindif2m  4075  iinin2m  4076  iinuniss  4090  sspwuni  4092  pwpwab  4095  iinpw  4098  iunpwss  4099  brab1  4173  csbopabg  4204  mptv  4223  trint  4239  vnex  4259  inex1g  4264  ssexg  4267  inteximm  4280  inuni  4286  repizf2  4294  axpweq  4303  bnd2  4305  pwuni  4324  exmidundif  4338  exmidundifim  4339  zfpair2  4342  rext  4350  sspwb  4351  unipw  4352  ssextss  4355  euabex  4360  mss  4361  exss  4362  opth  4372  opthg  4373  copsexg  4379  copsex4g  4382  moop2  4387  euotd  4390  opabid  4393  elopab  4395  opelopabsbALT  4396  opelopabsb  4397  opabm  4418  pwin  4422  pwunss  4423  epelg  4430  epel  4432  pofun  4452  epse  4482  tron  4522  sucel  4550  suctr  4561  vuniex  4579  uniexg  4580  unexb  4583  snnex  4589  pwnex  4590  uniuni  4592  eusvnf  4594  eusvnfb  4595  iunpw  4621  unon  4653  ordunisuc2r  4656  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  ordsucunielexmid  4673  elirr  4683  en2lp  4696  dtruex  4701  onintexmid  4715  reg3exmidlemwe  4721  dcextest  4723  finds  4742  finds2  4743  elomssom  4747  limom  4756  0nelxp  4797  opelxp  4799  opeliunxp  4825  elvv  4832  elvvv  4833  elvvuni  4834  xpsspw  4882  relopabiv  4898  relopabi  4900  opabid2  4906  difopab  4908  xpiindim  4912  raliunxp  4916  rexiunxp  4917  ralxpf  4921  rexxpf  4922  relop  4925  cnvco  4960  dfrn2  4963  dfdm4  4968  dmss  4975  dmin  4984  dmiun  4985  dmuni  4986  dm0  4990  dmi  4991  reldm0  4994  reldmm  4995  elreldm  5003  elrnmpt1  5028  dmrnssfld  5040  dmcoss  5047  dmcosseq  5049  opelresg  5065  resieq  5068  dmres  5079  elres  5094  relssres  5096  resopab  5102  resiexg  5103  iss  5104  dfres2  5110  restidsing  5114  dfima2  5123  imadmrn  5131  imai  5138  csbima12g  5143  elimasng  5150  args  5151  epini  5153  iniseg  5154  dfse2  5155  exse2  5156  cotr  5164  issref  5165  cnvsym  5166  intasym  5167  asymref  5168  intirr  5169  brcodir  5170  codir  5171  qfto  5172  poirr2  5175  cnvopab  5184  cnv0  5186  cnvi  5187  cnvdif  5189  rniun  5193  dminss  5197  imainss  5198  inimasn  5200  xpmlem  5203  dmxpss  5213  rnxpid  5217  ssrnres  5225  rninxp  5226  dminxp  5227  cnvcnv3  5232  dfrel2  5233  dmsnm  5248  dmsnopg  5254  cnvcnvsn  5259  dmsnsnsng  5260  cnvsng  5268  elxp4  5270  elxp5  5271  cnvresima  5272  dfco2  5282  dfco2a  5283  cores  5286  resco  5287  imaco  5288  rnco  5289  coiun  5292  co02  5296  coi1  5298  coass  5301  relssdmrn  5303  unielrel  5310  ressn  5323  cnviinm  5324  cnvpom  5325  cnvsom  5326  uniabio  5343  iotaval  5344  iotass  5350  sniota  5363  csbiotag  5365  dffun2  5382  dffun7  5399  dffun8  5400  dffun9  5401  funopg  5406  funssres  5415  funun  5417  funcnvsn  5421  funinsn  5425  funcnv2  5436  funcnv  5437  funcnv3  5438  funcnveq  5439  fun2cnv  5440  funcnvuni  5445  imadif  5456  funimaexglem  5459  isarep1  5462  2elresin  5489  fnres  5495  fcnvres  5570  fconstg  5584  fun11iun  5655  f1osng  5677  dffv3g  5686  fvssunirng  5705  sefvex  5711  fv3  5713  fvres  5714  nfunsn  5727  funimass4  5747  ssimaexg  5759  dmfco  5767  fvopab6  5796  fndmdif  5805  fvelrn  5830  dffo4  5847  f1ompt  5850  fmptco  5865  fsn  5871  fsng  5872  fsn2g  5874  dfmpt  5877  dfmptg  5879  funopsn  5882  funop  5883  funopdmsn  5886  fnressn  5892  fressnfv  5893  fvsng  5902  resfunexg  5927  funfvima3  5942  idref  5952  abrexco  5955  imaiun  5956  dff13  5964  foeqcnvco  5986  f1eqcocnv  5987  fliftcnv  5991  isocnv2  6008  isoini  6014  isose  6017  riotav  6034  csbriotag  6042  acexmidlem2  6072  oprabid  6107  csbov123g  6114  0neqopab  6123  brabvv  6124  dfoprab2  6125  rnoprab  6161  eloprabga  6165  mpov  6168  f1opw  6287  opabex3d  6340  opabex3  6341  abrexss  6348  ofmres  6359  uchoice  6361  op1stg  6374  op2ndg  6375  1stval2  6379  2ndval2  6380  fo1st  6381  fo2nd  6382  f1stres  6383  f2ndres  6384  fo1stresm  6385  fo2ndresm  6386  xp1st  6389  xp2nd  6390  releldm2  6409  reldm  6410  sbcopeq1a  6411  csbopeq1a  6412  dfoprab3  6415  opabn1stprc  6419  eloprabi  6422  mpomptsx  6423  dmmpossx  6425  fmpox  6426  mpofvex  6431  mpoexxg  6436  fmpoco  6442  df1st2  6445  df2nd2  6446  1stconst  6447  2ndconst  6448  dfmpo  6449  fo2ndf  6453  f1o2ndf1  6454  xporderlem  6457  cnvoprab  6460  f1od2  6461  suppval1  6469  cnvimadfsn  6475  suppimacnvfn  6476  brtpos2  6512  reldmtpos  6514  dmtpos  6517  rntpos  6518  ovtposg  6520  dftpos3  6523  dftpos4  6524  tpostpos  6525  tpossym  6537  tfrlem3  6572  tfrlem5  6575  tfrlem8  6579  tfrlemisucfn  6585  tfrlemisucaccv  6586  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrlemibex  6590  tfrlemi14d  6594  tfrexlem  6595  tfr1onlem3  6599  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemres  6610  tfri1dALT  6612  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemres  6623  tfrcl  6625  rdgtfr  6635  rdgruledefgg  6636  rdgivallem  6642  rdgon  6647  rdg0g  6649  frec0g  6658  frecabex  6659  frecabcl  6660  frectfr  6661  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecrdg  6669  oafnex  6707  sucinc  6708  fnoa  6710  oaexg  6711  omfnex  6712  fnom  6713  omexg  6714  fnoei  6715  oeiexg  6716  oeiv  6719  oacl  6723  omcl  6724  oeicl  6725  oav2  6726  nnsucelsuc  6754  nnsucuniel  6758  ercnv  6818  iserd  6823  eqerlem  6828  eqer  6829  ecdmn0m  6841  erth  6843  qsss  6858  ecid  6862  ecidg  6863  qsid  6864  iinerm  6871  qsel  6876  erovlem  6891  ecopovsym  6895  ecopover  6897  th3qlem2  6902  mapprc  6916  fnmap  6919  fnpm  6920  mapdm0  6927  mapfset  6935  mapfoss  6937  fsetsspwxp  6938  fsetdmprc0  6940  mapval2  6949  mapsnd  6960  mapsn  6962  mapsncnv  6967  mapsnf1o2  6968  ixpconstg  6979  ixpprc  6991  ixpin  6995  ixpiinm  6996  ixpssmap2g  6999  ixpssmapg  7000  elixpsn  7007  ixpsnf1o  7008  bren  7020  brdomg  7022  domen  7025  domeng  7026  idssen  7053  domssr  7054  ener  7056  domtr  7062  ensn1g  7074  en1  7076  en1bg  7077  fundmen  7084  fundmeng  7085  mapsnend  7089  mapsnen  7090  fiprc  7094  unen  7095  rex2dom  7100  en2m  7103  dom1o  7106  xpsnen  7109  xpsneng  7110  xpcomco  7114  xpcomeng  7116  xpassen  7118  xpdom2  7119  xpdom2g  7120  pw2f1odc  7125  xpf1o  7134  mapen  7136  mapxpen  7138  xpmapenlem  7139  mapunen  7141  ssenen  7142  phplem4  7146  phplem3g  7147  nneneq  7148  php5  7149  phpm  7157  findcard  7182  findcard2  7183  findcard2s  7184  isinfinf  7191  ac6sfi  7192  exmidpw  7205  exmidpweq  7206  exmidpw2en  7209  unfidisj  7219  fiintim  7228  xpfi  7229  fisseneq  7232  ssfirab  7234  mapfi  7251  snexxph  7257  fidcenumlemr  7262  sbthlemi10  7273  isbth  7274  ssfii  7298  fi0  7299  fiss  7301  f1setfi  7307  cnvinfex  7348  eqinfti  7350  infvalti  7352  infglbti  7355  infmoti  7358  ordiso2  7365  djuf1olem  7383  djuss  7400  ctm  7439  ctssdccl  7441  ctssdclemr  7442  finomni  7470  exmidomni  7472  fodjuomnilemdc  7474  nninfwlpoimlemginf  7506  pm54.43  7526  pr2cv1  7531  exmidfodomrlemim  7543  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  finacn  7550  acfun  7553  ccfunen  7620  cc2lem  7622  cc3  7624  acnccim  7628  indpi  7699  dfplpq2  7711  enq0sym  7789  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  nqnq0  7798  mulnnnq0  7807  nqprm  7899  nqprrnd  7900  nqprdisj  7901  nqprloc  7902  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemrl  7930  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  ltnqpr  7950  ltnqpri  7951  archpr  8000  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlem2  8017  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemopu  8056  suplocexprlemmu  8075  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  cnm  8189  ltresr  8196  peano1nnnn  8209  peano2nnnn  8210  axcnre  8238  axpre-apti  8242  renfdisj  8375  dfinfre  9276  1nn  9294  peano2nn  9295  indstr  9972  cnref1o  10030  ioof  10352  fzpr  10462  frec2uzrand  10820  frec2uzf1od  10821  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  frecfzennn  10841  seqp1g  10881  seqclg  10887  seqf1og  10936  seqfeq4g  10946  ser3le  10952  hashinfom  11195  hashunlem  11222  hashun  11223  hashxp  11245  hashmap  11246  hashfibclem  11260  hashfacen  11262  hashf1lem1  11263  hashf1lem2  11264  hashf1  11265  zfz1isolem1  11270  zfz1iso  11271  fundm2domnop0  11278  wrdexb  11294  fnpfx  11427  cats1un  11471  wrdind  11472  wrd2ind  11473  shftfvalg  11561  ovshftex  11562  shftfibg  11563  shftfval  11564  shftfib  11566  shftfn  11567  2shfti  11574  shftvalg  11579  shftval4g  11580  maxabslemval  11952  fimaxre2  11971  xrmaxiflemval  11994  fclim  12038  climshft  12048  zsumdc  12129  fsum3  12132  fsum2dlemstep  12179  fsumcnv  12182  fisumcom2  12183  fisum0diag2  12192  fsumconst  12199  modfsummodlemstep  12202  fsumabs  12210  fsumrelem  12216  fsumiun  12222  ntrivcvgap  12293  fprod2dlemstep  12367  fprodcnv  12370  fprodcom2fi  12371  fprodmodd  12386  nninfct  12796  algrf  12801  qredeu  12853  isprm2  12873  prmind2  12876  4sqlemafi  13152  4sqlem12  13159  ballotfilemcdc  13201  ballotfilemsf1o  13235  ballotfilem7  13257  ennnfonelemex  13283  ennnfonelemrn  13288  exmidunben  13295  ctinfom  13297  ctinf  13299  qnnen  13300  enctlem  13301  ctiunctlemfo  13308  slotslfn  13356  setscomd  13371  restfn  13574  elrest  13577  ptex  13595  prdsvallem  13598  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfnlemg  13612  fnpr2ob  13638  ismgm  13654  plusffng  13662  fn0g  13672  fngzsum  13685  gzsumsplit1r  13692  issgrp  13695  ismnddef  13708  gzsumcl  13781  mulgnngzsum  13907  subgintm  13978  releqgg  14000  eqgex  14001  eqgfval  14002  eqgval  14003  isghm  14023  gsumvalfi  14129  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  fnmgp  14196  isrng  14208  isring  14278  ringn0  14338  opprrngbg  14356  opprsubgg  14363  opprunitd  14390  dfrhm2  14434  rhmex  14437  opprsubrngg  14492  subrngintm  14493  subrngpropd  14497  subrgpropd  14534  isdomn  14551  opprdomnbg  14556  scaffng  14618  rmodislmodlem  14659  rmodislmod  14660  lssex  14663  lsssn0  14679  lss1d  14692  lssintclm  14693  ellspsn  14726  rlmfn  14762  isridl  14813  blfn  14860  mopnset  14861  metuex  14864  znval  14943  znleval  14960  psrval  14973  fnpsr  14974  mplvalcoe  15004  fnmpl  15007  bastg  15085  distop  15109  topnex  15110  epttop  15114  tgrest  15193  resttopon  15195  restco  15198  cnrest2  15260  cnptopresti  15262  cnptoprest  15263  cnptoprest2  15264  txuni2  15280  txbas  15282  eltx  15283  txcnp  15295  txcnmpt  15297  txrest  15300  txdis1cn  15302  txlm  15303  cnmpt1st  15312  cnmpt2nd  15313  txhmeo  15343  txswaphmeolem  15344  xmetec  15461  metrest  15530  reldvg  15703  dvfgg  15712  dvcj  15733  dvmptfsum  15749  elply2  15759  pilem3  15807  lgsquadlem1  16110  lgsquadlem2  16111  upgrex  16258  upgr1een  16279  umgredg  16300  umgredgnlp  16307  usgredgreu  16371  uspgredg2vtxeu  16373  ushgredgedg  16381  ushgredgedgloop  16383  griedg0ssusgr  16406  uhgrspansubgrlem  16431  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlk1walkdom  16514  eulerpathum  16636  depindlem1  16661  bdcvv  16797  bdsnss  16813  bdop  16815  bj-vprc  16836  bdinex1g  16841  bdssexg  16844  bj-inex  16847  bj-zfpair2  16850  bj-uniexg  16858  bdunexb  16860  bj-unexg  16861  bj-indint  16871  bj-ssom  16876  bj-om  16877  bj-2inf  16878  bj-bdfindis  16887  bj-nn0suc0  16890  bj-nnelirr  16893  bj-inf2vnlem1  16910  bj-inf2vnlem2  16911  bj-omex2  16917  bj-nn0sucALT  16918  bj-findis  16919  ss1oel2o  16931  domomsubct  16945  pw1nct  16947  nninfsellemeq  16962  exmidsbthrlem  16972