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

This proof depends on syntax axioms:   e. wcel 2209   _Vcvv 2821

This proof depends on 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 proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used 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  3635  velpw  3695  elpwg  3696  velsn  3726  vsnid  3741  exsnrex  3751  dftp2  3758  prmg  3835  prnzg  3838  snssgOLD  3851  difprsnss  3853  sneqrg  3887  preq12bg  3898  pwprss  3931  pwtpss  3932  pwv  3934  unipr  3949  uniprg  3950  unisng  3952  elintg  3978  elintrabg  3983  intss1  3985  ssint  3986  intmin  3990  intss  3991  intssunim  3992  intmin4  3998  intab  3999  intun  4001  intpr  4002  intprg  4003  uniintsnr  4006  iinconstm  4021  iuniin  4022  iinss1  4024  dfiin2g  4045  dfiunv2  4048  ssiinf  4062  iinss  4064  iinss2  4065  0iin  4071  iinab  4074  iundif2ss  4078  iindif2m  4080  iinin2m  4081  iinuniss  4095  sspwuni  4097  pwpwab  4100  iinpw  4103  iunpwss  4104  brab1  4178  csbopabg  4209  mptv  4228  trint  4244  vnex  4264  inex1g  4269  ssexg  4272  inteximm  4285  inuni  4291  repizf2  4299  axpweq  4308  bnd2  4310  pwuni  4329  exmidundif  4343  exmidundifim  4344  zfpair2  4347  rext  4355  sspwb  4356  unipw  4357  ssextss  4360  euabex  4365  mss  4366  exss  4367  opth  4377  opthg  4378  copsexg  4384  copsex4g  4387  moop2  4392  euotd  4395  opabid  4398  elopab  4400  opelopabsbALT  4401  opelopabsb  4402  opabm  4423  pwin  4427  pwunss  4428  epelg  4435  epel  4437  pofun  4457  epse  4487  tron  4527  sucel  4555  suctr  4566  vuniex  4584  uniexg  4585  unexb  4588  snnex  4594  pwnex  4595  uniuni  4597  eusvnf  4599  eusvnfb  4600  iunpw  4626  unon  4658  ordunisuc2r  4661  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsucunielexmid  4678  elirr  4688  en2lp  4701  dtruex  4706  onintexmid  4720  reg3exmidlemwe  4726  dcextest  4728  finds  4747  finds2  4748  elomssom  4752  limom  4761  0nelxp  4802  opelxp  4804  opeliunxp  4830  elvv  4837  elvvv  4838  elvvuni  4839  xpsspw  4887  relopabiv  4903  relopabi  4905  opabid2  4911  difopab  4913  xpiindim  4917  raliunxp  4921  rexiunxp  4922  ralxpf  4926  rexxpf  4927  relop  4930  cnvco  4965  dfrn2  4968  dfdm4  4973  dmss  4980  dmin  4989  dmiun  4990  dmuni  4991  dm0  4995  dmi  4996  reldm0  4999  reldmm  5000  elreldm  5008  elrnmpt1  5033  dmrnssfld  5045  dmcoss  5052  dmcosseq  5054  opelresg  5070  resieq  5073  dmres  5084  elres  5099  relssres  5101  resopab  5107  resiexg  5108  iss  5109  dfres2  5115  restidsing  5119  dfima2  5128  imadmrn  5136  imai  5143  csbima12g  5148  elimasng  5155  args  5156  epini  5158  iniseg  5159  dfse2  5160  exse2  5161  cotr  5169  issref  5170  cnvsym  5171  intasym  5172  asymref  5173  intirr  5174  brcodir  5175  codir  5176  qfto  5177  poirr2  5180  cnvopab  5189  cnv0  5191  cnvi  5192  cnvdif  5194  rniun  5198  dminss  5202  imainss  5203  inimasn  5205  xpmlem  5208  dmxpss  5218  rnxpid  5222  ssrnres  5230  rninxp  5231  dminxp  5232  cnvcnv3  5237  dfrel2  5238  dmsnm  5253  dmsnopg  5259  cnvcnvsn  5264  dmsnsnsng  5265  cnvsng  5273  elxp4  5275  elxp5  5276  cnvresima  5277  dfco2  5287  dfco2a  5288  cores  5291  resco  5292  imaco  5293  rnco  5294  coiun  5297  co02  5301  coi1  5303  coass  5306  relssdmrn  5308  unielrel  5315  ressn  5328  cnviinm  5329  cnvpom  5330  cnvsom  5331  uniabio  5348  iotaval  5349  iotass  5355  sniota  5368  csbiotag  5370  dffun2  5387  dffun7  5404  dffun8  5405  dffun9  5406  funopg  5411  funssres  5420  funun  5422  funcnvsn  5426  funinsn  5430  funcnv2  5441  funcnv  5442  funcnv3  5443  funcnveq  5444  fun2cnv  5445  funcnvuni  5450  imadif  5461  funimaexglem  5464  isarep1  5467  2elresin  5494  fnres  5500  fcnvres  5575  fconstg  5589  fun11iun  5660  f1osng  5682  dffv3g  5691  fvssunirng  5710  sefvex  5716  fv3  5718  fvres  5719  nfunsn  5733  funimass4  5753  ssimaexg  5765  dmfco  5773  fvopab6  5805  fndmdif  5814  fvelrn  5839  dffo4  5856  f1ompt  5859  fmptco  5874  fsn  5880  fsng  5881  fsn2g  5883  dfmpt  5886  dfmptg  5888  funopsn  5891  funop  5892  funopdmsn  5895  fnressn  5901  fressnfv  5902  fvsng  5911  resfunexg  5936  funfvima3  5952  idref  5962  abrexco  5965  imaiun  5966  dff13  5974  foeqcnvco  5996  f1eqcocnv  5997  fliftcnv  6001  isocnv2  6018  isoini  6024  isose  6027  riotav  6044  csbriotag  6052  acexmidlem2  6082  oprabid  6117  csbov123g  6124  0neqopab  6133  brabvv  6134  dfoprab2  6135  rnoprab  6171  eloprabga  6175  mpov  6178  f1opw  6297  opabex3d  6350  opabex3  6351  abrexss  6358  ofmres  6369  uchoice  6371  op1stg  6384  op2ndg  6385  1stval2  6389  2ndval2  6390  fo1st  6391  fo2nd  6392  f1stres  6393  f2ndres  6394  fo1stresm  6395  fo2ndresm  6396  xp1st  6399  xp2nd  6400  releldm2  6419  reldm  6420  sbcopeq1a  6421  csbopeq1a  6422  dfoprab3  6425  opabn1stprc  6429  eloprabi  6432  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  mpoexxg  6446  fmpoco  6452  df1st2  6455  df2nd2  6456  1stconst  6457  2ndconst  6458  dfmpo  6459  fo2ndf  6463  f1o2ndf1  6464  xporderlem  6467  cnvoprab  6470  f1od2  6471  suppval1  6479  cnvimadfsn  6485  suppimacnvfn  6486  brtpos2  6522  reldmtpos  6524  dmtpos  6527  rntpos  6528  ovtposg  6530  dftpos3  6533  dftpos4  6534  tpostpos  6535  tpossym  6547  tfrlem3  6582  tfrlem5  6585  tfrlem8  6589  tfrlemisucfn  6595  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemibex  6600  tfrlemi14d  6604  tfrexlem  6605  tfr1onlem3  6609  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  tfrcl  6635  rdgtfr  6645  rdgruledefgg  6646  rdgivallem  6652  rdgon  6657  rdg0g  6659  frec0g  6668  frecabex  6669  frecabcl  6670  frectfr  6671  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  oafnex  6717  sucinc  6718  fnoa  6720  oaexg  6721  omfnex  6722  fnom  6723  omexg  6724  fnoei  6725  oeiexg  6726  oeiv  6729  oacl  6733  omcl  6734  oeicl  6735  oav2  6736  nnsucelsuc  6764  nnsucuniel  6768  ercnv  6828  iserd  6833  eqerlem  6838  eqer  6839  ecdmn0m  6851  erth  6853  qsss  6868  ecid  6872  ecidg  6873  qsid  6874  iinerm  6881  qsel  6886  erovlem  6901  ecopovsym  6905  ecopover  6907  th3qlem2  6912  mapprc  6926  fnmap  6929  fnpm  6930  mapdm0  6937  mapfset  6945  mapfoss  6947  fsetsspwxp  6948  fsetdmprc0  6950  mapval2  6959  mapsnd  6970  mapsn  6972  mapsncnv  6977  mapsnf1o2  6978  ixpconstg  6989  ixpprc  7001  ixpin  7005  ixpiinm  7006  ixpssmap2g  7009  ixpssmapg  7010  elixpsn  7017  ixpsnf1o  7018  bren  7030  brdomg  7032  domen  7035  domeng  7036  idssen  7063  domssr  7064  ener  7066  domtr  7072  ensn1g  7084  en1  7086  en1bg  7087  fundmen  7094  fundmeng  7095  mapsnend  7099  mapsnen  7100  fiprc  7104  unen  7105  rex2dom  7110  en2m  7113  dom1o  7116  xpsnen  7119  xpsneng  7120  xpcomco  7124  xpcomeng  7126  xpassen  7128  xpdom2  7129  xpdom2g  7130  pw2f1odc  7135  xpf1o  7144  mapen  7146  mapxpen  7148  xpmapenlem  7149  mapunen  7151  ssenen  7152  phplem4  7156  phplem3g  7157  nneneq  7158  php5  7159  phpm  7167  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  ac6sfi  7202  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  unfidisj  7229  fiintim  7238  xpfi  7239  fisseneq  7242  ssfirab  7244  mapfi  7261  snexxph  7267  fidcenumlemr  7272  sbthlemi10  7283  isbth  7284  ssfii  7308  fi0  7309  fiss  7311  f1setfi  7317  cnvinfex  7358  eqinfti  7360  infvalti  7362  infglbti  7365  infmoti  7368  ordiso2  7375  djuf1olem  7393  djuss  7410  ctm  7449  ctssdccl  7451  ctssdclemr  7452  finomni  7480  exmidomni  7482  fodjuomnilemdc  7484  nninfwlpoimlemginf  7516  pm54.43  7536  pr2cv1  7541  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  finacn  7560  acfun  7563  ccfunen  7630  cc2lem  7632  cc3  7634  acnccim  7638  indpi  7709  dfplpq2  7721  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  mulnnnq0  7817  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  ltnqpr  7960  ltnqpri  7961  archpr  8010  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemopu  8066  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  cnm  8199  ltresr  8206  peano1nnnn  8219  peano2nnnn  8220  axcnre  8248  axpre-apti  8252  renfdisj  8385  dfinfre  9286  1nn  9315  peano2nn  9316  indstr  9993  cnref1o  10051  ioof  10373  fzpr  10484  frec2uzrand  10842  frec2uzf1od  10843  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  frecfzennn  10863  seqp1g  10903  seqclg  10909  seqf1og  10958  seqfeq4g  10968  ser3le  10974  hashinfom  11217  hashunlem  11244  hashun  11245  hashxp  11267  hashmap  11268  hashfibclem  11282  hashfacen  11284  hashf1lem1  11285  hashf1lem2  11286  hashf1  11287  zfz1isolem1  11292  zfz1iso  11293  fundm2domnop0  11300  wrdexb  11316  fnpfx  11449  cats1un  11493  wrdind  11494  wrd2ind  11495  shftfvalg  11583  ovshftex  11584  shftfibg  11585  shftfval  11586  shftfib  11588  shftfn  11589  2shfti  11596  shftvalg  11601  shftval4g  11602  maxabslemval  11974  fimaxre2  11993  xrmaxiflemval  12016  fclim  12060  climshft  12070  zsumdc  12151  fsum3  12154  fsum2dlemstep  12201  fsumcnv  12204  fisumcom2  12205  fisum0diag2  12214  fsumconst  12221  modfsummodlemstep  12224  fsumabs  12232  fsumrelem  12238  fsumiun  12244  ntrivcvgap  12315  fprod2dlemstep  12389  fprodcnv  12392  fprodcom2fi  12393  fprodmodd  12408  nninfct  12818  algrf  12823  qredeu  12875  isprm2  12895  prmind2  12898  4sqlemafi  13174  4sqlem12  13181  ballotfilemcdc  13223  ballotfilemsf1o  13257  ballotfilem7  13279  ennnfonelemex  13305  ennnfonelemrn  13310  exmidunben  13317  ctinfom  13319  ctinf  13321  qnnen  13322  enctlem  13323  ctiunctlemfo  13330  slotslfn  13378  setscomd  13393  restfn  13597  elrest  13600  ptex  13618  prdsvallem  13621  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfnlemg  13635  fnpr2ob  13661  ismgm  13677  plusffng  13685  fn0g  13695  fngzsum  13708  gzsumsplit1r  13715  issgrp  13718  ismnddef  13731  gzsumcl  13804  mulgnngzsum  13930  subgintm  14001  releqgg  14023  eqgex  14024  eqgfval  14025  eqgval  14026  isghm  14046  gsumvalfi  14152  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  fnmgp  14219  isrng  14233  isring  14304  ringn0  14365  opprrngbg  14383  opprsubgg  14390  opprunitd  14417  dfrhm2  14461  rhmex  14464  opprsubrngg  14519  subrngintm  14520  subrngpropd  14524  subrgpropd  14561  isdomn  14578  opprdomnbg  14583  scaffng  14646  rmodislmodlem  14687  rmodislmod  14688  lssex  14691  lsssn0  14707  lss1d  14720  lssintclm  14721  ellspsn  14754  rlmfn  14790  isridl  14841  blfn  14888  mopnset  14889  metuex  14892  znval  14971  znleval  14988  psrval  15050  fnpsr  15051  mplvalcoe  15081  fnmpl  15084  bastg  15162  distop  15186  topnex  15187  epttop  15191  tgrest  15270  resttopon  15272  restco  15275  cnrest2  15337  cnptopresti  15339  cnptoprest  15340  cnptoprest2  15341  txuni2  15357  txbas  15359  eltx  15360  txcnp  15372  txcnmpt  15374  txrest  15377  txdis1cn  15379  txlm  15380  cnmpt1st  15389  cnmpt2nd  15390  txhmeo  15420  txswaphmeolem  15421  xmetec  15538  metrest  15607  reldvg  15780  dvfgg  15789  dvcj  15810  dvmptfsum  15826  elply2  15836  pilem3  15884  lgsquadlem1  16196  lgsquadlem2  16197  upgrex  16344  upgr1een  16365  umgredg  16386  umgredgnlp  16393  usgredgreu  16457  uspgredg2vtxeu  16459  ushgredgedg  16467  ushgredgedgloop  16469  griedg0ssusgr  16492  uhgrspansubgrlem  16517  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlk1walkdom  16600  eulerpathum  16722  depindlem1  16747  bdcvv  16883  bdsnss  16899  bdop  16901  bj-vprc  16922  bdinex1g  16927  bdssexg  16930  bj-inex  16933  bj-zfpair2  16936  bj-uniexg  16944  bdunexb  16946  bj-unexg  16947  bj-indint  16957  bj-ssom  16962  bj-om  16963  bj-2inf  16964  bj-bdfindis  16973  bj-nn0suc0  16976  bj-nnelirr  16979  bj-inf2vnlem1  16996  bj-inf2vnlem2  16997  bj-omex2  17003  bj-nn0sucALT  17004  bj-findis  17005  ss1oel2o  17017  domomsubct  17031  pw1nct  17033  nninfsellemeq  17057  exmidsbthrlem  17067