Theorem vex 2729

Description: All setvar variables are sets (see isset 2732). 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 1689	. 2 |- x = x
2		df-v 2728	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2277	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 145	1 |- x e. _V

Syntax hints:   e. wcel 2136   _Vcvv 2726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  elv  2730  elvd  2731  isset  2732  eqvisset  2736  ralv  2743  rexv  2744  reuv  2745  rmov  2746  rabab  2747  sbhypf  2775  ceqex  2853  ralab  2886  rexab  2888  mo2icl  2905  reu8  2922  csbvarg  3073  csbiebg  3087  sbcnestgf  3096  sbnfc2  3105  ddifnel  3253  ddifstab  3254  csbing  3329  unssdif  3357  unssin  3361  inssun  3362  invdif  3364  vn0  3419  vn0m  3420  eqv  3428  abvor0dc  3432  sbss  3517  velpw  3566  elpwg  3567  velsn  3593  vsnid  3608  exsnrex  3618  dftp2  3625  prmg  3697  prnzg  3700  snssg  3709  difprsnss  3711  sneqrg  3742  preq12bg  3753  pwprss  3785  pwtpss  3786  pwv  3788  unipr  3803  uniprg  3804  unisng  3806  elintg  3832  elintrabg  3837  intss1  3839  ssint  3840  intmin  3844  intss  3845  intssunim  3846  intmin4  3852  intab  3853  intun  3855  intpr  3856  intprg  3857  uniintsnr  3860  iinconstm  3875  iuniin  3876  iinss1  3878  dfiin2g  3899  dfiunv2  3902  ssiinf  3915  iinss  3917  iinss2  3918  0iin  3924  iinab  3927  iundif2ss  3931  iindif2m  3933  iinin2m  3934  iinuniss  3948  sspwuni  3950  pwpwab  3953  iinpw  3956  iunpwss  3957  brab1  4029  csbopabg  4060  mptv  4079  trint  4095  vnex  4113  inex1g  4118  ssexg  4121  inteximm  4128  inuni  4134  repizf2  4141  axpweq  4150  bnd2  4152  pwuni  4171  exmidundif  4185  exmidundifim  4186  zfpair2  4188  rext  4193  sspwb  4194  unipw  4195  ssextss  4198  euabex  4203  mss  4204  exss  4205  opth  4215  opthg  4216  copsexg  4222  copsex4g  4225  moop2  4229  euotd  4232  opabid  4235  elopab  4236  opelopabsbALT  4237  opelopabsb  4238  opabm  4258  pwin  4260  pwunss  4261  epelg  4268  epel  4270  pofun  4290  epse  4320  tron  4360  sucel  4388  suctr  4399  vuniex  4416  uniexg  4417  unexb  4420  snnex  4426  pwnex  4427  uniuni  4429  eusvnf  4431  eusvnfb  4432  iunpw  4458  unon  4488  ordunisuc2r  4491  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  ordsucunielexmid  4508  elirr  4518  en2lp  4531  dtruex  4536  onintexmid  4550  reg3exmidlemwe  4556  dcextest  4558  finds  4577  finds2  4578  elomssom  4582  limom  4591  0nelxp  4632  opelxp  4634  opeliunxp  4659  elvv  4666  elvvv  4667  elvvuni  4668  xpsspw  4716  relopabi  4730  opabid2  4735  difopab  4737  xpiindim  4741  raliunxp  4745  rexiunxp  4746  ralxpf  4750  rexxpf  4751  relop  4754  cnvco  4789  dfrn2  4792  dfdm4  4796  dmss  4803  dmin  4812  dmiun  4813  dmuni  4814  dm0  4818  dmi  4819  reldm0  4822  elreldm  4830  elrnmpt1  4855  dmrnssfld  4867  dmcoss  4873  dmcosseq  4875  opelresg  4891  resieq  4894  dmres  4905  elres  4920  relssres  4922  resopab  4928  resiexg  4929  iss  4930  dfres2  4936  dfima2  4948  imadmrn  4956  imai  4960  csbima12g  4965  elimasng  4972  args  4973  epini  4975  iniseg  4976  dfse2  4977  exse2  4978  cotr  4985  issref  4986  cnvsym  4987  intasym  4988  asymref  4989  intirr  4990  brcodir  4991  codir  4992  qfto  4993  poirr2  4996  cnvopab  5005  cnv0  5007  cnvi  5008  cnvdif  5010  rniun  5014  dminss  5018  imainss  5019  inimasn  5021  xpmlem  5024  dmxpss  5034  rnxpid  5038  ssrnres  5046  rninxp  5047  dminxp  5048  cnvcnv3  5053  dfrel2  5054  dmsnm  5069  dmsnopg  5075  cnvcnvsn  5080  dmsnsnsng  5081  cnvsng  5089  elxp4  5091  elxp5  5092  cnvresima  5093  dfco2  5103  dfco2a  5104  cores  5107  resco  5108  imaco  5109  rnco  5110  coiun  5113  co02  5117  coi1  5119  coass  5122  relssdmrn  5124  unielrel  5131  ressn  5144  cnviinm  5145  cnvpom  5146  cnvsom  5147  uniabio  5163  iotaval  5164  iotass  5170  sniota  5180  csbiotag  5181  dffun2  5198  dffun7  5215  dffun8  5216  dffun9  5217  funopg  5222  funssres  5230  funun  5232  funcnvsn  5233  funinsn  5237  funcnv2  5248  funcnv  5249  funcnv3  5250  funcnveq  5251  fun2cnv  5252  funcnvuni  5257  imadif  5268  funimaexglem  5271  isarep1  5274  2elresin  5299  fnres  5304  fcnvres  5371  fconstg  5384  fun11iun  5453  f1osng  5473  dffv3g  5482  fvssunirng  5501  sefvex  5507  fv3  5509  fvres  5510  nfunsn  5520  funimass4  5537  ssimaexg  5548  dmfco  5554  fvopab6  5582  fndmdif  5590  fvelrn  5616  dffo4  5633  f1ompt  5636  fmptco  5651  fsn  5657  fsng  5658  dfmpt  5662  dfmptg  5664  fnressn  5671  fressnfv  5672  fvsng  5681  resfunexg  5706  funfvima3  5718  idref  5725  abrexco  5727  imaiun  5728  dff13  5736  foeqcnvco  5758  f1eqcocnv  5759  fliftcnv  5763  isocnv2  5780  isoini  5786  isose  5789  riotav  5803  csbriotag  5810  acexmidlem2  5839  oprabid  5874  csbov123g  5880  0neqopab  5887  brabvv  5888  dfoprab2  5889  rnoprab  5925  eloprabga  5929  mpov  5932  f1opw  6045  opabex3d  6089  opabex3  6090  ofmres  6104  op1stg  6118  op2ndg  6119  1stval2  6123  2ndval2  6124  fo1st  6125  fo2nd  6126  f1stres  6127  f2ndres  6128  fo1stresm  6129  fo2ndresm  6130  xp1st  6133  xp2nd  6134  releldm2  6153  reldm  6154  sbcopeq1a  6155  csbopeq1a  6156  dfoprab3  6159  eloprabi  6164  mpomptsx  6165  dmmpossx  6167  fmpox  6168  mpofvex  6171  mpoexxg  6178  fmpoco  6184  df1st2  6187  df2nd2  6188  1stconst  6189  2ndconst  6190  dfmpo  6191  fo2ndf  6195  f1o2ndf1  6196  xporderlem  6199  cnvoprab  6202  f1od2  6203  brtpos2  6219  reldmtpos  6221  dmtpos  6224  rntpos  6225  ovtposg  6227  dftpos3  6230  dftpos4  6231  tpostpos  6232  tpossym  6244  tfrlem3  6279  tfrlem5  6282  tfrlem8  6286  tfrlemisucfn  6292  tfrlemisucaccv  6293  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrlemibex  6297  tfrlemi14d  6301  tfrexlem  6302  tfr1onlem3  6306  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemres  6317  tfri1dALT  6319  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemres  6330  tfrcl  6332  rdgtfr  6342  rdgruledefgg  6343  rdgivallem  6349  rdgon  6354  rdg0g  6356  frec0g  6365  frecabex  6366  frecabcl  6367  frectfr  6368  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecrdg  6376  oafnex  6412  sucinc  6413  fnoa  6415  oaexg  6416  omfnex  6417  fnom  6418  omexg  6419  fnoei  6420  oeiexg  6421  oeiv  6424  oacl  6428  omcl  6429  oeicl  6430  oav2  6431  nnsucelsuc  6459  nnsucuniel  6463  ercnv  6522  iserd  6527  eqerlem  6532  eqer  6533  ecdmn0m  6543  erth  6545  qsss  6560  ecid  6564  ecidg  6565  qsid  6566  iinerm  6573  qsel  6578  erovlem  6593  ecopovsym  6597  ecopover  6599  th3qlem2  6604  mapprc  6618  fnmap  6621  fnpm  6622  mapdm0  6629  mapval2  6644  mapsn  6656  mapsncnv  6661  mapsnf1o2  6662  ixpconstg  6673  ixpprc  6685  ixpin  6689  ixpiinm  6690  ixpssmap2g  6693  ixpssmapg  6694  elixpsn  6701  ixpsnf1o  6702  bren  6713  brdomg  6714  domen  6717  domeng  6718  idssen  6743  ener  6745  domtr  6751  ensn1g  6763  en1  6765  en1bg  6766  fundmen  6772  fundmeng  6773  mapsnen  6777  fiprc  6781  unen  6782  xpsnen  6787  xpsneng  6788  xpcomco  6792  xpcomeng  6794  xpassen  6796  xpdom2  6797  xpdom2g  6798  xpf1o  6810  mapen  6812  mapxpen  6814  xpmapenlem  6815  ssenen  6817  phplem4  6821  phplem3g  6822  nneneq  6823  php5  6824  phpm  6831  findcard  6854  findcard2  6855  findcard2s  6856  isinfinf  6863  ac6sfi  6864  exmidpw  6874  exmidpweq  6875  unfidisj  6887  fiintim  6894  xpfi  6895  fisseneq  6897  ssfirab  6899  snexxph  6915  fidcenumlemr  6920  sbthlemi10  6931  isbth  6932  ssfii  6939  fi0  6940  fiss  6942  cnvinfex  6983  eqinfti  6985  infvalti  6987  infglbti  6990  infmoti  6993  ordiso2  7000  djuf1olem  7018  djuss  7035  ctm  7074  ctssdccl  7076  ctssdclemr  7077  finomni  7104  exmidomni  7106  fodjuomnilemdc  7108  pm54.43  7146  exmidfodomrlemim  7157  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  acfun  7163  ccfunen  7205  cc2lem  7207  cc3  7209  indpi  7283  dfplpq2  7295  enq0sym  7373  enq0ref  7374  enq0tr  7375  nqnq0pi  7379  nqnq0  7382  mulnnnq0  7391  nqprm  7483  nqprrnd  7484  nqprdisj  7485  nqprloc  7486  nqprl  7492  nqpru  7493  addnqprlemrl  7498  addnqprlemru  7499  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemrl  7514  mulnqprlemru  7515  mulnqprlemfl  7516  mulnqprlemfu  7517  ltnqpr  7534  ltnqpri  7535  archpr  7584  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlem2  7601  caucvgprlemladdfu  7618  caucvgprlem2  7621  caucvgprprlemopu  7640  suplocexprlemmu  7659  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  cnm  7773  ltresr  7780  peano1nnnn  7793  peano2nnnn  7794  axcnre  7822  axpre-apti  7826  renfdisj  7958  dfinfre  8851  1nn  8868  peano2nn  8869  indstr  9531  cnref1o  9588  ioof  9907  fzpr  10012  frec2uzrand  10340  frec2uzf1od  10341  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  frecfzennn  10361  ser3le  10453  hashinfom  10691  hashunlem  10717  hashun  10718  hashxp  10739  hashfacen  10749  zfz1isolem1  10753  zfz1iso  10754  shftfvalg  10760  ovshftex  10761  shftfibg  10762  shftfval  10763  shftfib  10765  shftfn  10766  2shfti  10773  shftvalg  10778  shftval4g  10779  maxabslemval  11150  fimaxre2  11168  xrmaxiflemval  11191  fclim  11235  climshft  11245  zsumdc  11325  fsum3  11328  fsum2dlemstep  11375  fsumcnv  11378  fisumcom2  11379  fisum0diag2  11388  fsumconst  11395  modfsummodlemstep  11398  fsumabs  11406  fsumrelem  11412  fsumiun  11418  ntrivcvgap  11489  fprod2dlemstep  11563  fprodcnv  11566  fprodcom2fi  11567  fprodmodd  11582  algrf  11977  qredeu  12029  isprm2  12049  prmind2  12052  ennnfonelemex  12347  ennnfonelemrn  12352  exmidunben  12359  ctinfom  12361  ctinf  12363  qnnen  12364  enctlem  12365  ctiunctlemfo  12372  slotslfn  12420  restfn  12560  elrest  12563  ismgm  12588  plusffng  12596  fn0g  12606  bastg  12701  distop  12725  topnex  12726  epttop  12730  tgrest  12809  resttopon  12811  restco  12814  cnrest2  12876  cnptopresti  12878  cnptoprest  12879  cnptoprest2  12880  txuni2  12896  txbas  12898  eltx  12899  txcnp  12911  txcnmpt  12913  txrest  12916  txdis1cn  12918  txlm  12919  cnmpt1st  12928  cnmpt2nd  12929  txhmeo  12959  txswaphmeolem  12960  xmetec  13077  metrest  13146  reldvg  13288  dvfgg  13297  dvcj  13313  pilem3  13344  bdcvv  13739  bdsnss  13755  bdop  13757  bj-vprc  13778  bdinex1g  13783  bdssexg  13786  bj-inex  13789  bj-zfpair2  13792  bj-uniexg  13800  bdunexb  13802  bj-unexg  13803  bj-indint  13813  bj-ssom  13818  bj-om  13819  bj-2inf  13820  bj-bdfindis  13829  bj-nn0suc0  13832  bj-nnelirr  13835  bj-inf2vnlem1  13852  bj-inf2vnlem2  13853  bj-omex2  13859  bj-nn0sucALT  13860  bj-findis  13861  ss1oel2o  13873  pw1nct  13883  nninfsellemeq  13894  exmidsbthrlem  13901