Theorem vex 2802

Description: All setvar variables are sets (see isset 2806). 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 2801	. . 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 2799

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 2801

This theorem is referenced by:  elv  2803  elvd  2804  el2v  2805  isset  2806  eqvisset  2810  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rabab  2821  sbhypf  2850  ceqex  2930  ralab  2963  rexab  2965  mo2icl  2982  reu8  2999  csbvarg  3152  csbiebg  3167  sbcnestgf  3176  sbnfc2  3185  ddifnel  3335  ddifstab  3336  csbing  3411  unssdif  3439  unssin  3443  inssun  3444  invdif  3446  vn0  3502  vn0m  3503  eqv  3511  abvor0dc  3515  sbss  3599  velpw  3656  elpwg  3657  velsn  3683  vsnid  3698  exsnrex  3708  dftp2  3715  prmg  3788  prnzg  3791  snssgOLD  3803  difprsnss  3805  sneqrg  3839  preq12bg  3850  pwprss  3883  pwtpss  3884  pwv  3886  unipr  3901  uniprg  3902  unisng  3904  elintg  3930  elintrabg  3935  intss1  3937  ssint  3938  intmin  3942  intss  3943  intssunim  3944  intmin4  3950  intab  3951  intun  3953  intpr  3954  intprg  3955  uniintsnr  3958  iinconstm  3973  iuniin  3974  iinss1  3976  dfiin2g  3997  dfiunv2  4000  ssiinf  4014  iinss  4016  iinss2  4017  0iin  4023  iinab  4026  iundif2ss  4030  iindif2m  4032  iinin2m  4033  iinuniss  4047  sspwuni  4049  pwpwab  4052  iinpw  4055  iunpwss  4056  brab1  4130  csbopabg  4161  mptv  4180  trint  4196  vnex  4214  inex1g  4219  ssexg  4222  inteximm  4232  inuni  4238  repizf2  4245  axpweq  4254  bnd2  4256  pwuni  4275  exmidundif  4289  exmidundifim  4290  zfpair2  4293  rext  4300  sspwb  4301  unipw  4302  ssextss  4305  euabex  4310  mss  4311  exss  4312  opth  4322  opthg  4323  copsexg  4329  copsex4g  4332  moop2  4337  euotd  4340  opabid  4343  elopab  4345  opelopabsbALT  4346  opelopabsb  4347  opabm  4368  pwin  4372  pwunss  4373  epelg  4380  epel  4382  pofun  4402  epse  4432  tron  4472  sucel  4500  suctr  4511  vuniex  4528  uniexg  4529  unexb  4532  snnex  4538  pwnex  4539  uniuni  4541  eusvnf  4543  eusvnfb  4544  iunpw  4570  unon  4602  ordunisuc2r  4605  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  ordsucunielexmid  4622  elirr  4632  en2lp  4645  dtruex  4650  onintexmid  4664  reg3exmidlemwe  4670  dcextest  4672  finds  4691  finds2  4692  elomssom  4696  limom  4705  0nelxp  4746  opelxp  4748  opeliunxp  4773  elvv  4780  elvvv  4781  elvvuni  4782  xpsspw  4830  relopabiv  4844  relopabi  4846  opabid2  4852  difopab  4854  xpiindim  4858  raliunxp  4862  rexiunxp  4863  ralxpf  4867  rexxpf  4868  relop  4871  cnvco  4906  dfrn2  4909  dfdm4  4914  dmss  4921  dmin  4930  dmiun  4931  dmuni  4932  dm0  4936  dmi  4937  reldm0  4940  reldmm  4941  elreldm  4949  elrnmpt1  4974  dmrnssfld  4986  dmcoss  4993  dmcosseq  4995  opelresg  5011  resieq  5014  dmres  5025  elres  5040  relssres  5042  resopab  5048  resiexg  5049  iss  5050  dfres2  5056  restidsing  5060  dfima2  5069  imadmrn  5077  imai  5083  csbima12g  5088  elimasng  5095  args  5096  epini  5098  iniseg  5099  dfse2  5100  exse2  5101  cotr  5109  issref  5110  cnvsym  5111  intasym  5112  asymref  5113  intirr  5114  brcodir  5115  codir  5116  qfto  5117  poirr2  5120  cnvopab  5129  cnv0  5131  cnvi  5132  cnvdif  5134  rniun  5138  dminss  5142  imainss  5143  inimasn  5145  xpmlem  5148  dmxpss  5158  rnxpid  5162  ssrnres  5170  rninxp  5171  dminxp  5172  cnvcnv3  5177  dfrel2  5178  dmsnm  5193  dmsnopg  5199  cnvcnvsn  5204  dmsnsnsng  5205  cnvsng  5213  elxp4  5215  elxp5  5216  cnvresima  5217  dfco2  5227  dfco2a  5228  cores  5231  resco  5232  imaco  5233  rnco  5234  coiun  5237  co02  5241  coi1  5243  coass  5246  relssdmrn  5248  unielrel  5255  ressn  5268  cnviinm  5269  cnvpom  5270  cnvsom  5271  uniabio  5288  iotaval  5289  iotass  5295  sniota  5308  csbiotag  5310  dffun2  5327  dffun7  5344  dffun8  5345  dffun9  5346  funopg  5351  funssres  5359  funun  5361  funcnvsn  5365  funinsn  5369  funcnv2  5380  funcnv  5381  funcnv3  5382  funcnveq  5383  fun2cnv  5384  funcnvuni  5389  imadif  5400  funimaexglem  5403  isarep1  5406  2elresin  5433  fnres  5439  fcnvres  5508  fconstg  5521  fun11iun  5592  f1osng  5613  dffv3g  5622  fvssunirng  5641  sefvex  5647  fv3  5649  fvres  5650  nfunsn  5663  funimass4  5683  ssimaexg  5695  dmfco  5701  fvopab6  5730  fndmdif  5739  fvelrn  5765  dffo4  5782  f1ompt  5785  fmptco  5800  fsn  5806  fsng  5807  dfmpt  5811  dfmptg  5813  funopsn  5816  funop  5817  funopdmsn  5818  fnressn  5824  fressnfv  5825  fvsng  5834  resfunexg  5859  funfvima3  5872  idref  5879  abrexco  5882  imaiun  5883  dff13  5891  foeqcnvco  5913  f1eqcocnv  5914  fliftcnv  5918  isocnv2  5935  isoini  5941  isose  5944  riotav  5959  csbriotag  5967  acexmidlem2  5997  oprabid  6032  csbov123g  6039  0neqopab  6048  brabvv  6049  dfoprab2  6050  rnoprab  6086  eloprabga  6090  mpov  6093  f1opw  6211  opabex3d  6264  opabex3  6265  ofmres  6279  uchoice  6281  op1stg  6294  op2ndg  6295  1stval2  6299  2ndval2  6300  fo1st  6301  fo2nd  6302  f1stres  6303  f2ndres  6304  fo1stresm  6305  fo2ndresm  6306  xp1st  6309  xp2nd  6310  releldm2  6329  reldm  6330  sbcopeq1a  6331  csbopeq1a  6332  dfoprab3  6335  eloprabi  6340  mpomptsx  6341  dmmpossx  6343  fmpox  6344  mpofvex  6349  mpoexxg  6354  fmpoco  6360  df1st2  6363  df2nd2  6364  1stconst  6365  2ndconst  6366  dfmpo  6367  fo2ndf  6371  f1o2ndf1  6372  xporderlem  6375  cnvoprab  6378  f1od2  6379  brtpos2  6395  reldmtpos  6397  dmtpos  6400  rntpos  6401  ovtposg  6403  dftpos3  6406  dftpos4  6407  tpostpos  6408  tpossym  6420  tfrlem3  6455  tfrlem5  6458  tfrlem8  6462  tfrlemisucfn  6468  tfrlemisucaccv  6469  tfrlemibxssdm  6471  tfrlemibfn  6472  tfrlemibex  6473  tfrlemi14d  6477  tfrexlem  6478  tfr1onlem3  6482  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemres  6493  tfri1dALT  6495  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemres  6506  tfrcl  6508  rdgtfr  6518  rdgruledefgg  6519  rdgivallem  6525  rdgon  6530  rdg0g  6532  frec0g  6541  frecabex  6542  frecabcl  6543  frectfr  6544  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecrdg  6552  oafnex  6588  sucinc  6589  fnoa  6591  oaexg  6592  omfnex  6593  fnom  6594  omexg  6595  fnoei  6596  oeiexg  6597  oeiv  6600  oacl  6604  omcl  6605  oeicl  6606  oav2  6607  nnsucelsuc  6635  nnsucuniel  6639  ercnv  6699  iserd  6704  eqerlem  6709  eqer  6710  ecdmn0m  6722  erth  6724  qsss  6739  ecid  6743  ecidg  6744  qsid  6745  iinerm  6752  qsel  6757  erovlem  6772  ecopovsym  6776  ecopover  6778  th3qlem2  6783  mapprc  6797  fnmap  6800  fnpm  6801  mapdm0  6808  mapval2  6823  mapsn  6835  mapsncnv  6840  mapsnf1o2  6841  ixpconstg  6852  ixpprc  6864  ixpin  6868  ixpiinm  6869  ixpssmap2g  6872  ixpssmapg  6873  elixpsn  6880  ixpsnf1o  6881  bren  6893  brdomg  6895  domen  6898  domeng  6899  idssen  6926  domssr  6927  ener  6929  domtr  6935  ensn1g  6947  en1  6949  en1bg  6950  fundmen  6957  fundmeng  6958  mapsnen  6962  fiprc  6966  unen  6967  rex2dom  6969  en2m  6972  xpsnen  6976  xpsneng  6977  xpcomco  6981  xpcomeng  6983  xpassen  6985  xpdom2  6986  xpdom2g  6987  pw2f1odc  6992  xpf1o  7001  mapen  7003  mapxpen  7005  xpmapenlem  7006  ssenen  7008  phplem4  7012  phplem3g  7013  nneneq  7014  php5  7015  phpm  7023  findcard  7046  findcard2  7047  findcard2s  7048  isinfinf  7055  ac6sfi  7056  exmidpw  7066  exmidpweq  7067  exmidpw2en  7070  unfidisj  7080  fiintim  7089  xpfi  7090  fisseneq  7092  ssfirab  7094  snexxph  7113  fidcenumlemr  7118  sbthlemi10  7129  isbth  7130  ssfii  7137  fi0  7138  fiss  7140  cnvinfex  7181  eqinfti  7183  infvalti  7185  infglbti  7188  infmoti  7191  ordiso2  7198  djuf1olem  7216  djuss  7233  ctm  7272  ctssdccl  7274  ctssdclemr  7275  finomni  7303  exmidomni  7305  fodjuomnilemdc  7307  nninfwlpoimlemginf  7339  pm54.43  7359  pr2cv1  7364  exmidfodomrlemim  7375  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  finacn  7382  acfun  7385  ccfunen  7446  cc2lem  7448  cc3  7450  acnccim  7454  indpi  7525  dfplpq2  7537  enq0sym  7615  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  nqnq0  7624  mulnnnq0  7633  nqprm  7725  nqprrnd  7726  nqprdisj  7727  nqprloc  7728  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  ltnqpr  7776  ltnqpri  7777  archpr  7826  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlem2  7843  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemopu  7882  suplocexprlemmu  7901  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  cnm  8015  ltresr  8022  peano1nnnn  8035  peano2nnnn  8036  axcnre  8064  axpre-apti  8068  renfdisj  8202  dfinfre  9099  1nn  9117  peano2nn  9118  indstr  9784  cnref1o  9842  ioof  10163  fzpr  10269  frec2uzrand  10622  frec2uzf1od  10623  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  frecfzennn  10643  seqp1g  10683  seqclg  10689  seqf1og  10738  seqfeq4g  10748  ser3le  10754  hashinfom  10995  hashunlem  11021  hashun  11022  hashxp  11043  hashfacen  11053  zfz1isolem1  11057  zfz1iso  11058  fundm2domnop0  11062  wrdexb  11078  fnpfx  11204  cats1un  11248  wrdind  11249  wrd2ind  11250  shftfvalg  11324  ovshftex  11325  shftfibg  11326  shftfval  11327  shftfib  11329  shftfn  11330  2shfti  11337  shftvalg  11342  shftval4g  11343  maxabslemval  11714  fimaxre2  11733  xrmaxiflemval  11756  fclim  11800  climshft  11810  zsumdc  11890  fsum3  11893  fsum2dlemstep  11940  fsumcnv  11943  fisumcom2  11944  fisum0diag2  11953  fsumconst  11960  modfsummodlemstep  11963  fsumabs  11971  fsumrelem  11977  fsumiun  11983  ntrivcvgap  12054  fprod2dlemstep  12128  fprodcnv  12131  fprodcom2fi  12132  fprodmodd  12147  nninfct  12557  algrf  12562  qredeu  12614  isprm2  12634  prmind2  12637  4sqlemafi  12913  4sqlem12  12920  ennnfonelemex  12980  ennnfonelemrn  12985  exmidunben  12992  ctinfom  12994  ctinf  12996  qnnen  12997  enctlem  12998  ctiunctlemfo  13005  slotslfn  13053  setscomd  13068  restfn  13271  elrest  13274  ptex  13292  prdsex  13297  prdsvallem  13300  prdsval  13301  prdsbaslemss  13302  prdsbas  13304  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfnlemg  13342  fnpr2ob  13368  ismgm  13385  plusffng  13393  fn0g  13403  fngsum  13416  gsumsplit1r  13426  gsumprval  13427  issgrp  13431  ismnddef  13446  gsumfzz  13523  gsumfzcl  13527  mulgnngsum  13659  subgintm  13730  releqgg  13752  eqgex  13753  eqgfval  13754  eqgval  13755  isghm  13775  fnmgp  13880  isrng  13892  isring  13958  ringn0  14018  opprrngbg  14036  opprsubgg  14042  opprunitd  14068  dfrhm2  14112  rhmex  14115  opprsubrngg  14169  subrngintm  14170  subrngpropd  14174  subrgpropd  14211  isdomn  14227  opprdomnbg  14232  scaffng  14267  rmodislmodlem  14308  rmodislmod  14309  lssex  14312  lsssn0  14328  lss1d  14341  lssintclm  14342  ellspsn  14375  rlmfn  14411  isridl  14462  blfn  14509  mopnset  14510  metuex  14513  znval  14594  znleval  14611  psrval  14624  fnpsr  14625  mplvalcoe  14648  fnmpl  14651  bastg  14729  distop  14753  topnex  14754  epttop  14758  tgrest  14837  resttopon  14839  restco  14842  cnrest2  14904  cnptopresti  14906  cnptoprest  14907  cnptoprest2  14908  txuni2  14924  txbas  14926  eltx  14927  txcnp  14939  txcnmpt  14941  txrest  14944  txdis1cn  14946  txlm  14947  cnmpt1st  14956  cnmpt2nd  14957  txhmeo  14987  txswaphmeolem  14988  xmetec  15105  metrest  15174  reldvg  15347  dvfgg  15356  dvcj  15377  dvmptfsum  15393  elply2  15403  pilem3  15451  lgsquadlem1  15750  lgsquadlem2  15751  upgrex  15897  umgredg  15937  umgredgnlp  15944  usgredgreu  16008  uspgredg2vtxeu  16010  ushgredgedg  16018  ushgredgedgloop  16020  wlkvtxiedgg  16042  bdcvv  16178  bdsnss  16194  bdop  16196  bj-vprc  16217  bdinex1g  16222  bdssexg  16225  bj-inex  16228  bj-zfpair2  16231  bj-uniexg  16239  bdunexb  16241  bj-unexg  16242  bj-indint  16252  bj-ssom  16257  bj-om  16258  bj-2inf  16259  bj-bdfindis  16268  bj-nn0suc0  16271  bj-nnelirr  16274  bj-inf2vnlem1  16291  bj-inf2vnlem2  16292  bj-omex2  16298  bj-nn0sucALT  16299  bj-findis  16300  ss1oel2o  16313  dom1o  16314  domomsubct  16326  pw1nct  16328  nninfsellemeq  16339  exmidsbthrlem  16349