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  fsn2g  5822  dfmpt  5825  dfmptg  5827  funopsn  5830  funop  5831  funopdmsn  5834  fnressn  5840  fressnfv  5841  fvsng  5850  resfunexg  5875  funfvima3  5888  idref  5897  abrexco  5900  imaiun  5901  dff13  5909  foeqcnvco  5931  f1eqcocnv  5932  fliftcnv  5936  isocnv2  5953  isoini  5959  isose  5962  riotav  5977  csbriotag  5985  acexmidlem2  6015  oprabid  6050  csbov123g  6057  0neqopab  6066  brabvv  6067  dfoprab2  6068  rnoprab  6104  eloprabga  6108  mpov  6111  f1opw  6230  opabex3d  6283  opabex3  6284  ofmres  6298  uchoice  6300  op1stg  6313  op2ndg  6314  1stval2  6318  2ndval2  6319  fo1st  6320  fo2nd  6321  f1stres  6322  f2ndres  6323  fo1stresm  6324  fo2ndresm  6325  xp1st  6328  xp2nd  6329  releldm2  6348  reldm  6349  sbcopeq1a  6350  csbopeq1a  6351  dfoprab3  6354  opabn1stprc  6358  eloprabi  6361  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  mpoexxg  6375  fmpoco  6381  df1st2  6384  df2nd2  6385  1stconst  6386  2ndconst  6387  dfmpo  6388  fo2ndf  6392  f1o2ndf1  6393  xporderlem  6396  cnvoprab  6399  f1od2  6400  brtpos2  6417  reldmtpos  6419  dmtpos  6422  rntpos  6423  ovtposg  6425  dftpos3  6428  dftpos4  6429  tpostpos  6430  tpossym  6442  tfrlem3  6477  tfrlem5  6480  tfrlem8  6484  tfrlemisucfn  6490  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemibex  6495  tfrlemi14d  6499  tfrexlem  6500  tfr1onlem3  6504  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  tfrcl  6530  rdgtfr  6540  rdgruledefgg  6541  rdgivallem  6547  rdgon  6552  rdg0g  6554  frec0g  6563  frecabex  6564  frecabcl  6565  frectfr  6566  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  oafnex  6612  sucinc  6613  fnoa  6615  oaexg  6616  omfnex  6617  fnom  6618  omexg  6619  fnoei  6620  oeiexg  6621  oeiv  6624  oacl  6628  omcl  6629  oeicl  6630  oav2  6631  nnsucelsuc  6659  nnsucuniel  6663  ercnv  6723  iserd  6728  eqerlem  6733  eqer  6734  ecdmn0m  6746  erth  6748  qsss  6763  ecid  6767  ecidg  6768  qsid  6769  iinerm  6776  qsel  6781  erovlem  6796  ecopovsym  6800  ecopover  6802  th3qlem2  6807  mapprc  6821  fnmap  6824  fnpm  6825  mapdm0  6832  mapval2  6847  mapsn  6859  mapsncnv  6864  mapsnf1o2  6865  ixpconstg  6876  ixpprc  6888  ixpin  6892  ixpiinm  6893  ixpssmap2g  6896  ixpssmapg  6897  elixpsn  6904  ixpsnf1o  6905  bren  6917  brdomg  6919  domen  6922  domeng  6923  idssen  6950  domssr  6951  ener  6953  domtr  6959  ensn1g  6971  en1  6973  en1bg  6974  fundmen  6981  fundmeng  6982  mapsnen  6986  fiprc  6990  unen  6991  rex2dom  6996  en2m  6999  dom1o  7002  xpsnen  7005  xpsneng  7006  xpcomco  7010  xpcomeng  7012  xpassen  7014  xpdom2  7015  xpdom2g  7016  pw2f1odc  7021  xpf1o  7030  mapen  7032  mapxpen  7034  xpmapenlem  7035  ssenen  7037  phplem4  7041  phplem3g  7042  nneneq  7043  php5  7044  phpm  7052  findcard  7077  findcard2  7078  findcard2s  7079  isinfinf  7086  ac6sfi  7087  exmidpw  7100  exmidpweq  7101  exmidpw2en  7104  unfidisj  7114  fiintim  7123  xpfi  7124  fisseneq  7127  ssfirab  7129  snexxph  7149  fidcenumlemr  7154  sbthlemi10  7165  isbth  7166  ssfii  7173  fi0  7174  fiss  7176  cnvinfex  7217  eqinfti  7219  infvalti  7221  infglbti  7224  infmoti  7227  ordiso2  7234  djuf1olem  7252  djuss  7269  ctm  7308  ctssdccl  7310  ctssdclemr  7311  finomni  7339  exmidomni  7341  fodjuomnilemdc  7343  nninfwlpoimlemginf  7375  pm54.43  7395  pr2cv1  7400  exmidfodomrlemim  7412  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  acfun  7422  ccfunen  7483  cc2lem  7485  cc3  7487  acnccim  7491  indpi  7562  dfplpq2  7574  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nqnq0  7661  mulnnnq0  7670  nqprm  7762  nqprrnd  7763  nqprdisj  7764  nqprloc  7765  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  ltnqpr  7813  ltnqpri  7814  archpr  7863  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlem2  7880  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemopu  7919  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  cnm  8052  ltresr  8059  peano1nnnn  8072  peano2nnnn  8073  axcnre  8101  axpre-apti  8105  renfdisj  8239  dfinfre  9136  1nn  9154  peano2nn  9155  indstr  9827  cnref1o  9885  ioof  10206  fzpr  10312  frec2uzrand  10668  frec2uzf1od  10669  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  frecfzennn  10689  seqp1g  10729  seqclg  10735  seqf1og  10784  seqfeq4g  10794  ser3le  10800  hashinfom  11041  hashunlem  11068  hashun  11069  hashxp  11091  hashfacen  11101  zfz1isolem1  11105  zfz1iso  11106  fundm2domnop0  11113  wrdexb  11129  fnpfx  11262  cats1un  11306  wrdind  11307  wrd2ind  11308  shftfvalg  11396  ovshftex  11397  shftfibg  11398  shftfval  11399  shftfib  11401  shftfn  11402  2shfti  11409  shftvalg  11414  shftval4g  11415  maxabslemval  11786  fimaxre2  11805  xrmaxiflemval  11828  fclim  11872  climshft  11882  zsumdc  11963  fsum3  11966  fsum2dlemstep  12013  fsumcnv  12016  fisumcom2  12017  fisum0diag2  12026  fsumconst  12033  modfsummodlemstep  12036  fsumabs  12044  fsumrelem  12050  fsumiun  12056  ntrivcvgap  12127  fprod2dlemstep  12201  fprodcnv  12204  fprodcom2fi  12205  fprodmodd  12220  nninfct  12630  algrf  12635  qredeu  12687  isprm2  12707  prmind2  12710  4sqlemafi  12986  4sqlem12  12993  ennnfonelemex  13053  ennnfonelemrn  13058  exmidunben  13065  ctinfom  13067  ctinf  13069  qnnen  13070  enctlem  13071  ctiunctlemfo  13078  slotslfn  13126  setscomd  13141  restfn  13344  elrest  13347  ptex  13365  prdsex  13370  prdsvallem  13373  prdsval  13374  prdsbaslemss  13375  prdsbas  13377  imasex  13406  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfnlemg  13415  fnpr2ob  13441  ismgm  13458  plusffng  13466  fn0g  13476  fngsum  13489  gsumsplit1r  13499  gsumprval  13500  issgrp  13504  ismnddef  13519  gsumfzz  13596  gsumfzcl  13600  mulgnngsum  13732  subgintm  13803  releqgg  13825  eqgex  13826  eqgfval  13827  eqgval  13828  isghm  13848  fnmgp  13954  isrng  13966  isring  14032  ringn0  14092  opprrngbg  14110  opprsubgg  14116  opprunitd  14143  dfrhm2  14187  rhmex  14190  opprsubrngg  14244  subrngintm  14245  subrngpropd  14249  subrgpropd  14286  isdomn  14302  opprdomnbg  14307  scaffng  14342  rmodislmodlem  14383  rmodislmod  14384  lssex  14387  lsssn0  14403  lss1d  14416  lssintclm  14417  ellspsn  14450  rlmfn  14486  isridl  14537  blfn  14584  mopnset  14585  metuex  14588  znval  14669  znleval  14686  psrval  14699  fnpsr  14700  mplvalcoe  14723  fnmpl  14726  bastg  14804  distop  14828  topnex  14829  epttop  14833  tgrest  14912  resttopon  14914  restco  14917  cnrest2  14979  cnptopresti  14981  cnptoprest  14982  cnptoprest2  14983  txuni2  14999  txbas  15001  eltx  15002  txcnp  15014  txcnmpt  15016  txrest  15019  txdis1cn  15021  txlm  15022  cnmpt1st  15031  cnmpt2nd  15032  txhmeo  15062  txswaphmeolem  15063  xmetec  15180  metrest  15249  reldvg  15422  dvfgg  15431  dvcj  15452  dvmptfsum  15468  elply2  15478  pilem3  15526  lgsquadlem1  15825  lgsquadlem2  15826  upgrex  15973  upgr1een  15994  umgredg  16015  umgredgnlp  16022  usgredgreu  16086  uspgredg2vtxeu  16088  ushgredgedg  16096  ushgredgedgloop  16098  griedg0ssusgr  16121  uhgrspansubgrlem  16146  upgrspanop  16153  umgrspanop  16154  usgrspanop  16155  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlk1walkdom  16229  eulerpathum  16351  depindlem1  16376  bdcvv  16503  bdsnss  16519  bdop  16521  bj-vprc  16542  bdinex1g  16547  bdssexg  16550  bj-inex  16553  bj-zfpair2  16556  bj-uniexg  16564  bdunexb  16566  bj-unexg  16567  bj-indint  16577  bj-ssom  16582  bj-om  16583  bj-2inf  16584  bj-bdfindis  16593  bj-nn0suc0  16596  bj-nnelirr  16599  bj-inf2vnlem1  16616  bj-inf2vnlem2  16617  bj-omex2  16623  bj-nn0sucALT  16624  bj-findis  16625  ss1oel2o  16637  domomsubct  16653  pw1nct  16655  nninfsellemeq  16667  exmidsbthrlem  16677  gfsumval  16732