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  3790  prnzg  3793  snssgOLD  3805  difprsnss  3807  sneqrg  3841  preq12bg  3852  pwprss  3885  pwtpss  3886  pwv  3888  unipr  3903  uniprg  3904  unisng  3906  elintg  3932  elintrabg  3937  intss1  3939  ssint  3940  intmin  3944  intss  3945  intssunim  3946  intmin4  3952  intab  3953  intun  3955  intpr  3956  intprg  3957  uniintsnr  3960  iinconstm  3975  iuniin  3976  iinss1  3978  dfiin2g  3999  dfiunv2  4002  ssiinf  4016  iinss  4018  iinss2  4019  0iin  4025  iinab  4028  iundif2ss  4032  iindif2m  4034  iinin2m  4035  iinuniss  4049  sspwuni  4051  pwpwab  4054  iinpw  4057  iunpwss  4058  brab1  4132  csbopabg  4163  mptv  4182  trint  4198  vnex  4216  inex1g  4221  ssexg  4224  inteximm  4235  inuni  4241  repizf2  4248  axpweq  4257  bnd2  4259  pwuni  4278  exmidundif  4292  exmidundifim  4293  zfpair2  4296  rext  4303  sspwb  4304  unipw  4305  ssextss  4308  euabex  4313  mss  4314  exss  4315  opth  4325  opthg  4326  copsexg  4332  copsex4g  4335  moop2  4340  euotd  4343  opabid  4346  elopab  4348  opelopabsbALT  4349  opelopabsb  4350  opabm  4371  pwin  4375  pwunss  4376  epelg  4383  epel  4385  pofun  4405  epse  4435  tron  4475  sucel  4503  suctr  4514  vuniex  4531  uniexg  4532  unexb  4535  snnex  4541  pwnex  4542  uniuni  4544  eusvnf  4546  eusvnfb  4547  iunpw  4573  unon  4605  ordunisuc2r  4608  ordtri2or2exmidlem  4620  onsucelsucexmidlem  4623  ordsucunielexmid  4625  elirr  4635  en2lp  4648  dtruex  4653  onintexmid  4667  reg3exmidlemwe  4673  dcextest  4675  finds  4694  finds2  4695  elomssom  4699  limom  4708  0nelxp  4749  opelxp  4751  opeliunxp  4777  elvv  4784  elvvv  4785  elvvuni  4786  xpsspw  4834  relopabiv  4849  relopabi  4851  opabid2  4857  difopab  4859  xpiindim  4863  raliunxp  4867  rexiunxp  4868  ralxpf  4872  rexxpf  4873  relop  4876  cnvco  4911  dfrn2  4914  dfdm4  4919  dmss  4926  dmin  4935  dmiun  4936  dmuni  4937  dm0  4941  dmi  4942  reldm0  4945  reldmm  4946  elreldm  4954  elrnmpt1  4979  dmrnssfld  4991  dmcoss  4998  dmcosseq  5000  opelresg  5016  resieq  5019  dmres  5030  elres  5045  relssres  5047  resopab  5053  resiexg  5054  iss  5055  dfres2  5061  restidsing  5065  dfima2  5074  imadmrn  5082  imai  5088  csbima12g  5093  elimasng  5100  args  5101  epini  5103  iniseg  5104  dfse2  5105  exse2  5106  cotr  5114  issref  5115  cnvsym  5116  intasym  5117  asymref  5118  intirr  5119  brcodir  5120  codir  5121  qfto  5122  poirr2  5125  cnvopab  5134  cnv0  5136  cnvi  5137  cnvdif  5139  rniun  5143  dminss  5147  imainss  5148  inimasn  5150  xpmlem  5153  dmxpss  5163  rnxpid  5167  ssrnres  5175  rninxp  5176  dminxp  5177  cnvcnv3  5182  dfrel2  5183  dmsnm  5198  dmsnopg  5204  cnvcnvsn  5209  dmsnsnsng  5210  cnvsng  5218  elxp4  5220  elxp5  5221  cnvresima  5222  dfco2  5232  dfco2a  5233  cores  5236  resco  5237  imaco  5238  rnco  5239  coiun  5242  co02  5246  coi1  5248  coass  5251  relssdmrn  5253  unielrel  5260  ressn  5273  cnviinm  5274  cnvpom  5275  cnvsom  5276  uniabio  5293  iotaval  5294  iotass  5300  sniota  5313  csbiotag  5315  dffun2  5332  dffun7  5349  dffun8  5350  dffun9  5351  funopg  5356  funssres  5364  funun  5366  funcnvsn  5370  funinsn  5374  funcnv2  5385  funcnv  5386  funcnv3  5387  funcnveq  5388  fun2cnv  5389  funcnvuni  5394  imadif  5405  funimaexglem  5408  isarep1  5411  2elresin  5438  fnres  5444  fcnvres  5515  fconstg  5528  fun11iun  5599  f1osng  5620  dffv3g  5629  fvssunirng  5648  sefvex  5654  fv3  5656  fvres  5657  nfunsn  5670  funimass4  5690  ssimaexg  5702  dmfco  5708  fvopab6  5737  fndmdif  5746  fvelrn  5772  dffo4  5789  f1ompt  5792  fmptco  5807  fsn  5813  fsng  5814  dfmpt  5818  dfmptg  5820  funopsn  5823  funop  5824  funopdmsn  5827  fnressn  5833  fressnfv  5834  fvsng  5843  resfunexg  5868  funfvima3  5881  idref  5890  abrexco  5893  imaiun  5894  dff13  5902  foeqcnvco  5924  f1eqcocnv  5925  fliftcnv  5929  isocnv2  5946  isoini  5952  isose  5955  riotav  5970  csbriotag  5978  acexmidlem2  6008  oprabid  6043  csbov123g  6050  0neqopab  6059  brabvv  6060  dfoprab2  6061  rnoprab  6097  eloprabga  6101  mpov  6104  f1opw  6223  opabex3d  6276  opabex3  6277  ofmres  6291  uchoice  6293  op1stg  6306  op2ndg  6307  1stval2  6311  2ndval2  6312  fo1st  6313  fo2nd  6314  f1stres  6315  f2ndres  6316  fo1stresm  6317  fo2ndresm  6318  xp1st  6321  xp2nd  6322  releldm2  6341  reldm  6342  sbcopeq1a  6343  csbopeq1a  6344  dfoprab3  6347  opabn1stprc  6351  eloprabi  6354  mpomptsx  6355  dmmpossx  6357  fmpox  6358  mpofvex  6363  mpoexxg  6368  fmpoco  6374  df1st2  6377  df2nd2  6378  1stconst  6379  2ndconst  6380  dfmpo  6381  fo2ndf  6385  f1o2ndf1  6386  xporderlem  6389  cnvoprab  6392  f1od2  6393  brtpos2  6410  reldmtpos  6412  dmtpos  6415  rntpos  6416  ovtposg  6418  dftpos3  6421  dftpos4  6422  tpostpos  6423  tpossym  6435  tfrlem3  6470  tfrlem5  6473  tfrlem8  6477  tfrlemisucfn  6483  tfrlemisucaccv  6484  tfrlemibxssdm  6486  tfrlemibfn  6487  tfrlemibex  6488  tfrlemi14d  6492  tfrexlem  6493  tfr1onlem3  6497  tfr1onlemsucaccv  6500  tfr1onlembxssdm  6502  tfr1onlembfn  6503  tfr1onlemres  6508  tfri1dALT  6510  tfrcllemsucaccv  6513  tfrcllembxssdm  6515  tfrcllembfn  6516  tfrcllemres  6521  tfrcl  6523  rdgtfr  6533  rdgruledefgg  6534  rdgivallem  6540  rdgon  6545  rdg0g  6547  frec0g  6556  frecabex  6557  frecabcl  6558  frectfr  6559  freccllem  6561  frecfcllem  6563  frecsuclem  6565  frecrdg  6567  oafnex  6605  sucinc  6606  fnoa  6608  oaexg  6609  omfnex  6610  fnom  6611  omexg  6612  fnoei  6613  oeiexg  6614  oeiv  6617  oacl  6621  omcl  6622  oeicl  6623  oav2  6624  nnsucelsuc  6652  nnsucuniel  6656  ercnv  6716  iserd  6721  eqerlem  6726  eqer  6727  ecdmn0m  6739  erth  6741  qsss  6756  ecid  6760  ecidg  6761  qsid  6762  iinerm  6769  qsel  6774  erovlem  6789  ecopovsym  6793  ecopover  6795  th3qlem2  6800  mapprc  6814  fnmap  6817  fnpm  6818  mapdm0  6825  mapval2  6840  mapsn  6852  mapsncnv  6857  mapsnf1o2  6858  ixpconstg  6869  ixpprc  6881  ixpin  6885  ixpiinm  6886  ixpssmap2g  6889  ixpssmapg  6890  elixpsn  6897  ixpsnf1o  6898  bren  6910  brdomg  6912  domen  6915  domeng  6916  idssen  6943  domssr  6944  ener  6946  domtr  6952  ensn1g  6964  en1  6966  en1bg  6967  fundmen  6974  fundmeng  6975  mapsnen  6979  fiprc  6983  unen  6984  rex2dom  6989  en2m  6992  dom1o  6995  xpsnen  6998  xpsneng  6999  xpcomco  7003  xpcomeng  7005  xpassen  7007  xpdom2  7008  xpdom2g  7009  pw2f1odc  7014  xpf1o  7023  mapen  7025  mapxpen  7027  xpmapenlem  7028  ssenen  7030  phplem4  7034  phplem3g  7035  nneneq  7036  php5  7037  phpm  7045  findcard  7068  findcard2  7069  findcard2s  7070  isinfinf  7077  ac6sfi  7078  exmidpw  7091  exmidpweq  7092  exmidpw2en  7095  unfidisj  7105  fiintim  7114  xpfi  7115  fisseneq  7117  ssfirab  7119  snexxph  7138  fidcenumlemr  7143  sbthlemi10  7154  isbth  7155  ssfii  7162  fi0  7163  fiss  7165  cnvinfex  7206  eqinfti  7208  infvalti  7210  infglbti  7213  infmoti  7216  ordiso2  7223  djuf1olem  7241  djuss  7258  ctm  7297  ctssdccl  7299  ctssdclemr  7300  finomni  7328  exmidomni  7330  fodjuomnilemdc  7332  nninfwlpoimlemginf  7364  pm54.43  7384  pr2cv1  7389  exmidfodomrlemim  7400  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  finacn  7407  acfun  7410  ccfunen  7471  cc2lem  7473  cc3  7475  acnccim  7479  indpi  7550  dfplpq2  7562  enq0sym  7640  enq0ref  7641  enq0tr  7642  nqnq0pi  7646  nqnq0  7649  mulnnnq0  7658  nqprm  7750  nqprrnd  7751  nqprdisj  7752  nqprloc  7753  nqprl  7759  nqpru  7760  addnqprlemrl  7765  addnqprlemru  7766  addnqprlemfl  7767  addnqprlemfu  7768  mulnqprlemrl  7781  mulnqprlemru  7782  mulnqprlemfl  7783  mulnqprlemfu  7784  ltnqpr  7801  ltnqpri  7802  archpr  7851  cauappcvgprlemladdfu  7862  cauappcvgprlemladdfl  7863  cauappcvgprlem2  7868  caucvgprlemladdfu  7885  caucvgprlem2  7888  caucvgprprlemopu  7907  suplocexprlemmu  7926  suplocexprlemdisj  7928  suplocexprlemloc  7929  suplocexprlemub  7931  cnm  8040  ltresr  8047  peano1nnnn  8060  peano2nnnn  8061  axcnre  8089  axpre-apti  8093  renfdisj  8227  dfinfre  9124  1nn  9142  peano2nn  9143  indstr  9815  cnref1o  9873  ioof  10194  fzpr  10300  frec2uzrand  10655  frec2uzf1od  10656  frecuzrdgtcl  10662  frecuzrdgfunlem  10669  frecfzennn  10676  seqp1g  10716  seqclg  10722  seqf1og  10771  seqfeq4g  10781  ser3le  10787  hashinfom  11028  hashunlem  11054  hashun  11055  hashxp  11077  hashfacen  11087  zfz1isolem1  11091  zfz1iso  11092  fundm2domnop0  11096  wrdexb  11112  fnpfx  11245  cats1un  11289  wrdind  11290  wrd2ind  11291  shftfvalg  11366  ovshftex  11367  shftfibg  11368  shftfval  11369  shftfib  11371  shftfn  11372  2shfti  11379  shftvalg  11384  shftval4g  11385  maxabslemval  11756  fimaxre2  11775  xrmaxiflemval  11798  fclim  11842  climshft  11852  zsumdc  11932  fsum3  11935  fsum2dlemstep  11982  fsumcnv  11985  fisumcom2  11986  fisum0diag2  11995  fsumconst  12002  modfsummodlemstep  12005  fsumabs  12013  fsumrelem  12019  fsumiun  12025  ntrivcvgap  12096  fprod2dlemstep  12170  fprodcnv  12173  fprodcom2fi  12174  fprodmodd  12189  nninfct  12599  algrf  12604  qredeu  12656  isprm2  12676  prmind2  12679  4sqlemafi  12955  4sqlem12  12962  ennnfonelemex  13022  ennnfonelemrn  13027  exmidunben  13034  ctinfom  13036  ctinf  13038  qnnen  13039  enctlem  13040  ctiunctlemfo  13047  slotslfn  13095  setscomd  13110  restfn  13313  elrest  13316  ptex  13334  prdsex  13339  prdsvallem  13342  prdsval  13343  prdsbaslemss  13344  prdsbas  13346  imasex  13375  imasival  13376  imasbas  13377  imasplusg  13378  imasmulr  13379  imasaddfnlemg  13384  fnpr2ob  13410  ismgm  13427  plusffng  13435  fn0g  13445  fngsum  13458  gsumsplit1r  13468  gsumprval  13469  issgrp  13473  ismnddef  13488  gsumfzz  13565  gsumfzcl  13569  mulgnngsum  13701  subgintm  13772  releqgg  13794  eqgex  13795  eqgfval  13796  eqgval  13797  isghm  13817  fnmgp  13922  isrng  13934  isring  14000  ringn0  14060  opprrngbg  14078  opprsubgg  14084  opprunitd  14111  dfrhm2  14155  rhmex  14158  opprsubrngg  14212  subrngintm  14213  subrngpropd  14217  subrgpropd  14254  isdomn  14270  opprdomnbg  14275  scaffng  14310  rmodislmodlem  14351  rmodislmod  14352  lssex  14355  lsssn0  14371  lss1d  14384  lssintclm  14385  ellspsn  14418  rlmfn  14454  isridl  14505  blfn  14552  mopnset  14553  metuex  14556  znval  14637  znleval  14654  psrval  14667  fnpsr  14668  mplvalcoe  14691  fnmpl  14694  bastg  14772  distop  14796  topnex  14797  epttop  14801  tgrest  14880  resttopon  14882  restco  14885  cnrest2  14947  cnptopresti  14949  cnptoprest  14950  cnptoprest2  14951  txuni2  14967  txbas  14969  eltx  14970  txcnp  14982  txcnmpt  14984  txrest  14987  txdis1cn  14989  txlm  14990  cnmpt1st  14999  cnmpt2nd  15000  txhmeo  15030  txswaphmeolem  15031  xmetec  15148  metrest  15217  reldvg  15390  dvfgg  15399  dvcj  15420  dvmptfsum  15436  elply2  15446  pilem3  15494  lgsquadlem1  15793  lgsquadlem2  15794  upgrex  15940  umgredg  15980  umgredgnlp  15987  usgredgreu  16051  uspgredg2vtxeu  16053  ushgredgedg  16061  ushgredgedgloop  16063  griedg0ssusgr  16086  wlkvtxiedg  16133  wlkvtxiedgg  16134  wlk1walkdom  16147  bdcvv  16362  bdsnss  16378  bdop  16380  bj-vprc  16401  bdinex1g  16406  bdssexg  16409  bj-inex  16412  bj-zfpair2  16415  bj-uniexg  16423  bdunexb  16425  bj-unexg  16426  bj-indint  16436  bj-ssom  16441  bj-om  16442  bj-2inf  16443  bj-bdfindis  16452  bj-nn0suc0  16455  bj-nnelirr  16458  bj-inf2vnlem1  16475  bj-inf2vnlem2  16476  bj-omex2  16482  bj-nn0sucALT  16483  bj-findis  16484  ss1oel2o  16496  domomsubct  16512  pw1nct  16514  nninfsellemeq  16526  exmidsbthrlem  16536