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  brtpos2  6526  reldmtpos  6528  dmtpos  6531  rntpos  6532  ovtposg  6534  dftpos3  6537  dftpos4  6538  tpostpos  6539  tpossym  6551  tfrlem3  6586  tfrlem5  6589  tfrlem8  6593  tfrlemisucfn  6599  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemibex  6604  tfrlemi14d  6608  tfrexlem  6609  tfr1onlem3  6613  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  tfrcl  6639  rdgtfr  6649  rdgruledefgg  6650  rdgivallem  6656  rdgon  6661  rdg0g  6663  frec0g  6672  frecabex  6673  frecabcl  6674  frectfr  6675  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  oafnex  6721  sucinc  6722  fnoa  6724  oaexg  6725  omfnex  6726  fnom  6727  omexg  6728  fnoei  6729  oeiexg  6730  oeiv  6733  oacl  6737  omcl  6738  oeicl  6739  oav2  6740  nnsucelsuc  6768  nnsucuniel  6772  ercnv  6832  iserd  6837  eqerlem  6842  eqer  6843  ecdmn0m  6855  erth  6857  qsss  6872  ecid  6876  ecidg  6877  qsid  6878  iinerm  6885  qsel  6890  erovlem  6905  ecopovsym  6909  ecopover  6911  th3qlem2  6916  mapprc  6930  fnmap  6933  fnpm  6934  mapdm0  6941  mapfset  6949  mapfoss  6951  fsetsspwxp  6952  fsetdmprc0  6954  mapval2  6963  mapsnd  6974  mapsn  6976  mapsncnv  6981  mapsnf1o2  6982  ixpconstg  6993  ixpprc  7005  ixpin  7009  ixpiinm  7010  ixpssmap2g  7013  ixpssmapg  7014  elixpsn  7021  ixpsnf1o  7022  bren  7034  brdomg  7036  domen  7039  domeng  7040  idssen  7067  domssr  7068  ener  7070  domtr  7076  ensn1g  7088  en1  7090  en1bg  7091  fundmen  7098  fundmeng  7099  mapsnend  7103  mapsnen  7104  fiprc  7108  unen  7109  rex2dom  7114  en2m  7117  dom1o  7120  xpsnen  7123  xpsneng  7124  xpcomco  7128  xpcomeng  7130  xpassen  7132  xpdom2  7133  xpdom2g  7134  pw2f1odc  7139  xpf1o  7148  mapen  7150  mapxpen  7152  xpmapenlem  7153  mapunen  7155  ssenen  7156  phplem4  7160  phplem3g  7161  nneneq  7162  php5  7163  phpm  7171  findcard  7196  findcard2  7197  findcard2s  7198  isinfinf  7205  ac6sfi  7206  exmidpw  7219  exmidpweq  7220  exmidpw2en  7223  unfidisj  7233  fiintim  7242  xpfi  7243  fisseneq  7246  ssfirab  7248  mapfi  7265  snexxph  7272  fidcenumlemr  7277  sbthlemi10  7288  isbth  7289  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  10009  cnref1o  10068  ioof  10390  fzpr  10501  frec2uzrand  10863  frec2uzf1od  10864  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  frecfzennn  10884  seqp1g  10924  seqclg  10930  seqf1og  10979  seqfeq4g  10989  ser3le  10995  hashinfom  11239  hashunlem  11266  hashun  11267  hashxp  11289  hashmap  11290  hashfibclem  11304  hashfacen  11306  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  zfz1isolem1  11314  zfz1iso  11315  fundm2domnop0  11322  wrdexb  11338  fnpfx  11471  cats1un  11515  wrdind  11516  wrd2ind  11517  shftfvalg  11605  ovshftex  11606  shftfibg  11607  shftfval  11608  shftfib  11610  shftfn  11611  2shfti  11618  shftvalg  11623  shftval4g  11624  maxabslemval  11997  fimaxre2  12016  xrmaxiflemval  12041  fclim  12085  climshft  12095  zsumdc  12176  fsum3  12179  fsum2dlemstep  12226  fsumcnv  12229  fisumcom2  12230  fisum0diag2  12239  fsumconst  12246  modfsummodlemstep  12249  fsumabs  12257  fsumrelem  12263  fsumiun  12269  ntrivcvgap  12340  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  fprodmodd  12433  nninfct  12843  algrf  12848  qredeu  12900  isprm2  12920  prmind2  12923  4sqlemafi  13203  4sqlem12  13210  ballotfilemcdc  13281  ballotfilemsf1o  13315  ballotfilem7  13337  ennnfonelemex  13363  ennnfonelemrn  13368  exmidunben  13375  ctinfom  13377  ctinf  13379  qnnen  13380  enctlem  13381  ctiunctlemfo  13388  slotslfn  13436  setscomd  13451  restfn  13656  elrest  13659  ptex  13677  prdsvallem  13680  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  fnpr2ob  13720  ismgm  13736  plusffng  13744  fn0g  13754  fngzsum  13767  gzsumsplit1r  13774  issgrp  13777  ismnddef  13790  gzsumcl  13863  mulgnngzsum  13989  subgintm  14060  releqgg  14082  eqgex  14083  eqgfval  14084  eqgval  14085  isghm  14105  gsumvalfi  14242  gsumsnfdcmn  14257  gsum2dfilem1  14271  gsum2dfilem2  14272  gsum2d2fi  14274  gsumcom2fi  14275  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  fnmgp  14326  isrng  14340  isring  14411  ringn0  14472  opprrngbg  14492  opprsubgg  14499  opprunitd  14526  dfrhm2  14570  rhmex  14573  opprsubrngg  14628  subrngintm  14629  subrngpropd  14633  subrgpropd  14670  isdomn  14687  opprdomnbg  14692  scaffng  14755  rmodislmodlem  14796  rmodislmod  14797  lssex  14800  lsssn0  14816  lss1d  14829  lssintclm  14830  ellspsn  14863  rlmfn  14899  isridl  14950  blfn  14997  mopnset  14998  metuex  15001  znval  15080  znleval  15097  psrval  15159  fnpsr  15160  mplvalcoe  15206  fnmpl  15209  bastg  15287  distop  15311  topnex  15312  epttop  15316  tgrest  15395  resttopon  15397  restco  15400  cnrest2  15462  cnptopresti  15464  cnptoprest  15465  cnptoprest2  15466  txuni2  15482  txbas  15484  eltx  15485  txcnp  15497  txcnmpt  15499  txrest  15502  txdis1cn  15504  txlm  15505  cnmpt1st  15514  cnmpt2nd  15515  txhmeo  15545  txswaphmeolem  15546  xmetec  15663  metrest  15732  reldvg  15905  dvfgg  15914  dvcj  15935  dvmptfsum  15951  elply2  15961  pilem3  16010  prmorcht  16282  lgsquadlem1  16401  lgsquadlem2  16402  upgrex  16549  upgr1een  16570  umgredg  16591  umgredgnlp  16598  usgredgreu  16662  uspgredg2vtxeu  16664  ushgredgedg  16672  ushgredgedgloop  16674  griedg0ssusgr  16697  uhgrspansubgrlem  16722  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlk1walkdom  16805  eulerpathum  16927  depindlem1  16952  bdcvv  17088  bdsnss  17104  bdop  17106  bj-vprc  17127  bdinex1g  17132  bdssexg  17135  bj-inex  17138  bj-zfpair2  17141  bj-uniexg  17149  bdunexb  17151  bj-unexg  17152  bj-indint  17162  bj-ssom  17167  bj-om  17168  bj-2inf  17169  bj-bdfindis  17178  bj-nn0suc0  17181  bj-nnelirr  17184  bj-inf2vnlem1  17201  bj-inf2vnlem2  17202  bj-omex2  17208  bj-nn0sucALT  17209  bj-findis  17210  ss1oel2o  17222  domomsubct  17236  pw1nct  17238  nninfsellemeq  17263  exmidsbthrlem  17273