Theorem vex 2805

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

Syntax hints:   e. wcel 2202   _Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elv  2806  elvd  2807  el2v  2808  isset  2809  eqvisset  2813  ralv  2820  rexv  2821  reuv  2822  rmov  2823  rabab  2824  sbhypf  2853  ceqex  2933  ralab  2966  rexab  2968  mo2icl  2985  reu8  3002  csbvarg  3155  csbiebg  3170  sbcnestgf  3179  sbnfc2  3188  ddifnel  3338  ddifstab  3339  csbing  3414  unssdif  3442  unssin  3446  inssun  3447  invdif  3449  vn0  3505  vn0m  3506  eqv  3514  abvor0dc  3518  sbss  3602  velpw  3659  elpwg  3660  velsn  3686  vsnid  3701  exsnrex  3711  dftp2  3718  prmg  3794  prnzg  3797  snssgOLD  3809  difprsnss  3811  sneqrg  3845  preq12bg  3856  pwprss  3889  pwtpss  3890  pwv  3892  unipr  3907  uniprg  3908  unisng  3910  elintg  3936  elintrabg  3941  intss1  3943  ssint  3944  intmin  3948  intss  3949  intssunim  3950  intmin4  3956  intab  3957  intun  3959  intpr  3960  intprg  3961  uniintsnr  3964  iinconstm  3979  iuniin  3980  iinss1  3982  dfiin2g  4003  dfiunv2  4006  ssiinf  4020  iinss  4022  iinss2  4023  0iin  4029  iinab  4032  iundif2ss  4036  iindif2m  4038  iinin2m  4039  iinuniss  4053  sspwuni  4055  pwpwab  4058  iinpw  4061  iunpwss  4062  brab1  4136  csbopabg  4167  mptv  4186  trint  4202  vnex  4220  inex1g  4225  ssexg  4228  inteximm  4239  inuni  4245  repizf2  4252  axpweq  4261  bnd2  4263  pwuni  4282  exmidundif  4296  exmidundifim  4297  zfpair2  4300  rext  4307  sspwb  4308  unipw  4309  ssextss  4312  euabex  4317  mss  4318  exss  4319  opth  4329  opthg  4330  copsexg  4336  copsex4g  4339  moop2  4344  euotd  4347  opabid  4350  elopab  4352  opelopabsbALT  4353  opelopabsb  4354  opabm  4375  pwin  4379  pwunss  4380  epelg  4387  epel  4389  pofun  4409  epse  4439  tron  4479  sucel  4507  suctr  4518  vuniex  4535  uniexg  4536  unexb  4539  snnex  4545  pwnex  4546  uniuni  4548  eusvnf  4550  eusvnfb  4551  iunpw  4577  unon  4609  ordunisuc2r  4612  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordsucunielexmid  4629  elirr  4639  en2lp  4652  dtruex  4657  onintexmid  4671  reg3exmidlemwe  4677  dcextest  4679  finds  4698  finds2  4699  elomssom  4703  limom  4712  0nelxp  4753  opelxp  4755  opeliunxp  4781  elvv  4788  elvvv  4789  elvvuni  4790  xpsspw  4838  relopabiv  4853  relopabi  4855  opabid2  4861  difopab  4863  xpiindim  4867  raliunxp  4871  rexiunxp  4872  ralxpf  4876  rexxpf  4877  relop  4880  cnvco  4915  dfrn2  4918  dfdm4  4923  dmss  4930  dmin  4939  dmiun  4940  dmuni  4941  dm0  4945  dmi  4946  reldm0  4949  reldmm  4950  elreldm  4958  elrnmpt1  4983  dmrnssfld  4995  dmcoss  5002  dmcosseq  5004  opelresg  5020  resieq  5023  dmres  5034  elres  5049  relssres  5051  resopab  5057  resiexg  5058  iss  5059  dfres2  5065  restidsing  5069  dfima2  5078  imadmrn  5086  imai  5092  csbima12g  5097  elimasng  5104  args  5105  epini  5107  iniseg  5108  dfse2  5109  exse2  5110  cotr  5118  issref  5119  cnvsym  5120  intasym  5121  asymref  5122  intirr  5123  brcodir  5124  codir  5125  qfto  5126  poirr2  5129  cnvopab  5138  cnv0  5140  cnvi  5141  cnvdif  5143  rniun  5147  dminss  5151  imainss  5152  inimasn  5154  xpmlem  5157  dmxpss  5167  rnxpid  5171  ssrnres  5179  rninxp  5180  dminxp  5181  cnvcnv3  5186  dfrel2  5187  dmsnm  5202  dmsnopg  5208  cnvcnvsn  5213  dmsnsnsng  5214  cnvsng  5222  elxp4  5224  elxp5  5225  cnvresima  5226  dfco2  5236  dfco2a  5237  cores  5240  resco  5241  imaco  5242  rnco  5243  coiun  5246  co02  5250  coi1  5252  coass  5255  relssdmrn  5257  unielrel  5264  ressn  5277  cnviinm  5278  cnvpom  5279  cnvsom  5280  uniabio  5297  iotaval  5298  iotass  5304  sniota  5317  csbiotag  5319  dffun2  5336  dffun7  5353  dffun8  5354  dffun9  5355  funopg  5360  funssres  5369  funun  5371  funcnvsn  5375  funinsn  5379  funcnv2  5390  funcnv  5391  funcnv3  5392  funcnveq  5393  fun2cnv  5394  funcnvuni  5399  imadif  5410  funimaexglem  5413  isarep1  5416  2elresin  5443  fnres  5449  fcnvres  5520  fconstg  5533  fun11iun  5604  f1osng  5626  dffv3g  5635  fvssunirng  5654  sefvex  5660  fv3  5662  fvres  5663  nfunsn  5676  funimass4  5696  ssimaexg  5708  dmfco  5714  fvopab6  5743  fndmdif  5752  fvelrn  5778  dffo4  5795  f1ompt  5798  fmptco  5813  fsn  5819  fsng  5820  dfmpt  5824  dfmptg  5826  funopsn  5829  funop  5830  funopdmsn  5833  fnressn  5839  fressnfv  5840  fvsng  5849  resfunexg  5874  funfvima3  5887  idref  5896  abrexco  5899  imaiun  5900  dff13  5908  foeqcnvco  5930  f1eqcocnv  5931  fliftcnv  5935  isocnv2  5952  isoini  5958  isose  5961  riotav  5976  csbriotag  5984  acexmidlem2  6014  oprabid  6049  csbov123g  6056  0neqopab  6065  brabvv  6066  dfoprab2  6067  rnoprab  6103  eloprabga  6107  mpov  6110  f1opw  6229  opabex3d  6282  opabex3  6283  ofmres  6297  uchoice  6299  op1stg  6312  op2ndg  6313  1stval2  6317  2ndval2  6318  fo1st  6319  fo2nd  6320  f1stres  6321  f2ndres  6322  fo1stresm  6323  fo2ndresm  6324  xp1st  6327  xp2nd  6328  releldm2  6347  reldm  6348  sbcopeq1a  6349  csbopeq1a  6350  dfoprab3  6353  opabn1stprc  6357  eloprabi  6360  mpomptsx  6361  dmmpossx  6363  fmpox  6364  mpofvex  6369  mpoexxg  6374  fmpoco  6380  df1st2  6383  df2nd2  6384  1stconst  6385  2ndconst  6386  dfmpo  6387  fo2ndf  6391  f1o2ndf1  6392  xporderlem  6395  cnvoprab  6398  f1od2  6399  brtpos2  6416  reldmtpos  6418  dmtpos  6421  rntpos  6422  ovtposg  6424  dftpos3  6427  dftpos4  6428  tpostpos  6429  tpossym  6441  tfrlem3  6476  tfrlem5  6479  tfrlem8  6483  tfrlemisucfn  6489  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemibex  6494  tfrlemi14d  6498  tfrexlem  6499  tfr1onlem3  6503  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemres  6514  tfri1dALT  6516  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemres  6527  tfrcl  6529  rdgtfr  6539  rdgruledefgg  6540  rdgivallem  6546  rdgon  6551  rdg0g  6553  frec0g  6562  frecabex  6563  frecabcl  6564  frectfr  6565  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecrdg  6573  oafnex  6611  sucinc  6612  fnoa  6614  oaexg  6615  omfnex  6616  fnom  6617  omexg  6618  fnoei  6619  oeiexg  6620  oeiv  6623  oacl  6627  omcl  6628  oeicl  6629  oav2  6630  nnsucelsuc  6658  nnsucuniel  6662  ercnv  6722  iserd  6727  eqerlem  6732  eqer  6733  ecdmn0m  6745  erth  6747  qsss  6762  ecid  6766  ecidg  6767  qsid  6768  iinerm  6775  qsel  6780  erovlem  6795  ecopovsym  6799  ecopover  6801  th3qlem2  6806  mapprc  6820  fnmap  6823  fnpm  6824  mapdm0  6831  mapval2  6846  mapsn  6858  mapsncnv  6863  mapsnf1o2  6864  ixpconstg  6875  ixpprc  6887  ixpin  6891  ixpiinm  6892  ixpssmap2g  6895  ixpssmapg  6896  elixpsn  6903  ixpsnf1o  6904  bren  6916  brdomg  6918  domen  6921  domeng  6922  idssen  6949  domssr  6950  ener  6952  domtr  6958  ensn1g  6970  en1  6972  en1bg  6973  fundmen  6980  fundmeng  6981  mapsnen  6985  fiprc  6989  unen  6990  rex2dom  6995  en2m  6998  dom1o  7001  xpsnen  7004  xpsneng  7005  xpcomco  7009  xpcomeng  7011  xpassen  7013  xpdom2  7014  xpdom2g  7015  pw2f1odc  7020  xpf1o  7029  mapen  7031  mapxpen  7033  xpmapenlem  7034  ssenen  7036  phplem4  7040  phplem3g  7041  nneneq  7042  php5  7043  phpm  7051  findcard  7076  findcard2  7077  findcard2s  7078  isinfinf  7085  ac6sfi  7086  exmidpw  7099  exmidpweq  7100  exmidpw2en  7103  unfidisj  7113  fiintim  7122  xpfi  7123  fisseneq  7126  ssfirab  7128  snexxph  7148  fidcenumlemr  7153  sbthlemi10  7164  isbth  7165  ssfii  7172  fi0  7173  fiss  7175  cnvinfex  7216  eqinfti  7218  infvalti  7220  infglbti  7223  infmoti  7226  ordiso2  7233  djuf1olem  7251  djuss  7268  ctm  7307  ctssdccl  7309  ctssdclemr  7310  finomni  7338  exmidomni  7340  fodjuomnilemdc  7342  nninfwlpoimlemginf  7374  pm54.43  7394  pr2cv1  7399  exmidfodomrlemim  7411  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  finacn  7418  acfun  7421  ccfunen  7482  cc2lem  7484  cc3  7486  acnccim  7490  indpi  7561  dfplpq2  7573  enq0sym  7651  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  nqnq0  7660  mulnnnq0  7669  nqprm  7761  nqprrnd  7762  nqprdisj  7763  nqprloc  7764  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  ltnqpr  7812  ltnqpri  7813  archpr  7862  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlem2  7879  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemopu  7918  suplocexprlemmu  7937  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  cnm  8051  ltresr  8058  peano1nnnn  8071  peano2nnnn  8072  axcnre  8100  axpre-apti  8104  renfdisj  8238  dfinfre  9135  1nn  9153  peano2nn  9154  indstr  9826  cnref1o  9884  ioof  10205  fzpr  10311  frec2uzrand  10666  frec2uzf1od  10667  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  frecfzennn  10687  seqp1g  10727  seqclg  10733  seqf1og  10782  seqfeq4g  10792  ser3le  10798  hashinfom  11039  hashunlem  11066  hashun  11067  hashxp  11089  hashfacen  11099  zfz1isolem1  11103  zfz1iso  11104  fundm2domnop0  11108  wrdexb  11124  fnpfx  11257  cats1un  11301  wrdind  11302  wrd2ind  11303  shftfvalg  11378  ovshftex  11379  shftfibg  11380  shftfval  11381  shftfib  11383  shftfn  11384  2shfti  11391  shftvalg  11396  shftval4g  11397  maxabslemval  11768  fimaxre2  11787  xrmaxiflemval  11810  fclim  11854  climshft  11864  zsumdc  11944  fsum3  11947  fsum2dlemstep  11994  fsumcnv  11997  fisumcom2  11998  fisum0diag2  12007  fsumconst  12014  modfsummodlemstep  12017  fsumabs  12025  fsumrelem  12031  fsumiun  12037  ntrivcvgap  12108  fprod2dlemstep  12182  fprodcnv  12185  fprodcom2fi  12186  fprodmodd  12201  nninfct  12611  algrf  12616  qredeu  12668  isprm2  12688  prmind2  12691  4sqlemafi  12967  4sqlem12  12974  ennnfonelemex  13034  ennnfonelemrn  13039  exmidunben  13046  ctinfom  13048  ctinf  13050  qnnen  13051  enctlem  13052  ctiunctlemfo  13059  slotslfn  13107  setscomd  13122  restfn  13325  elrest  13328  ptex  13346  prdsex  13351  prdsvallem  13354  prdsval  13355  prdsbaslemss  13356  prdsbas  13358  imasex  13387  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfnlemg  13396  fnpr2ob  13422  ismgm  13439  plusffng  13447  fn0g  13457  fngsum  13470  gsumsplit1r  13480  gsumprval  13481  issgrp  13485  ismnddef  13500  gsumfzz  13577  gsumfzcl  13581  mulgnngsum  13713  subgintm  13784  releqgg  13806  eqgex  13807  eqgfval  13808  eqgval  13809  isghm  13829  fnmgp  13934  isrng  13946  isring  14012  ringn0  14072  opprrngbg  14090  opprsubgg  14096  opprunitd  14123  dfrhm2  14167  rhmex  14170  opprsubrngg  14224  subrngintm  14225  subrngpropd  14229  subrgpropd  14266  isdomn  14282  opprdomnbg  14287  scaffng  14322  rmodislmodlem  14363  rmodislmod  14364  lssex  14367  lsssn0  14383  lss1d  14396  lssintclm  14397  ellspsn  14430  rlmfn  14466  isridl  14517  blfn  14564  mopnset  14565  metuex  14568  znval  14649  znleval  14666  psrval  14679  fnpsr  14680  mplvalcoe  14703  fnmpl  14706  bastg  14784  distop  14808  topnex  14809  epttop  14813  tgrest  14892  resttopon  14894  restco  14897  cnrest2  14959  cnptopresti  14961  cnptoprest  14962  cnptoprest2  14963  txuni2  14979  txbas  14981  eltx  14982  txcnp  14994  txcnmpt  14996  txrest  14999  txdis1cn  15001  txlm  15002  cnmpt1st  15011  cnmpt2nd  15012  txhmeo  15042  txswaphmeolem  15043  xmetec  15160  metrest  15229  reldvg  15402  dvfgg  15411  dvcj  15432  dvmptfsum  15448  elply2  15458  pilem3  15506  lgsquadlem1  15805  lgsquadlem2  15806  upgrex  15953  upgr1een  15974  umgredg  15995  umgredgnlp  16002  usgredgreu  16066  uspgredg2vtxeu  16068  ushgredgedg  16076  ushgredgedgloop  16078  griedg0ssusgr  16101  uhgrspansubgrlem  16126  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlk1walkdom  16209  bdcvv  16452  bdsnss  16468  bdop  16470  bj-vprc  16491  bdinex1g  16496  bdssexg  16499  bj-inex  16502  bj-zfpair2  16505  bj-uniexg  16513  bdunexb  16515  bj-unexg  16516  bj-indint  16526  bj-ssom  16531  bj-om  16532  bj-2inf  16533  bj-bdfindis  16542  bj-nn0suc0  16545  bj-nnelirr  16548  bj-inf2vnlem1  16565  bj-inf2vnlem2  16566  bj-omex2  16572  bj-nn0sucALT  16573  bj-findis  16574  ss1oel2o  16586  domomsubct  16602  pw1nct  16604  nninfsellemeq  16616  exmidsbthrlem  16626  gfsumval  16680