Theorem vex 2803

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

Syntax hints:   e. wcel 2200   _Vcvv 2800

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  elv  2804  elvd  2805  el2v  2806  isset  2807  eqvisset  2811  ralv  2818  rexv  2819  reuv  2820  rmov  2821  rabab  2822  sbhypf  2851  ceqex  2931  ralab  2964  rexab  2966  mo2icl  2983  reu8  3000  csbvarg  3153  csbiebg  3168  sbcnestgf  3177  sbnfc2  3186  ddifnel  3336  ddifstab  3337  csbing  3412  unssdif  3440  unssin  3444  inssun  3445  invdif  3447  vn0  3503  vn0m  3504  eqv  3512  abvor0dc  3516  sbss  3600  velpw  3657  elpwg  3658  velsn  3684  vsnid  3699  exsnrex  3709  dftp2  3716  prmg  3792  prnzg  3795  snssgOLD  3807  difprsnss  3809  sneqrg  3843  preq12bg  3854  pwprss  3887  pwtpss  3888  pwv  3890  unipr  3905  uniprg  3906  unisng  3908  elintg  3934  elintrabg  3939  intss1  3941  ssint  3942  intmin  3946  intss  3947  intssunim  3948  intmin4  3954  intab  3955  intun  3957  intpr  3958  intprg  3959  uniintsnr  3962  iinconstm  3977  iuniin  3978  iinss1  3980  dfiin2g  4001  dfiunv2  4004  ssiinf  4018  iinss  4020  iinss2  4021  0iin  4027  iinab  4030  iundif2ss  4034  iindif2m  4036  iinin2m  4037  iinuniss  4051  sspwuni  4053  pwpwab  4056  iinpw  4059  iunpwss  4060  brab1  4134  csbopabg  4165  mptv  4184  trint  4200  vnex  4218  inex1g  4223  ssexg  4226  inteximm  4237  inuni  4243  repizf2  4250  axpweq  4259  bnd2  4261  pwuni  4280  exmidundif  4294  exmidundifim  4295  zfpair2  4298  rext  4305  sspwb  4306  unipw  4307  ssextss  4310  euabex  4315  mss  4316  exss  4317  opth  4327  opthg  4328  copsexg  4334  copsex4g  4337  moop2  4342  euotd  4345  opabid  4348  elopab  4350  opelopabsbALT  4351  opelopabsb  4352  opabm  4373  pwin  4377  pwunss  4378  epelg  4385  epel  4387  pofun  4407  epse  4437  tron  4477  sucel  4505  suctr  4516  vuniex  4533  uniexg  4534  unexb  4537  snnex  4543  pwnex  4544  uniuni  4546  eusvnf  4548  eusvnfb  4549  iunpw  4575  unon  4607  ordunisuc2r  4610  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  ordsucunielexmid  4627  elirr  4637  en2lp  4650  dtruex  4655  onintexmid  4669  reg3exmidlemwe  4675  dcextest  4677  finds  4696  finds2  4697  elomssom  4701  limom  4710  0nelxp  4751  opelxp  4753  opeliunxp  4779  elvv  4786  elvvv  4787  elvvuni  4788  xpsspw  4836  relopabiv  4851  relopabi  4853  opabid2  4859  difopab  4861  xpiindim  4865  raliunxp  4869  rexiunxp  4870  ralxpf  4874  rexxpf  4875  relop  4878  cnvco  4913  dfrn2  4916  dfdm4  4921  dmss  4928  dmin  4937  dmiun  4938  dmuni  4939  dm0  4943  dmi  4944  reldm0  4947  reldmm  4948  elreldm  4956  elrnmpt1  4981  dmrnssfld  4993  dmcoss  5000  dmcosseq  5002  opelresg  5018  resieq  5021  dmres  5032  elres  5047  relssres  5049  resopab  5055  resiexg  5056  iss  5057  dfres2  5063  restidsing  5067  dfima2  5076  imadmrn  5084  imai  5090  csbima12g  5095  elimasng  5102  args  5103  epini  5105  iniseg  5106  dfse2  5107  exse2  5108  cotr  5116  issref  5117  cnvsym  5118  intasym  5119  asymref  5120  intirr  5121  brcodir  5122  codir  5123  qfto  5124  poirr2  5127  cnvopab  5136  cnv0  5138  cnvi  5139  cnvdif  5141  rniun  5145  dminss  5149  imainss  5150  inimasn  5152  xpmlem  5155  dmxpss  5165  rnxpid  5169  ssrnres  5177  rninxp  5178  dminxp  5179  cnvcnv3  5184  dfrel2  5185  dmsnm  5200  dmsnopg  5206  cnvcnvsn  5211  dmsnsnsng  5212  cnvsng  5220  elxp4  5222  elxp5  5223  cnvresima  5224  dfco2  5234  dfco2a  5235  cores  5238  resco  5239  imaco  5240  rnco  5241  coiun  5244  co02  5248  coi1  5250  coass  5253  relssdmrn  5255  unielrel  5262  ressn  5275  cnviinm  5276  cnvpom  5277  cnvsom  5278  uniabio  5295  iotaval  5296  iotass  5302  sniota  5315  csbiotag  5317  dffun2  5334  dffun7  5351  dffun8  5352  dffun9  5353  funopg  5358  funssres  5366  funun  5368  funcnvsn  5372  funinsn  5376  funcnv2  5387  funcnv  5388  funcnv3  5389  funcnveq  5390  fun2cnv  5391  funcnvuni  5396  imadif  5407  funimaexglem  5410  isarep1  5413  2elresin  5440  fnres  5446  fcnvres  5517  fconstg  5530  fun11iun  5601  f1osng  5622  dffv3g  5631  fvssunirng  5650  sefvex  5656  fv3  5658  fvres  5659  nfunsn  5672  funimass4  5692  ssimaexg  5704  dmfco  5710  fvopab6  5739  fndmdif  5748  fvelrn  5774  dffo4  5791  f1ompt  5794  fmptco  5809  fsn  5815  fsng  5816  dfmpt  5820  dfmptg  5822  funopsn  5825  funop  5826  funopdmsn  5829  fnressn  5835  fressnfv  5836  fvsng  5845  resfunexg  5870  funfvima3  5883  idref  5892  abrexco  5895  imaiun  5896  dff13  5904  foeqcnvco  5926  f1eqcocnv  5927  fliftcnv  5931  isocnv2  5948  isoini  5954  isose  5957  riotav  5972  csbriotag  5980  acexmidlem2  6010  oprabid  6045  csbov123g  6052  0neqopab  6061  brabvv  6062  dfoprab2  6063  rnoprab  6099  eloprabga  6103  mpov  6106  f1opw  6225  opabex3d  6278  opabex3  6279  ofmres  6293  uchoice  6295  op1stg  6308  op2ndg  6309  1stval2  6313  2ndval2  6314  fo1st  6315  fo2nd  6316  f1stres  6317  f2ndres  6318  fo1stresm  6319  fo2ndresm  6320  xp1st  6323  xp2nd  6324  releldm2  6343  reldm  6344  sbcopeq1a  6345  csbopeq1a  6346  dfoprab3  6349  opabn1stprc  6353  eloprabi  6356  mpomptsx  6357  dmmpossx  6359  fmpox  6360  mpofvex  6365  mpoexxg  6370  fmpoco  6376  df1st2  6379  df2nd2  6380  1stconst  6381  2ndconst  6382  dfmpo  6383  fo2ndf  6387  f1o2ndf1  6388  xporderlem  6391  cnvoprab  6394  f1od2  6395  brtpos2  6412  reldmtpos  6414  dmtpos  6417  rntpos  6418  ovtposg  6420  dftpos3  6423  dftpos4  6424  tpostpos  6425  tpossym  6437  tfrlem3  6472  tfrlem5  6475  tfrlem8  6479  tfrlemisucfn  6485  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemibex  6490  tfrlemi14d  6494  tfrexlem  6495  tfr1onlem3  6499  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  tfrcl  6525  rdgtfr  6535  rdgruledefgg  6536  rdgivallem  6542  rdgon  6547  rdg0g  6549  frec0g  6558  frecabex  6559  frecabcl  6560  frectfr  6561  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  oafnex  6607  sucinc  6608  fnoa  6610  oaexg  6611  omfnex  6612  fnom  6613  omexg  6614  fnoei  6615  oeiexg  6616  oeiv  6619  oacl  6623  omcl  6624  oeicl  6625  oav2  6626  nnsucelsuc  6654  nnsucuniel  6658  ercnv  6718  iserd  6723  eqerlem  6728  eqer  6729  ecdmn0m  6741  erth  6743  qsss  6758  ecid  6762  ecidg  6763  qsid  6764  iinerm  6771  qsel  6776  erovlem  6791  ecopovsym  6795  ecopover  6797  th3qlem2  6802  mapprc  6816  fnmap  6819  fnpm  6820  mapdm0  6827  mapval2  6842  mapsn  6854  mapsncnv  6859  mapsnf1o2  6860  ixpconstg  6871  ixpprc  6883  ixpin  6887  ixpiinm  6888  ixpssmap2g  6891  ixpssmapg  6892  elixpsn  6899  ixpsnf1o  6900  bren  6912  brdomg  6914  domen  6917  domeng  6918  idssen  6945  domssr  6946  ener  6948  domtr  6954  ensn1g  6966  en1  6968  en1bg  6969  fundmen  6976  fundmeng  6977  mapsnen  6981  fiprc  6985  unen  6986  rex2dom  6991  en2m  6994  dom1o  6997  xpsnen  7000  xpsneng  7001  xpcomco  7005  xpcomeng  7007  xpassen  7009  xpdom2  7010  xpdom2g  7011  pw2f1odc  7016  xpf1o  7025  mapen  7027  mapxpen  7029  xpmapenlem  7030  ssenen  7032  phplem4  7036  phplem3g  7037  nneneq  7038  php5  7039  phpm  7047  findcard  7070  findcard2  7071  findcard2s  7072  isinfinf  7079  ac6sfi  7080  exmidpw  7093  exmidpweq  7094  exmidpw2en  7097  unfidisj  7107  fiintim  7116  xpfi  7117  fisseneq  7119  ssfirab  7121  snexxph  7140  fidcenumlemr  7145  sbthlemi10  7156  isbth  7157  ssfii  7164  fi0  7165  fiss  7167  cnvinfex  7208  eqinfti  7210  infvalti  7212  infglbti  7215  infmoti  7218  ordiso2  7225  djuf1olem  7243  djuss  7260  ctm  7299  ctssdccl  7301  ctssdclemr  7302  finomni  7330  exmidomni  7332  fodjuomnilemdc  7334  nninfwlpoimlemginf  7366  pm54.43  7386  pr2cv1  7391  exmidfodomrlemim  7402  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  finacn  7409  acfun  7412  ccfunen  7473  cc2lem  7475  cc3  7477  acnccim  7481  indpi  7552  dfplpq2  7564  enq0sym  7642  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  nqnq0  7651  mulnnnq0  7660  nqprm  7752  nqprrnd  7753  nqprdisj  7754  nqprloc  7755  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemrl  7783  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  ltnqpr  7803  ltnqpri  7804  archpr  7853  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlem2  7870  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemopu  7909  suplocexprlemmu  7928  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  cnm  8042  ltresr  8049  peano1nnnn  8062  peano2nnnn  8063  axcnre  8091  axpre-apti  8095  renfdisj  8229  dfinfre  9126  1nn  9144  peano2nn  9145  indstr  9817  cnref1o  9875  ioof  10196  fzpr  10302  frec2uzrand  10657  frec2uzf1od  10658  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  frecfzennn  10678  seqp1g  10718  seqclg  10724  seqf1og  10773  seqfeq4g  10783  ser3le  10789  hashinfom  11030  hashunlem  11057  hashun  11058  hashxp  11080  hashfacen  11090  zfz1isolem1  11094  zfz1iso  11095  fundm2domnop0  11099  wrdexb  11115  fnpfx  11248  cats1un  11292  wrdind  11293  wrd2ind  11294  shftfvalg  11369  ovshftex  11370  shftfibg  11371  shftfval  11372  shftfib  11374  shftfn  11375  2shfti  11382  shftvalg  11387  shftval4g  11388  maxabslemval  11759  fimaxre2  11778  xrmaxiflemval  11801  fclim  11845  climshft  11855  zsumdc  11935  fsum3  11938  fsum2dlemstep  11985  fsumcnv  11988  fisumcom2  11989  fisum0diag2  11998  fsumconst  12005  modfsummodlemstep  12008  fsumabs  12016  fsumrelem  12022  fsumiun  12028  ntrivcvgap  12099  fprod2dlemstep  12173  fprodcnv  12176  fprodcom2fi  12177  fprodmodd  12192  nninfct  12602  algrf  12607  qredeu  12659  isprm2  12679  prmind2  12682  4sqlemafi  12958  4sqlem12  12965  ennnfonelemex  13025  ennnfonelemrn  13030  exmidunben  13037  ctinfom  13039  ctinf  13041  qnnen  13042  enctlem  13043  ctiunctlemfo  13050  slotslfn  13098  setscomd  13113  restfn  13316  elrest  13319  ptex  13337  prdsex  13342  prdsvallem  13345  prdsval  13346  prdsbaslemss  13347  prdsbas  13349  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfnlemg  13387  fnpr2ob  13413  ismgm  13430  plusffng  13438  fn0g  13448  fngsum  13461  gsumsplit1r  13471  gsumprval  13472  issgrp  13476  ismnddef  13491  gsumfzz  13568  gsumfzcl  13572  mulgnngsum  13704  subgintm  13775  releqgg  13797  eqgex  13798  eqgfval  13799  eqgval  13800  isghm  13820  fnmgp  13925  isrng  13937  isring  14003  ringn0  14063  opprrngbg  14081  opprsubgg  14087  opprunitd  14114  dfrhm2  14158  rhmex  14161  opprsubrngg  14215  subrngintm  14216  subrngpropd  14220  subrgpropd  14257  isdomn  14273  opprdomnbg  14278  scaffng  14313  rmodislmodlem  14354  rmodislmod  14355  lssex  14358  lsssn0  14374  lss1d  14387  lssintclm  14388  ellspsn  14421  rlmfn  14457  isridl  14508  blfn  14555  mopnset  14556  metuex  14559  znval  14640  znleval  14657  psrval  14670  fnpsr  14671  mplvalcoe  14694  fnmpl  14697  bastg  14775  distop  14799  topnex  14800  epttop  14804  tgrest  14883  resttopon  14885  restco  14888  cnrest2  14950  cnptopresti  14952  cnptoprest  14953  cnptoprest2  14954  txuni2  14970  txbas  14972  eltx  14973  txcnp  14985  txcnmpt  14987  txrest  14990  txdis1cn  14992  txlm  14993  cnmpt1st  15002  cnmpt2nd  15003  txhmeo  15033  txswaphmeolem  15034  xmetec  15151  metrest  15220  reldvg  15393  dvfgg  15402  dvcj  15423  dvmptfsum  15439  elply2  15449  pilem3  15497  lgsquadlem1  15796  lgsquadlem2  15797  upgrex  15944  umgredg  15984  umgredgnlp  15991  usgredgreu  16055  uspgredg2vtxeu  16057  ushgredgedg  16065  ushgredgedgloop  16067  griedg0ssusgr  16090  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlk1walkdom  16156  bdcvv  16388  bdsnss  16404  bdop  16406  bj-vprc  16427  bdinex1g  16432  bdssexg  16435  bj-inex  16438  bj-zfpair2  16441  bj-uniexg  16449  bdunexb  16451  bj-unexg  16452  bj-indint  16462  bj-ssom  16467  bj-om  16468  bj-2inf  16469  bj-bdfindis  16478  bj-nn0suc0  16481  bj-nnelirr  16484  bj-inf2vnlem1  16501  bj-inf2vnlem2  16502  bj-omex2  16508  bj-nn0sucALT  16509  bj-findis  16510  ss1oel2o  16522  domomsubct  16538  pw1nct  16540  nninfsellemeq  16552  exmidsbthrlem  16562