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  7359  eqinfti  7361  infvalti  7363  infglbti  7366  infmoti  7369  ordiso2  7376  djuf1olem  7394  djuss  7411  ctm  7450  ctssdccl  7452  ctssdclemr  7453  finomni  7481  exmidomni  7483  fodjuomnilemdc  7485  nninfwlpoimlemginf  7517  pm54.43  7537  pr2cv1  7542  exmidfodomrlemim  7554  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  finacn  7561  acfun  7564  ccfunen  7631  cc2lem  7633  cc3  7635  acnccim  7639  indpi  7710  dfplpq2  7722  enq0sym  7800  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nqnq0  7809  mulnnnq0  7818  nqprm  7910  nqprrnd  7911  nqprdisj  7912  nqprloc  7913  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  ltnqpr  7961  ltnqpri  7962  archpr  8011  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlem2  8028  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemopu  8067  suplocexprlemmu  8086  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  cnm  8200  ltresr  8207  peano1nnnn  8220  peano2nnnn  8221  axcnre  8249  axpre-apti  8253  renfdisj  8386  dfinfre  9289  1nn  9318  peano2nn  9319  indstr  10003  cnref1o  10062  ioof  10384  fzpr  10495  frec2uzrand  10857  frec2uzf1od  10858  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  frecfzennn  10878  seqp1g  10918  seqclg  10924  seqf1og  10973  seqfeq4g  10983  ser3le  10989  hashinfom  11233  hashunlem  11260  hashun  11261  hashxp  11283  hashmap  11284  hashfibclem  11298  hashfacen  11300  hashf1lem1  11301  hashf1lem2  11302  hashf1  11303  zfz1isolem1  11308  zfz1iso  11309  fundm2domnop0  11316  wrdexb  11332  fnpfx  11465  cats1un  11509  wrdind  11510  wrd2ind  11511  shftfvalg  11599  ovshftex  11600  shftfibg  11601  shftfval  11602  shftfib  11604  shftfn  11605  2shfti  11612  shftvalg  11617  shftval4g  11618  maxabslemval  11991  fimaxre2  12010  xrmaxiflemval  12035  fclim  12079  climshft  12089  zsumdc  12170  fsum3  12173  fsum2dlemstep  12220  fsumcnv  12223  fisumcom2  12224  fisum0diag2  12233  fsumconst  12240  modfsummodlemstep  12243  fsumabs  12251  fsumrelem  12257  fsumiun  12263  ntrivcvgap  12334  fprod2dlemstep  12408  fprodcnv  12411  fprodcom2fi  12412  fprodmodd  12427  nninfct  12837  algrf  12842  qredeu  12894  isprm2  12914  prmind2  12917  4sqlemafi  13197  4sqlem12  13204  ballotfilemcdc  13275  ballotfilemsf1o  13309  ballotfilem7  13331  ennnfonelemex  13357  ennnfonelemrn  13362  exmidunben  13369  ctinfom  13371  ctinf  13373  qnnen  13374  enctlem  13375  ctiunctlemfo  13382  slotslfn  13430  setscomd  13445  restfn  13650  elrest  13653  ptex  13671  prdsvallem  13674  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfnlemg  13688  fnpr2ob  13714  ismgm  13730  plusffng  13738  fn0g  13748  fngzsum  13761  gzsumsplit1r  13768  issgrp  13771  ismnddef  13784  gzsumcl  13857  mulgnngzsum  13983  subgintm  14054  releqgg  14076  eqgex  14077  eqgfval  14078  eqgval  14079  isghm  14099  gsumvalfi  14236  prdsex  14256  prdsval  14257  prdsbaslemss  14258  prdsbas  14260  fnmgp  14303  isrng  14317  isring  14388  ringn0  14449  opprrngbg  14467  opprsubgg  14474  opprunitd  14501  dfrhm2  14545  rhmex  14548  opprsubrngg  14603  subrngintm  14604  subrngpropd  14608  subrgpropd  14645  isdomn  14662  opprdomnbg  14667  scaffng  14730  rmodislmodlem  14771  rmodislmod  14772  lssex  14775  lsssn0  14791  lss1d  14804  lssintclm  14805  ellspsn  14838  rlmfn  14874  isridl  14925  blfn  14972  mopnset  14973  metuex  14976  znval  15055  znleval  15072  psrval  15134  fnpsr  15135  mplvalcoe  15172  fnmpl  15175  bastg  15253  distop  15277  topnex  15278  epttop  15282  tgrest  15361  resttopon  15363  restco  15366  cnrest2  15428  cnptopresti  15430  cnptoprest  15431  cnptoprest2  15432  txuni2  15448  txbas  15450  eltx  15451  txcnp  15463  txcnmpt  15465  txrest  15468  txdis1cn  15470  txlm  15471  cnmpt1st  15480  cnmpt2nd  15481  txhmeo  15511  txswaphmeolem  15512  xmetec  15629  metrest  15698  reldvg  15871  dvfgg  15880  dvcj  15901  dvmptfsum  15917  elply2  15927  pilem3  15976  prmorcht  16243  lgsquadlem1  16362  lgsquadlem2  16363  upgrex  16510  upgr1een  16531  umgredg  16552  umgredgnlp  16559  usgredgreu  16623  uspgredg2vtxeu  16625  ushgredgedg  16633  ushgredgedgloop  16635  griedg0ssusgr  16658  uhgrspansubgrlem  16683  upgrspanop  16690  umgrspanop  16691  usgrspanop  16692  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlk1walkdom  16766  eulerpathum  16888  depindlem1  16913  bdcvv  17049  bdsnss  17065  bdop  17067  bj-vprc  17088  bdinex1g  17093  bdssexg  17096  bj-inex  17099  bj-zfpair2  17102  bj-uniexg  17110  bdunexb  17112  bj-unexg  17113  bj-indint  17123  bj-ssom  17128  bj-om  17129  bj-2inf  17130  bj-bdfindis  17139  bj-nn0suc0  17142  bj-nnelirr  17145  bj-inf2vnlem1  17162  bj-inf2vnlem2  17163  bj-omex2  17169  bj-nn0sucALT  17170  bj-findis  17171  ss1oel2o  17183  domomsubct  17197  pw1nct  17199  nninfsellemeq  17223  exmidsbthrlem  17233