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  4179  csbopabg  4210  mptv  4230  trint  4246  vnex  4266  inex1g  4271  ssexg  4274  inteximm  4287  inuni  4293  repizf2  4301  axpweq  4310  bnd2  4312  pwuni  4331  exmidundif  4345  exmidundifim  4346  zfpair2  4349  rext  4357  sspwb  4358  unipw  4359  ssextss  4362  euabex  4367  mss  4368  exss  4369  opth  4379  opthg  4380  copsexg  4386  copsex4g  4389  moop2  4394  euotd  4397  opabid  4400  elopab  4402  opelopabsbALT  4403  opelopabsb  4404  opabm  4425  pwin  4429  pwunss  4430  epelg  4437  epel  4439  pofun  4459  epse  4489  tron  4529  sucel  4557  suctr  4568  vuniex  4586  uniexg  4587  unexb  4590  snnex  4596  pwnex  4597  uniuni  4599  eusvnf  4601  eusvnfb  4602  iunpw  4628  unon  4660  ordunisuc2r  4663  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsucunielexmid  4680  elirr  4690  en2lp  4703  dtruex  4708  onintexmid  4722  reg3exmidlemwe  4728  dcextest  4730  finds  4749  finds2  4750  elomssom  4754  limom  4763  0nelxp  4804  opelxp  4806  opeliunxp  4832  elvv  4839  elvvv  4840  elvvuni  4841  xpsspw  4889  relopabiv  4905  relopabi  4907  opabid2  4913  difopab  4915  xpiindim  4919  raliunxp  4923  rexiunxp  4924  ralxpf  4928  rexxpf  4929  relop  4932  cnvco  4967  dfrn2  4970  dfdm4  4975  dmss  4982  dmin  4991  dmiun  4992  dmuni  4993  dm0  4997  dmi  4998  reldm0  5001  reldmm  5002  elreldm  5010  elrnmpt1  5035  dmrnssfld  5047  dmcoss  5054  dmcosseq  5056  opelresg  5072  resieq  5075  dmres  5086  elres  5101  relssres  5103  resopab  5110  resiexg  5111  iss  5112  dfres2  5118  restidsing  5122  dfima2  5131  imadmrn  5139  imai  5146  csbima12g  5151  elimasng  5158  args  5159  epini  5161  iniseg  5162  dfse2  5163  exse2  5164  cotr  5172  issref  5173  cnvsym  5174  intasym  5175  asymref  5176  intirr  5177  brcodir  5178  codir  5179  qfto  5180  poirr2  5183  cnvopab  5192  cnv0  5194  cnvi  5195  cnvdif  5197  rniun  5201  dminss  5205  imainss  5206  inimasn  5208  xpmlem  5211  dmxpss  5221  rnxpid  5225  ssrnres  5233  rninxp  5234  dminxp  5235  cnvcnv3  5240  dfrel2  5241  dmsnm  5256  dmsnopg  5262  cnvcnvsn  5267  dmsnsnsng  5268  cnvsng  5276  elxp4  5278  elxp5  5279  cnvresima  5280  dfco2  5290  dfco2a  5291  cores  5294  resco  5295  imaco  5296  rnco  5297  coiun  5300  co02  5304  coi1  5306  coass  5309  relssdmrn  5311  unielrel  5318  ressn  5331  cnviinm  5332  cnvpom  5333  cnvsom  5334  uniabio  5351  iotaval  5352  iotass  5358  sniota  5371  csbiotag  5373  dffun2  5390  dffun7  5407  dffun8  5408  dffun9  5409  funopg  5414  funssres  5423  funun  5425  funcnvsn  5429  funinsn  5433  funcnv2  5444  funcnv  5445  funcnv3  5446  funcnveq  5447  fun2cnv  5448  funcnvuni  5453  imadif  5464  funimaexglem  5467  isarep1  5470  2elresin  5497  fnres  5503  fcnvres  5578  fconstg  5592  fun11iun  5663  f1osng  5685  dffv3g  5694  fvssunirng  5713  sefvex  5719  fv3  5721  fvres  5722  nfunsn  5736  funimass4  5756  ssimaexg  5768  dmfco  5776  fvopab6  5808  fndmdif  5817  fvelrn  5842  dffo4  5859  f1ompt  5862  fmptco  5877  fsn  5883  fsng  5884  fsn2g  5886  dfmpt  5889  dfmptg  5891  funopsn  5894  funop  5895  funopdmsn  5898  fnressn  5904  fressnfv  5905  fvsng  5914  resfunexg  5939  funfvima3  5955  idref  5965  abrexco  5968  imaiun  5969  dff13  5977  foeqcnvco  5999  f1eqcocnv  6000  fliftcnv  6004  isocnv2  6021  isoini  6027  isose  6030  riotav  6047  csbriotag  6055  acexmidlem2  6085  oprabid  6120  csbov123g  6127  0neqopab  6136  brabvv  6137  dfoprab2  6138  rnoprab  6174  eloprabga  6178  mpov  6181  f1opw  6300  opabex3d  6354  opabex3  6355  abrexss  6362  ofmres  6373  uchoice  6375  op1stg  6388  op2ndg  6389  1stval2  6393  2ndval2  6394  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  fo1stresm  6399  fo2ndresm  6400  xp1st  6403  xp2nd  6404  releldm2  6423  reldm  6424  sbcopeq1a  6425  csbopeq1a  6426  dfoprab3  6429  opabn1stprc  6433  eloprabi  6436  mpomptsx  6437  dmmpossx  6439  fmpox  6440  mpofvex  6445  mpoexxg  6450  fmpoco  6456  df1st2  6459  df2nd2  6460  1stconst  6461  2ndconst  6462  dfmpo  6463  fo2ndf  6467  f1o2ndf1  6468  xporderlem  6471  cnvoprab  6474  f1od2  6475  suppval1  6483  cnvimadfsn  6489  suppimacnvfn  6490  suppinisegdc  6513  brtpos2  6527  reldmtpos  6529  dmtpos  6532  rntpos  6533  ovtposg  6535  dftpos3  6538  dftpos4  6539  tpostpos  6540  tpossym  6552  tfrlem3  6587  tfrlem5  6590  tfrlem8  6594  tfrlemisucfn  6600  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemibex  6605  tfrlemi14d  6609  tfrexlem  6610  tfr1onlem3  6614  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemres  6625  tfri1dALT  6627  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemres  6638  tfrcl  6640  rdgtfr  6650  rdgruledefgg  6651  rdgivallem  6657  rdgon  6662  rdg0g  6664  frec0g  6673  frecabex  6674  frecabcl  6675  frectfr  6676  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecrdg  6684  oafnex  6722  sucinc  6723  fnoa  6725  oaexg  6726  omfnex  6727  fnom  6728  omexg  6729  fnoei  6730  oeiexg  6731  oeiv  6734  oacl  6738  omcl  6739  oeicl  6740  oav2  6741  nnsucelsuc  6769  nnsucuniel  6773  ercnv  6833  iserd  6838  eqerlem  6843  eqer  6844  ecdmn0m  6856  erth  6858  qsss  6873  ecid  6877  ecidg  6878  qsid  6879  iinerm  6886  qsel  6891  erovlem  6906  ecopovsym  6910  ecopover  6912  th3qlem2  6917  mapprc  6931  fnmap  6934  fnpm  6935  mapdm0  6942  mapfset  6950  mapfoss  6952  fsetsspwxp  6953  fsetdmprc0  6955  mapval2  6964  mapsnd  6976  mapsn  6978  mapsncnv  6983  mapsnf1o2  6984  ixpconstg  6995  ixpprc  7007  ixpin  7011  ixpiinm  7012  ixpssmap2g  7015  ixpssmapg  7016  elixpsn  7023  ixpsnf1o  7024  bren  7036  brdomg  7038  domen  7041  domeng  7042  idssen  7069  domssr  7070  ener  7072  domtr  7078  ensn1g  7090  en1  7092  en1bg  7093  fundmen  7100  fundmeng  7101  mapsnend  7105  mapsnen  7106  fiprc  7110  unen  7111  rex2dom  7116  en2m  7119  dom1o  7122  xpsnen  7125  xpsneng  7126  xpcomco  7130  xpcomeng  7132  xpassen  7134  xpdom2  7135  xpdom2g  7136  pw2f1odc  7141  xpf1o  7150  mapen  7152  mapxpen  7154  xpmapenlem  7155  mapunen  7157  ssenen  7158  phplem4  7162  phplem3g  7163  nneneq  7164  php5  7165  phpm  7173  findcard  7198  findcard2  7199  findcard2s  7200  isinfinf  7207  ac6sfi  7208  exmidpw  7221  exmidpweq  7222  exmidpw2en  7225  unfidisj  7235  fiintim  7244  xpfi  7245  fisseneq  7248  ssfirab  7250  mapfi  7267  snexxph  7274  fidcenumlemr  7279  sbthlemi10  7290  isbth  7291  ssfii  7313  fi0  7314  fiss  7316  f1setfi  7322  cnvinfex  7364  eqinfti  7366  infvalti  7368  infglbti  7371  infmoti  7374  ordiso2  7381  djuf1olem  7399  djuss  7416  ctm  7455  ctssdccl  7457  ctssdclemr  7458  finomni  7486  exmidomni  7488  fodjuomnilemdc  7490  nninfwlpoimlemginf  7522  pm54.43  7542  pr2cv1  7547  exmidfodomrlemim  7559  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  finacn  7566  acfun  7569  ccfunen  7636  cc2lem  7638  cc3  7640  acnccim  7644  indpi  7715  dfplpq2  7727  enq0sym  7805  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  nqnq0  7814  mulnnnq0  7823  nqprm  7915  nqprrnd  7916  nqprdisj  7917  nqprloc  7918  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  ltnqpr  7966  ltnqpri  7967  archpr  8016  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlem2  8033  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemopu  8072  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  cnm  8205  ltresr  8212  peano1nnnn  8225  peano2nnnn  8226  axcnre  8254  axpre-apti  8258  renfdisj  8391  dfinfre  9294  1nn  9324  peano2nn  9325  indstr  10008  cnref1o  10067  ioof  10389  fzpr  10500  frec2uzrand  10862  frec2uzf1od  10863  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  frecfzennn  10883  seqp1g  10923  seqclg  10929  seqf1og  10978  seqfeq4g  10988  ser3le  10994  hashinfom  11238  hashunlem  11265  hashun  11266  hashxp  11288  hashmap  11289  hashfibclem  11303  hashfacen  11305  hashf1lem1  11306  hashf1lem2  11307  hashf1  11308  zfz1isolem1  11313  zfz1iso  11314  fundm2domnop0  11321  wrdexb  11337  fnpfx  11470  cats1un  11514  wrdind  11515  wrd2ind  11516  shftfvalg  11604  ovshftex  11605  shftfibg  11606  shftfval  11607  shftfib  11609  shftfn  11610  2shfti  11617  shftvalg  11622  shftval4g  11623  maxabslemval  11996  fimaxre2  12015  xrmaxiflemval  12040  fclim  12084  climshft  12094  zsumdc  12175  fsum3  12178  fsum2dlemstep  12225  fsumcnv  12228  fisumcom2  12229  fisum0diag2  12238  fsumconst  12245  modfsummodlemstep  12248  fsumabs  12256  fsumrelem  12262  fsumiun  12268  ntrivcvgap  12339  fprod2dlemstep  12413  fprodcnv  12416  fprodcom2fi  12417  fprodmodd  12432  nninfct  12842  algrf  12847  qredeu  12899  isprm2  12919  prmind2  12922  4sqlemafi  13202  4sqlem12  13209  ballotfilemcdc  13280  ballotfilemsf1o  13314  ballotfilem7  13336  ennnfonelemex  13362  ennnfonelemrn  13367  exmidunben  13374  ctinfom  13376  ctinf  13378  qnnen  13379  enctlem  13380  ctiunctlemfo  13387  slotslfn  13435  setscomd  13450  restfn  13655  elrest  13658  ptex  13676  prdsvallem  13679  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfnlemg  13693  fnpr2ob  13719  ismgm  13735  plusffng  13743  fn0g  13753  fngzsum  13766  gzsumsplit1r  13773  issgrp  13776  ismnddef  13789  gzsumcl  13862  mulgnngzsum  13988  subgintm  14059  releqgg  14081  eqgex  14082  eqgfval  14083  eqgval  14084  isghm  14104  gsumvalfi  14241  gsumsnfdcmn  14256  gsum2dfilem1  14270  gsum2dfilem2  14271  gsum2d2fi  14273  gsumcom2fi  14274  prdsex  14278  prdsval  14279  prdsbaslemss  14280  prdsbas  14282  fnmgp  14325  isrng  14339  isring  14410  ringn0  14471  opprrngbg  14491  opprsubgg  14498  opprunitd  14525  dfrhm2  14569  rhmex  14572  opprsubrngg  14627  subrngintm  14628  subrngpropd  14632  subrgpropd  14669  isdomn  14686  opprdomnbg  14691  scaffng  14754  rmodislmodlem  14795  rmodislmod  14796  lssex  14799  lsssn0  14815  lss1d  14828  lssintclm  14829  ellspsn  14862  rlmfn  14898  isridl  14949  blfn  14996  mopnset  14997  metuex  15000  znval  15079  znleval  15096  psrval  15160  fnpsr  15161  mplvalg  15222  fnmpl  15225  bastg  15304  distop  15328  topnex  15329  epttop  15333  tgrest  15412  resttopon  15414  restco  15417  cnrest2  15479  cnptopresti  15481  cnptoprest  15482  cnptoprest2  15483  txuni2  15499  txbas  15501  eltx  15502  txcnp  15514  txcnmpt  15516  txrest  15519  txdis1cn  15521  txlm  15522  cnmpt1st  15531  cnmpt2nd  15532  txhmeo  15562  txswaphmeolem  15563  xmetec  15680  metrest  15749  reldvg  15922  dvfgg  15931  dvcj  15952  dvmptfsum  15968  elply2  15978  pilem3  16027  prmorcht  16299  lgsquadlem1  16418  lgsquadlem2  16419  upgrex  16566  upgr1een  16587  umgredg  16608  umgredgnlp  16615  usgredgreu  16679  uspgredg2vtxeu  16681  ushgredgedg  16689  ushgredgedgloop  16691  griedg0ssusgr  16714  uhgrspansubgrlem  16739  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlk1walkdom  16822  eulerpathum  16944  depindlem1  16969  bdcvv  17105  bdsnss  17121  bdop  17123  bj-vprc  17144  bdinex1g  17149  bdssexg  17152  bj-inex  17155  bj-zfpair2  17158  bj-uniexg  17166  bdunexb  17168  bj-unexg  17169  bj-indint  17179  bj-ssom  17184  bj-om  17185  bj-2inf  17186  bj-bdfindis  17195  bj-nn0suc0  17198  bj-nnelirr  17201  bj-inf2vnlem1  17218  bj-inf2vnlem2  17219  bj-omex2  17225  bj-nn0sucALT  17226  bj-findis  17227  ss1oel2o  17239  domomsubct  17253  pw1nct  17255  nninfsellemeq  17280  exmidsbthrlem  17290