Theorem vex 2776

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

Syntax hints:   e. wcel 2177   _Vcvv 2773

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  elv  2777  elvd  2778  el2v  2779  isset  2780  eqvisset  2784  ralv  2791  rexv  2792  reuv  2793  rmov  2794  rabab  2795  sbhypf  2824  ceqex  2904  ralab  2937  rexab  2939  mo2icl  2956  reu8  2973  csbvarg  3125  csbiebg  3140  sbcnestgf  3149  sbnfc2  3158  ddifnel  3308  ddifstab  3309  csbing  3384  unssdif  3412  unssin  3416  inssun  3417  invdif  3419  vn0  3475  vn0m  3476  eqv  3484  abvor0dc  3488  sbss  3572  velpw  3628  elpwg  3629  velsn  3655  vsnid  3670  exsnrex  3680  dftp2  3687  prmg  3760  prnzg  3763  snssgOLD  3775  difprsnss  3777  sneqrg  3809  preq12bg  3820  pwprss  3852  pwtpss  3853  pwv  3855  unipr  3870  uniprg  3871  unisng  3873  elintg  3899  elintrabg  3904  intss1  3906  ssint  3907  intmin  3911  intss  3912  intssunim  3913  intmin4  3919  intab  3920  intun  3922  intpr  3923  intprg  3924  uniintsnr  3927  iinconstm  3942  iuniin  3943  iinss1  3945  dfiin2g  3966  dfiunv2  3969  ssiinf  3983  iinss  3985  iinss2  3986  0iin  3992  iinab  3995  iundif2ss  3999  iindif2m  4001  iinin2m  4002  iinuniss  4016  sspwuni  4018  pwpwab  4021  iinpw  4024  iunpwss  4025  brab1  4099  csbopabg  4130  mptv  4149  trint  4165  vnex  4183  inex1g  4188  ssexg  4191  inteximm  4201  inuni  4207  repizf2  4214  axpweq  4223  bnd2  4225  pwuni  4244  exmidundif  4258  exmidundifim  4259  zfpair2  4262  rext  4267  sspwb  4268  unipw  4269  ssextss  4272  euabex  4277  mss  4278  exss  4279  opth  4289  opthg  4290  copsexg  4296  copsex4g  4299  moop2  4304  euotd  4307  opabid  4310  elopab  4312  opelopabsbALT  4313  opelopabsb  4314  opabm  4335  pwin  4337  pwunss  4338  epelg  4345  epel  4347  pofun  4367  epse  4397  tron  4437  sucel  4465  suctr  4476  vuniex  4493  uniexg  4494  unexb  4497  snnex  4503  pwnex  4504  uniuni  4506  eusvnf  4508  eusvnfb  4509  iunpw  4535  unon  4567  ordunisuc2r  4570  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  ordsucunielexmid  4587  elirr  4597  en2lp  4610  dtruex  4615  onintexmid  4629  reg3exmidlemwe  4635  dcextest  4637  finds  4656  finds2  4657  elomssom  4661  limom  4670  0nelxp  4711  opelxp  4713  opeliunxp  4738  elvv  4745  elvvv  4746  elvvuni  4747  xpsspw  4795  relopabiv  4809  relopabi  4811  opabid2  4817  difopab  4819  xpiindim  4823  raliunxp  4827  rexiunxp  4828  ralxpf  4832  rexxpf  4833  relop  4836  cnvco  4871  dfrn2  4874  dfdm4  4879  dmss  4886  dmin  4895  dmiun  4896  dmuni  4897  dm0  4901  dmi  4902  reldm0  4905  elreldm  4913  elrnmpt1  4938  dmrnssfld  4950  dmcoss  4957  dmcosseq  4959  opelresg  4975  resieq  4978  dmres  4989  elres  5004  relssres  5006  resopab  5012  resiexg  5013  iss  5014  dfres2  5020  restidsing  5024  dfima2  5033  imadmrn  5041  imai  5047  csbima12g  5052  elimasng  5059  args  5060  epini  5062  iniseg  5063  dfse2  5064  exse2  5065  cotr  5073  issref  5074  cnvsym  5075  intasym  5076  asymref  5077  intirr  5078  brcodir  5079  codir  5080  qfto  5081  poirr2  5084  cnvopab  5093  cnv0  5095  cnvi  5096  cnvdif  5098  rniun  5102  dminss  5106  imainss  5107  inimasn  5109  xpmlem  5112  dmxpss  5122  rnxpid  5126  ssrnres  5134  rninxp  5135  dminxp  5136  cnvcnv3  5141  dfrel2  5142  dmsnm  5157  dmsnopg  5163  cnvcnvsn  5168  dmsnsnsng  5169  cnvsng  5177  elxp4  5179  elxp5  5180  cnvresima  5181  dfco2  5191  dfco2a  5192  cores  5195  resco  5196  imaco  5197  rnco  5198  coiun  5201  co02  5205  coi1  5207  coass  5210  relssdmrn  5212  unielrel  5219  ressn  5232  cnviinm  5233  cnvpom  5234  cnvsom  5235  uniabio  5251  iotaval  5252  iotass  5258  sniota  5271  csbiotag  5273  dffun2  5290  dffun7  5307  dffun8  5308  dffun9  5309  funopg  5314  funssres  5322  funun  5324  funcnvsn  5328  funinsn  5332  funcnv2  5343  funcnv  5344  funcnv3  5345  funcnveq  5346  fun2cnv  5347  funcnvuni  5352  imadif  5363  funimaexglem  5366  isarep1  5369  2elresin  5396  fnres  5402  fcnvres  5471  fconstg  5484  fun11iun  5555  f1osng  5576  dffv3g  5585  fvssunirng  5604  sefvex  5610  fv3  5612  fvres  5613  nfunsn  5624  funimass4  5642  ssimaexg  5654  dmfco  5660  fvopab6  5689  fndmdif  5698  fvelrn  5724  dffo4  5741  f1ompt  5744  fmptco  5759  fsn  5765  fsng  5766  dfmpt  5770  dfmptg  5772  funopsn  5775  funop  5776  funopdmsn  5777  fnressn  5783  fressnfv  5784  fvsng  5793  resfunexg  5818  funfvima3  5831  idref  5838  abrexco  5841  imaiun  5842  dff13  5850  foeqcnvco  5872  f1eqcocnv  5873  fliftcnv  5877  isocnv2  5894  isoini  5900  isose  5903  riotav  5918  csbriotag  5925  acexmidlem2  5954  oprabid  5989  csbov123g  5996  0neqopab  6003  brabvv  6004  dfoprab2  6005  rnoprab  6041  eloprabga  6045  mpov  6048  f1opw  6166  opabex3d  6219  opabex3  6220  ofmres  6234  uchoice  6236  op1stg  6249  op2ndg  6250  1stval2  6254  2ndval2  6255  fo1st  6256  fo2nd  6257  f1stres  6258  f2ndres  6259  fo1stresm  6260  fo2ndresm  6261  xp1st  6264  xp2nd  6265  releldm2  6284  reldm  6285  sbcopeq1a  6286  csbopeq1a  6287  dfoprab3  6290  eloprabi  6295  mpomptsx  6296  dmmpossx  6298  fmpox  6299  mpofvex  6304  mpoexxg  6309  fmpoco  6315  df1st2  6318  df2nd2  6319  1stconst  6320  2ndconst  6321  dfmpo  6322  fo2ndf  6326  f1o2ndf1  6327  xporderlem  6330  cnvoprab  6333  f1od2  6334  brtpos2  6350  reldmtpos  6352  dmtpos  6355  rntpos  6356  ovtposg  6358  dftpos3  6361  dftpos4  6362  tpostpos  6363  tpossym  6375  tfrlem3  6410  tfrlem5  6413  tfrlem8  6417  tfrlemisucfn  6423  tfrlemisucaccv  6424  tfrlemibxssdm  6426  tfrlemibfn  6427  tfrlemibex  6428  tfrlemi14d  6432  tfrexlem  6433  tfr1onlem3  6437  tfr1onlemsucaccv  6440  tfr1onlembxssdm  6442  tfr1onlembfn  6443  tfr1onlemres  6448  tfri1dALT  6450  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllembfn  6456  tfrcllemres  6461  tfrcl  6463  rdgtfr  6473  rdgruledefgg  6474  rdgivallem  6480  rdgon  6485  rdg0g  6487  frec0g  6496  frecabex  6497  frecabcl  6498  frectfr  6499  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecrdg  6507  oafnex  6543  sucinc  6544  fnoa  6546  oaexg  6547  omfnex  6548  fnom  6549  omexg  6550  fnoei  6551  oeiexg  6552  oeiv  6555  oacl  6559  omcl  6560  oeicl  6561  oav2  6562  nnsucelsuc  6590  nnsucuniel  6594  ercnv  6654  iserd  6659  eqerlem  6664  eqer  6665  ecdmn0m  6677  erth  6679  qsss  6694  ecid  6698  ecidg  6699  qsid  6700  iinerm  6707  qsel  6712  erovlem  6727  ecopovsym  6731  ecopover  6733  th3qlem2  6738  mapprc  6752  fnmap  6755  fnpm  6756  mapdm0  6763  mapval2  6778  mapsn  6790  mapsncnv  6795  mapsnf1o2  6796  ixpconstg  6807  ixpprc  6819  ixpin  6823  ixpiinm  6824  ixpssmap2g  6827  ixpssmapg  6828  elixpsn  6835  ixpsnf1o  6836  bren  6848  brdomg  6850  domen  6853  domeng  6854  idssen  6881  domssr  6882  ener  6884  domtr  6890  ensn1g  6902  en1  6904  en1bg  6905  fundmen  6912  fundmeng  6913  mapsnen  6917  fiprc  6921  unen  6922  rex2dom  6924  en2m  6927  xpsnen  6931  xpsneng  6932  xpcomco  6936  xpcomeng  6938  xpassen  6940  xpdom2  6941  xpdom2g  6942  pw2f1odc  6947  xpf1o  6956  mapen  6958  mapxpen  6960  xpmapenlem  6961  ssenen  6963  phplem4  6967  phplem3g  6968  nneneq  6969  php5  6970  phpm  6977  findcard  7000  findcard2  7001  findcard2s  7002  isinfinf  7009  ac6sfi  7010  exmidpw  7020  exmidpweq  7021  exmidpw2en  7024  unfidisj  7034  fiintim  7043  xpfi  7044  fisseneq  7046  ssfirab  7048  snexxph  7067  fidcenumlemr  7072  sbthlemi10  7083  isbth  7084  ssfii  7091  fi0  7092  fiss  7094  cnvinfex  7135  eqinfti  7137  infvalti  7139  infglbti  7142  infmoti  7145  ordiso2  7152  djuf1olem  7170  djuss  7187  ctm  7226  ctssdccl  7228  ctssdclemr  7229  finomni  7257  exmidomni  7259  fodjuomnilemdc  7261  nninfwlpoimlemginf  7293  pm54.43  7313  exmidfodomrlemim  7325  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  finacn  7332  acfun  7335  ccfunen  7396  cc2lem  7398  cc3  7400  acnccim  7404  indpi  7475  dfplpq2  7487  enq0sym  7565  enq0ref  7566  enq0tr  7567  nqnq0pi  7571  nqnq0  7574  mulnnnq0  7583  nqprm  7675  nqprrnd  7676  nqprdisj  7677  nqprloc  7678  nqprl  7684  nqpru  7685  addnqprlemrl  7690  addnqprlemru  7691  addnqprlemfl  7692  addnqprlemfu  7693  mulnqprlemrl  7706  mulnqprlemru  7707  mulnqprlemfl  7708  mulnqprlemfu  7709  ltnqpr  7726  ltnqpri  7727  archpr  7776  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlem2  7793  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemopu  7832  suplocexprlemmu  7851  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemub  7856  cnm  7965  ltresr  7972  peano1nnnn  7985  peano2nnnn  7986  axcnre  8014  axpre-apti  8018  renfdisj  8152  dfinfre  9049  1nn  9067  peano2nn  9068  indstr  9734  cnref1o  9792  ioof  10113  fzpr  10219  frec2uzrand  10572  frec2uzf1od  10573  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  frecfzennn  10593  seqp1g  10633  seqclg  10639  seqf1og  10688  seqfeq4g  10698  ser3le  10704  hashinfom  10945  hashunlem  10971  hashun  10972  hashxp  10993  hashfacen  11003  zfz1isolem1  11007  zfz1iso  11008  fundm2domnop0  11012  wrdexb  11028  fnpfx  11153  cats1un  11197  wrdind  11198  wrd2ind  11199  shftfvalg  11204  ovshftex  11205  shftfibg  11206  shftfval  11207  shftfib  11209  shftfn  11210  2shfti  11217  shftvalg  11222  shftval4g  11223  maxabslemval  11594  fimaxre2  11613  xrmaxiflemval  11636  fclim  11680  climshft  11690  zsumdc  11770  fsum3  11773  fsum2dlemstep  11820  fsumcnv  11823  fisumcom2  11824  fisum0diag2  11833  fsumconst  11840  modfsummodlemstep  11843  fsumabs  11851  fsumrelem  11857  fsumiun  11863  ntrivcvgap  11934  fprod2dlemstep  12008  fprodcnv  12011  fprodcom2fi  12012  fprodmodd  12027  nninfct  12437  algrf  12442  qredeu  12494  isprm2  12514  prmind2  12517  4sqlemafi  12793  4sqlem12  12800  ennnfonelemex  12860  ennnfonelemrn  12865  exmidunben  12872  ctinfom  12874  ctinf  12876  qnnen  12877  enctlem  12878  ctiunctlemfo  12885  slotslfn  12933  setscomd  12948  restfn  13150  elrest  13153  ptex  13171  prdsex  13176  prdsvallem  13179  prdsval  13180  prdsbaslemss  13181  prdsbas  13183  imasex  13212  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  imasaddfnlemg  13221  fnpr2ob  13247  ismgm  13264  plusffng  13272  fn0g  13282  fngsum  13295  gsumsplit1r  13305  gsumprval  13306  issgrp  13310  ismnddef  13325  gsumfzz  13402  gsumfzcl  13406  mulgnngsum  13538  subgintm  13609  releqgg  13631  eqgex  13632  eqgfval  13633  eqgval  13634  isghm  13654  fnmgp  13759  isrng  13771  isring  13837  ringn0  13897  opprrngbg  13915  opprsubgg  13921  opprunitd  13947  dfrhm2  13991  rhmex  13994  opprsubrngg  14048  subrngintm  14049  subrngpropd  14053  subrgpropd  14090  isdomn  14106  opprdomnbg  14111  scaffng  14146  rmodislmodlem  14187  rmodislmod  14188  lssex  14191  lsssn0  14207  lss1d  14220  lssintclm  14221  ellspsn  14254  rlmfn  14290  isridl  14341  blfn  14388  mopnset  14389  metuex  14392  znval  14473  znleval  14490  psrval  14503  fnpsr  14504  mplvalcoe  14527  fnmpl  14530  bastg  14608  distop  14632  topnex  14633  epttop  14637  tgrest  14716  resttopon  14718  restco  14721  cnrest2  14783  cnptopresti  14785  cnptoprest  14786  cnptoprest2  14787  txuni2  14803  txbas  14805  eltx  14806  txcnp  14818  txcnmpt  14820  txrest  14823  txdis1cn  14825  txlm  14826  cnmpt1st  14835  cnmpt2nd  14836  txhmeo  14866  txswaphmeolem  14867  xmetec  14984  metrest  15053  reldvg  15226  dvfgg  15235  dvcj  15256  dvmptfsum  15272  elply2  15282  pilem3  15330  lgsquadlem1  15629  lgsquadlem2  15630  upgrex  15774  bdcvv  15931  bdsnss  15947  bdop  15949  bj-vprc  15970  bdinex1g  15975  bdssexg  15978  bj-inex  15981  bj-zfpair2  15984  bj-uniexg  15992  bdunexb  15994  bj-unexg  15995  bj-indint  16005  bj-ssom  16010  bj-om  16011  bj-2inf  16012  bj-bdfindis  16021  bj-nn0suc0  16024  bj-nnelirr  16027  bj-inf2vnlem1  16044  bj-inf2vnlem2  16045  bj-omex2  16051  bj-nn0sucALT  16052  bj-findis  16053  ss1oel2o  16066  dom1o  16067  domomsubct  16079  pw1nct  16081  nninfsellemeq  16092  exmidsbthrlem  16102