Theorem vex 2733

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

Syntax hints:   e. wcel 2141   _Vcvv 2730

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  elv  2734  elvd  2735  isset  2736  eqvisset  2740  ralv  2747  rexv  2748  reuv  2749  rmov  2750  rabab  2751  sbhypf  2779  ceqex  2857  ralab  2890  rexab  2892  mo2icl  2909  reu8  2926  csbvarg  3077  csbiebg  3091  sbcnestgf  3100  sbnfc2  3109  ddifnel  3258  ddifstab  3259  csbing  3334  unssdif  3362  unssin  3366  inssun  3367  invdif  3369  vn0  3425  vn0m  3426  eqv  3434  abvor0dc  3438  sbss  3523  velpw  3573  elpwg  3574  velsn  3600  vsnid  3615  exsnrex  3625  dftp2  3632  prmg  3704  prnzg  3707  snssg  3716  difprsnss  3718  sneqrg  3749  preq12bg  3760  pwprss  3792  pwtpss  3793  pwv  3795  unipr  3810  uniprg  3811  unisng  3813  elintg  3839  elintrabg  3844  intss1  3846  ssint  3847  intmin  3851  intss  3852  intssunim  3853  intmin4  3859  intab  3860  intun  3862  intpr  3863  intprg  3864  uniintsnr  3867  iinconstm  3882  iuniin  3883  iinss1  3885  dfiin2g  3906  dfiunv2  3909  ssiinf  3922  iinss  3924  iinss2  3925  0iin  3931  iinab  3934  iundif2ss  3938  iindif2m  3940  iinin2m  3941  iinuniss  3955  sspwuni  3957  pwpwab  3960  iinpw  3963  iunpwss  3964  brab1  4036  csbopabg  4067  mptv  4086  trint  4102  vnex  4120  inex1g  4125  ssexg  4128  inteximm  4135  inuni  4141  repizf2  4148  axpweq  4157  bnd2  4159  pwuni  4178  exmidundif  4192  exmidundifim  4193  zfpair2  4195  rext  4200  sspwb  4201  unipw  4202  ssextss  4205  euabex  4210  mss  4211  exss  4212  opth  4222  opthg  4223  copsexg  4229  copsex4g  4232  moop2  4236  euotd  4239  opabid  4242  elopab  4243  opelopabsbALT  4244  opelopabsb  4245  opabm  4265  pwin  4267  pwunss  4268  epelg  4275  epel  4277  pofun  4297  epse  4327  tron  4367  sucel  4395  suctr  4406  vuniex  4423  uniexg  4424  unexb  4427  snnex  4433  pwnex  4434  uniuni  4436  eusvnf  4438  eusvnfb  4439  iunpw  4465  unon  4495  ordunisuc2r  4498  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordsucunielexmid  4515  elirr  4525  en2lp  4538  dtruex  4543  onintexmid  4557  reg3exmidlemwe  4563  dcextest  4565  finds  4584  finds2  4585  elomssom  4589  limom  4598  0nelxp  4639  opelxp  4641  opeliunxp  4666  elvv  4673  elvvv  4674  elvvuni  4675  xpsspw  4723  relopabi  4737  opabid2  4742  difopab  4744  xpiindim  4748  raliunxp  4752  rexiunxp  4753  ralxpf  4757  rexxpf  4758  relop  4761  cnvco  4796  dfrn2  4799  dfdm4  4803  dmss  4810  dmin  4819  dmiun  4820  dmuni  4821  dm0  4825  dmi  4826  reldm0  4829  elreldm  4837  elrnmpt1  4862  dmrnssfld  4874  dmcoss  4880  dmcosseq  4882  opelresg  4898  resieq  4901  dmres  4912  elres  4927  relssres  4929  resopab  4935  resiexg  4936  iss  4937  dfres2  4943  dfima2  4955  imadmrn  4963  imai  4967  csbima12g  4972  elimasng  4979  args  4980  epini  4982  iniseg  4983  dfse2  4984  exse2  4985  cotr  4992  issref  4993  cnvsym  4994  intasym  4995  asymref  4996  intirr  4997  brcodir  4998  codir  4999  qfto  5000  poirr2  5003  cnvopab  5012  cnv0  5014  cnvi  5015  cnvdif  5017  rniun  5021  dminss  5025  imainss  5026  inimasn  5028  xpmlem  5031  dmxpss  5041  rnxpid  5045  ssrnres  5053  rninxp  5054  dminxp  5055  cnvcnv3  5060  dfrel2  5061  dmsnm  5076  dmsnopg  5082  cnvcnvsn  5087  dmsnsnsng  5088  cnvsng  5096  elxp4  5098  elxp5  5099  cnvresima  5100  dfco2  5110  dfco2a  5111  cores  5114  resco  5115  imaco  5116  rnco  5117  coiun  5120  co02  5124  coi1  5126  coass  5129  relssdmrn  5131  unielrel  5138  ressn  5151  cnviinm  5152  cnvpom  5153  cnvsom  5154  uniabio  5170  iotaval  5171  iotass  5177  sniota  5189  csbiotag  5191  dffun2  5208  dffun7  5225  dffun8  5226  dffun9  5227  funopg  5232  funssres  5240  funun  5242  funcnvsn  5243  funinsn  5247  funcnv2  5258  funcnv  5259  funcnv3  5260  funcnveq  5261  fun2cnv  5262  funcnvuni  5267  imadif  5278  funimaexglem  5281  isarep1  5284  2elresin  5309  fnres  5314  fcnvres  5381  fconstg  5394  fun11iun  5463  f1osng  5483  dffv3g  5492  fvssunirng  5511  sefvex  5517  fv3  5519  fvres  5520  nfunsn  5530  funimass4  5547  ssimaexg  5558  dmfco  5564  fvopab6  5592  fndmdif  5601  fvelrn  5627  dffo4  5644  f1ompt  5647  fmptco  5662  fsn  5668  fsng  5669  dfmpt  5673  dfmptg  5675  fnressn  5682  fressnfv  5683  fvsng  5692  resfunexg  5717  funfvima3  5729  idref  5736  abrexco  5738  imaiun  5739  dff13  5747  foeqcnvco  5769  f1eqcocnv  5770  fliftcnv  5774  isocnv2  5791  isoini  5797  isose  5800  riotav  5814  csbriotag  5821  acexmidlem2  5850  oprabid  5885  csbov123g  5891  0neqopab  5898  brabvv  5899  dfoprab2  5900  rnoprab  5936  eloprabga  5940  mpov  5943  f1opw  6056  opabex3d  6100  opabex3  6101  ofmres  6115  op1stg  6129  op2ndg  6130  1stval2  6134  2ndval2  6135  fo1st  6136  fo2nd  6137  f1stres  6138  f2ndres  6139  fo1stresm  6140  fo2ndresm  6141  xp1st  6144  xp2nd  6145  releldm2  6164  reldm  6165  sbcopeq1a  6166  csbopeq1a  6167  dfoprab3  6170  eloprabi  6175  mpomptsx  6176  dmmpossx  6178  fmpox  6179  mpofvex  6182  mpoexxg  6189  fmpoco  6195  df1st2  6198  df2nd2  6199  1stconst  6200  2ndconst  6201  dfmpo  6202  fo2ndf  6206  f1o2ndf1  6207  xporderlem  6210  cnvoprab  6213  f1od2  6214  brtpos2  6230  reldmtpos  6232  dmtpos  6235  rntpos  6236  ovtposg  6238  dftpos3  6241  dftpos4  6242  tpostpos  6243  tpossym  6255  tfrlem3  6290  tfrlem5  6293  tfrlem8  6297  tfrlemisucfn  6303  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemibex  6308  tfrlemi14d  6312  tfrexlem  6313  tfr1onlem3  6317  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemres  6328  tfri1dALT  6330  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemres  6341  tfrcl  6343  rdgtfr  6353  rdgruledefgg  6354  rdgivallem  6360  rdgon  6365  rdg0g  6367  frec0g  6376  frecabex  6377  frecabcl  6378  frectfr  6379  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecrdg  6387  oafnex  6423  sucinc  6424  fnoa  6426  oaexg  6427  omfnex  6428  fnom  6429  omexg  6430  fnoei  6431  oeiexg  6432  oeiv  6435  oacl  6439  omcl  6440  oeicl  6441  oav2  6442  nnsucelsuc  6470  nnsucuniel  6474  ercnv  6534  iserd  6539  eqerlem  6544  eqer  6545  ecdmn0m  6555  erth  6557  qsss  6572  ecid  6576  ecidg  6577  qsid  6578  iinerm  6585  qsel  6590  erovlem  6605  ecopovsym  6609  ecopover  6611  th3qlem2  6616  mapprc  6630  fnmap  6633  fnpm  6634  mapdm0  6641  mapval2  6656  mapsn  6668  mapsncnv  6673  mapsnf1o2  6674  ixpconstg  6685  ixpprc  6697  ixpin  6701  ixpiinm  6702  ixpssmap2g  6705  ixpssmapg  6706  elixpsn  6713  ixpsnf1o  6714  bren  6725  brdomg  6726  domen  6729  domeng  6730  idssen  6755  ener  6757  domtr  6763  ensn1g  6775  en1  6777  en1bg  6778  fundmen  6784  fundmeng  6785  mapsnen  6789  fiprc  6793  unen  6794  xpsnen  6799  xpsneng  6800  xpcomco  6804  xpcomeng  6806  xpassen  6808  xpdom2  6809  xpdom2g  6810  xpf1o  6822  mapen  6824  mapxpen  6826  xpmapenlem  6827  ssenen  6829  phplem4  6833  phplem3g  6834  nneneq  6835  php5  6836  phpm  6843  findcard  6866  findcard2  6867  findcard2s  6868  isinfinf  6875  ac6sfi  6876  exmidpw  6886  exmidpweq  6887  unfidisj  6899  fiintim  6906  xpfi  6907  fisseneq  6909  ssfirab  6911  snexxph  6927  fidcenumlemr  6932  sbthlemi10  6943  isbth  6944  ssfii  6951  fi0  6952  fiss  6954  cnvinfex  6995  eqinfti  6997  infvalti  6999  infglbti  7002  infmoti  7005  ordiso2  7012  djuf1olem  7030  djuss  7047  ctm  7086  ctssdccl  7088  ctssdclemr  7089  finomni  7116  exmidomni  7118  fodjuomnilemdc  7120  nninfwlpoimlemginf  7152  pm54.43  7167  exmidfodomrlemim  7178  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  ccfunen  7226  cc2lem  7228  cc3  7230  indpi  7304  dfplpq2  7316  enq0sym  7394  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nqnq0  7403  mulnnnq0  7412  nqprm  7504  nqprrnd  7505  nqprdisj  7506  nqprloc  7507  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemrl  7535  mulnqprlemru  7536  mulnqprlemfl  7537  mulnqprlemfu  7538  ltnqpr  7555  ltnqpri  7556  archpr  7605  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlem2  7622  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemopu  7661  suplocexprlemmu  7680  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  cnm  7794  ltresr  7801  peano1nnnn  7814  peano2nnnn  7815  axcnre  7843  axpre-apti  7847  renfdisj  7979  dfinfre  8872  1nn  8889  peano2nn  8890  indstr  9552  cnref1o  9609  ioof  9928  fzpr  10033  frec2uzrand  10361  frec2uzf1od  10362  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  frecfzennn  10382  ser3le  10474  hashinfom  10712  hashunlem  10739  hashun  10740  hashxp  10761  hashfacen  10771  zfz1isolem1  10775  zfz1iso  10776  shftfvalg  10782  ovshftex  10783  shftfibg  10784  shftfval  10785  shftfib  10787  shftfn  10788  2shfti  10795  shftvalg  10800  shftval4g  10801  maxabslemval  11172  fimaxre2  11190  xrmaxiflemval  11213  fclim  11257  climshft  11267  zsumdc  11347  fsum3  11350  fsum2dlemstep  11397  fsumcnv  11400  fisumcom2  11401  fisum0diag2  11410  fsumconst  11417  modfsummodlemstep  11420  fsumabs  11428  fsumrelem  11434  fsumiun  11440  ntrivcvgap  11511  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  fprodmodd  11604  algrf  11999  qredeu  12051  isprm2  12071  prmind2  12074  ennnfonelemex  12369  ennnfonelemrn  12374  exmidunben  12381  ctinfom  12383  ctinf  12385  qnnen  12386  enctlem  12387  ctiunctlemfo  12394  slotslfn  12442  restfn  12583  elrest  12586  ismgm  12611  plusffng  12619  fn0g  12629  issgrp  12644  ismnddef  12654  bastg  12855  distop  12879  topnex  12880  epttop  12884  tgrest  12963  resttopon  12965  restco  12968  cnrest2  13030  cnptopresti  13032  cnptoprest  13033  cnptoprest2  13034  txuni2  13050  txbas  13052  eltx  13053  txcnp  13065  txcnmpt  13067  txrest  13070  txdis1cn  13072  txlm  13073  cnmpt1st  13082  cnmpt2nd  13083  txhmeo  13113  txswaphmeolem  13114  xmetec  13231  metrest  13300  reldvg  13442  dvfgg  13451  dvcj  13467  pilem3  13498  bdcvv  13892  bdsnss  13908  bdop  13910  bj-vprc  13931  bdinex1g  13936  bdssexg  13939  bj-inex  13942  bj-zfpair2  13945  bj-uniexg  13953  bdunexb  13955  bj-unexg  13956  bj-indint  13966  bj-ssom  13971  bj-om  13972  bj-2inf  13973  bj-bdfindis  13982  bj-nn0suc0  13985  bj-nnelirr  13988  bj-inf2vnlem1  14005  bj-inf2vnlem2  14006  bj-omex2  14012  bj-nn0sucALT  14013  bj-findis  14014  ss1oel2o  14026  pw1nct  14036  nninfsellemeq  14047  exmidsbthrlem  14054