Theorem vex 2763

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

Syntax hints:   e. wcel 2164   _Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elv  2764  elvd  2765  isset  2766  eqvisset  2770  ralv  2777  rexv  2778  reuv  2779  rmov  2780  rabab  2781  sbhypf  2810  ceqex  2888  ralab  2921  rexab  2923  mo2icl  2940  reu8  2957  csbvarg  3109  csbiebg  3124  sbcnestgf  3133  sbnfc2  3142  ddifnel  3291  ddifstab  3292  csbing  3367  unssdif  3395  unssin  3399  inssun  3400  invdif  3402  vn0  3458  vn0m  3459  eqv  3467  abvor0dc  3471  sbss  3555  velpw  3609  elpwg  3610  velsn  3636  vsnid  3651  exsnrex  3661  dftp2  3668  prmg  3740  prnzg  3743  snssgOLD  3755  difprsnss  3757  sneqrg  3789  preq12bg  3800  pwprss  3832  pwtpss  3833  pwv  3835  unipr  3850  uniprg  3851  unisng  3853  elintg  3879  elintrabg  3884  intss1  3886  ssint  3887  intmin  3891  intss  3892  intssunim  3893  intmin4  3899  intab  3900  intun  3902  intpr  3903  intprg  3904  uniintsnr  3907  iinconstm  3922  iuniin  3923  iinss1  3925  dfiin2g  3946  dfiunv2  3949  ssiinf  3963  iinss  3965  iinss2  3966  0iin  3972  iinab  3975  iundif2ss  3979  iindif2m  3981  iinin2m  3982  iinuniss  3996  sspwuni  3998  pwpwab  4001  iinpw  4004  iunpwss  4005  brab1  4077  csbopabg  4108  mptv  4127  trint  4143  vnex  4161  inex1g  4166  ssexg  4169  inteximm  4179  inuni  4185  repizf2  4192  axpweq  4201  bnd2  4203  pwuni  4222  exmidundif  4236  exmidundifim  4237  zfpair2  4240  rext  4245  sspwb  4246  unipw  4247  ssextss  4250  euabex  4255  mss  4256  exss  4257  opth  4267  opthg  4268  copsexg  4274  copsex4g  4277  moop2  4281  euotd  4284  opabid  4287  elopab  4289  opelopabsbALT  4290  opelopabsb  4291  opabm  4312  pwin  4314  pwunss  4315  epelg  4322  epel  4324  pofun  4344  epse  4374  tron  4414  sucel  4442  suctr  4453  vuniex  4470  uniexg  4471  unexb  4474  snnex  4480  pwnex  4481  uniuni  4483  eusvnf  4485  eusvnfb  4486  iunpw  4512  unon  4544  ordunisuc2r  4547  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  ordsucunielexmid  4564  elirr  4574  en2lp  4587  dtruex  4592  onintexmid  4606  reg3exmidlemwe  4612  dcextest  4614  finds  4633  finds2  4634  elomssom  4638  limom  4647  0nelxp  4688  opelxp  4690  opeliunxp  4715  elvv  4722  elvvv  4723  elvvuni  4724  xpsspw  4772  relopabiv  4786  relopabi  4788  opabid2  4794  difopab  4796  xpiindim  4800  raliunxp  4804  rexiunxp  4805  ralxpf  4809  rexxpf  4810  relop  4813  cnvco  4848  dfrn2  4851  dfdm4  4855  dmss  4862  dmin  4871  dmiun  4872  dmuni  4873  dm0  4877  dmi  4878  reldm0  4881  elreldm  4889  elrnmpt1  4914  dmrnssfld  4926  dmcoss  4932  dmcosseq  4934  opelresg  4950  resieq  4953  dmres  4964  elres  4979  relssres  4981  resopab  4987  resiexg  4988  iss  4989  dfres2  4995  restidsing  4999  dfima2  5008  imadmrn  5016  imai  5022  csbima12g  5027  elimasng  5034  args  5035  epini  5037  iniseg  5038  dfse2  5039  exse2  5040  cotr  5048  issref  5049  cnvsym  5050  intasym  5051  asymref  5052  intirr  5053  brcodir  5054  codir  5055  qfto  5056  poirr2  5059  cnvopab  5068  cnv0  5070  cnvi  5071  cnvdif  5073  rniun  5077  dminss  5081  imainss  5082  inimasn  5084  xpmlem  5087  dmxpss  5097  rnxpid  5101  ssrnres  5109  rninxp  5110  dminxp  5111  cnvcnv3  5116  dfrel2  5117  dmsnm  5132  dmsnopg  5138  cnvcnvsn  5143  dmsnsnsng  5144  cnvsng  5152  elxp4  5154  elxp5  5155  cnvresima  5156  dfco2  5166  dfco2a  5167  cores  5170  resco  5171  imaco  5172  rnco  5173  coiun  5176  co02  5180  coi1  5182  coass  5185  relssdmrn  5187  unielrel  5194  ressn  5207  cnviinm  5208  cnvpom  5209  cnvsom  5210  uniabio  5226  iotaval  5227  iotass  5233  sniota  5246  csbiotag  5248  dffun2  5265  dffun7  5282  dffun8  5283  dffun9  5284  funopg  5289  funssres  5297  funun  5299  funcnvsn  5300  funinsn  5304  funcnv2  5315  funcnv  5316  funcnv3  5317  funcnveq  5318  fun2cnv  5319  funcnvuni  5324  imadif  5335  funimaexglem  5338  isarep1  5341  2elresin  5366  fnres  5371  fcnvres  5438  fconstg  5451  fun11iun  5522  f1osng  5542  dffv3g  5551  fvssunirng  5570  sefvex  5576  fv3  5578  fvres  5579  nfunsn  5590  funimass4  5608  ssimaexg  5620  dmfco  5626  fvopab6  5655  fndmdif  5664  fvelrn  5690  dffo4  5707  f1ompt  5710  fmptco  5725  fsn  5731  fsng  5732  dfmpt  5736  dfmptg  5738  fnressn  5745  fressnfv  5746  fvsng  5755  resfunexg  5780  funfvima3  5793  idref  5800  abrexco  5803  imaiun  5804  dff13  5812  foeqcnvco  5834  f1eqcocnv  5835  fliftcnv  5839  isocnv2  5856  isoini  5862  isose  5865  riotav  5880  csbriotag  5887  acexmidlem2  5916  oprabid  5951  csbov123g  5957  0neqopab  5964  brabvv  5965  dfoprab2  5966  rnoprab  6002  eloprabga  6006  mpov  6009  f1opw  6127  opabex3d  6175  opabex3  6176  ofmres  6190  uchoice  6192  op1stg  6205  op2ndg  6206  1stval2  6210  2ndval2  6211  fo1st  6212  fo2nd  6213  f1stres  6214  f2ndres  6215  fo1stresm  6216  fo2ndresm  6217  xp1st  6220  xp2nd  6221  releldm2  6240  reldm  6241  sbcopeq1a  6242  csbopeq1a  6243  dfoprab3  6246  eloprabi  6251  mpomptsx  6252  dmmpossx  6254  fmpox  6255  mpofvex  6260  mpoexxg  6265  fmpoco  6271  df1st2  6274  df2nd2  6275  1stconst  6276  2ndconst  6277  dfmpo  6278  fo2ndf  6282  f1o2ndf1  6283  xporderlem  6286  cnvoprab  6289  f1od2  6290  brtpos2  6306  reldmtpos  6308  dmtpos  6311  rntpos  6312  ovtposg  6314  dftpos3  6317  dftpos4  6318  tpostpos  6319  tpossym  6331  tfrlem3  6366  tfrlem5  6369  tfrlem8  6373  tfrlemisucfn  6379  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemibex  6384  tfrlemi14d  6388  tfrexlem  6389  tfr1onlem3  6393  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemres  6404  tfri1dALT  6406  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemres  6417  tfrcl  6419  rdgtfr  6429  rdgruledefgg  6430  rdgivallem  6436  rdgon  6441  rdg0g  6443  frec0g  6452  frecabex  6453  frecabcl  6454  frectfr  6455  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecrdg  6463  oafnex  6499  sucinc  6500  fnoa  6502  oaexg  6503  omfnex  6504  fnom  6505  omexg  6506  fnoei  6507  oeiexg  6508  oeiv  6511  oacl  6515  omcl  6516  oeicl  6517  oav2  6518  nnsucelsuc  6546  nnsucuniel  6550  ercnv  6610  iserd  6615  eqerlem  6620  eqer  6621  ecdmn0m  6633  erth  6635  qsss  6650  ecid  6654  ecidg  6655  qsid  6656  iinerm  6663  qsel  6668  erovlem  6683  ecopovsym  6687  ecopover  6689  th3qlem2  6694  mapprc  6708  fnmap  6711  fnpm  6712  mapdm0  6719  mapval2  6734  mapsn  6746  mapsncnv  6751  mapsnf1o2  6752  ixpconstg  6763  ixpprc  6775  ixpin  6779  ixpiinm  6780  ixpssmap2g  6783  ixpssmapg  6784  elixpsn  6791  ixpsnf1o  6792  bren  6803  brdomg  6804  domen  6807  domeng  6808  idssen  6833  ener  6835  domtr  6841  ensn1g  6853  en1  6855  en1bg  6856  fundmen  6862  fundmeng  6863  mapsnen  6867  fiprc  6871  unen  6872  xpsnen  6877  xpsneng  6878  xpcomco  6882  xpcomeng  6884  xpassen  6886  xpdom2  6887  xpdom2g  6888  pw2f1odc  6893  xpf1o  6902  mapen  6904  mapxpen  6906  xpmapenlem  6907  ssenen  6909  phplem4  6913  phplem3g  6914  nneneq  6915  php5  6916  phpm  6923  findcard  6946  findcard2  6947  findcard2s  6948  isinfinf  6955  ac6sfi  6956  exmidpw  6966  exmidpweq  6967  exmidpw2en  6970  unfidisj  6980  fiintim  6987  xpfi  6988  fisseneq  6990  ssfirab  6992  snexxph  7011  fidcenumlemr  7016  sbthlemi10  7027  isbth  7028  ssfii  7035  fi0  7036  fiss  7038  cnvinfex  7079  eqinfti  7081  infvalti  7083  infglbti  7086  infmoti  7089  ordiso2  7096  djuf1olem  7114  djuss  7131  ctm  7170  ctssdccl  7172  ctssdclemr  7173  finomni  7201  exmidomni  7203  fodjuomnilemdc  7205  nninfwlpoimlemginf  7237  pm54.43  7252  exmidfodomrlemim  7263  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  acfun  7269  ccfunen  7326  cc2lem  7328  cc3  7330  indpi  7404  dfplpq2  7416  enq0sym  7494  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nqnq0  7503  mulnnnq0  7512  nqprm  7604  nqprrnd  7605  nqprdisj  7606  nqprloc  7607  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemrl  7635  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  ltnqpr  7655  ltnqpri  7656  archpr  7705  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlem2  7722  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemopu  7761  suplocexprlemmu  7780  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  cnm  7894  ltresr  7901  peano1nnnn  7914  peano2nnnn  7915  axcnre  7943  axpre-apti  7947  renfdisj  8081  dfinfre  8977  1nn  8995  peano2nn  8996  indstr  9661  cnref1o  9719  ioof  10040  fzpr  10146  frec2uzrand  10479  frec2uzf1od  10480  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  frecfzennn  10500  seqp1g  10540  seqclg  10546  seqf1og  10595  seqfeq4g  10605  ser3le  10611  hashinfom  10852  hashunlem  10878  hashun  10879  hashxp  10900  hashfacen  10910  zfz1isolem1  10914  zfz1iso  10915  wrdexb  10929  shftfvalg  10965  ovshftex  10966  shftfibg  10967  shftfval  10968  shftfib  10970  shftfn  10971  2shfti  10978  shftvalg  10983  shftval4g  10984  maxabslemval  11355  fimaxre2  11373  xrmaxiflemval  11396  fclim  11440  climshft  11450  zsumdc  11530  fsum3  11533  fsum2dlemstep  11580  fsumcnv  11583  fisumcom2  11584  fisum0diag2  11593  fsumconst  11600  modfsummodlemstep  11603  fsumabs  11611  fsumrelem  11617  fsumiun  11623  ntrivcvgap  11694  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  fprodmodd  11787  nninfct  12181  algrf  12186  qredeu  12238  isprm2  12258  prmind2  12261  4sqlemafi  12536  4sqlem12  12543  ennnfonelemex  12574  ennnfonelemrn  12579  exmidunben  12586  ctinfom  12588  ctinf  12590  qnnen  12591  enctlem  12592  ctiunctlemfo  12599  slotslfn  12647  setscomd  12662  restfn  12857  elrest  12860  ptex  12878  prdsex  12883  imasex  12891  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfnlemg  12900  fnpr2ob  12926  ismgm  12943  plusffng  12951  fn0g  12961  fngsum  12974  gsumsplit1r  12984  gsumprval  12985  issgrp  12989  ismnddef  13002  gsumfzz  13070  gsumfzcl  13074  mulgnngsum  13200  subgintm  13271  releqgg  13293  eqgex  13294  eqgfval  13295  eqgval  13296  isghm  13316  fnmgp  13421  isrng  13433  isring  13499  ringn0  13559  opprrngbg  13577  opprsubgg  13583  opprunitd  13609  dfrhm2  13653  rhmex  13656  opprsubrngg  13710  subrngintm  13711  subrngpropd  13715  subrgpropd  13752  isdomn  13768  opprdomnbg  13773  scaffng  13808  rmodislmodlem  13849  rmodislmod  13850  lssex  13853  lsssn0  13869  lss1d  13882  lssintclm  13883  ellspsn  13916  rlmfn  13952  isridl  14003  blfn  14050  mopnset  14051  metuex  14054  znval  14135  znleval  14152  psrval  14163  fnpsr  14164  bastg  14240  distop  14264  topnex  14265  epttop  14269  tgrest  14348  resttopon  14350  restco  14353  cnrest2  14415  cnptopresti  14417  cnptoprest  14418  cnptoprest2  14419  txuni2  14435  txbas  14437  eltx  14438  txcnp  14450  txcnmpt  14452  txrest  14455  txdis1cn  14457  txlm  14458  cnmpt1st  14467  cnmpt2nd  14468  txhmeo  14498  txswaphmeolem  14499  xmetec  14616  metrest  14685  reldvg  14858  dvfgg  14867  dvcj  14888  dvmptfsum  14904  elply2  14914  pilem3  14959  lgsquadlem1  15234  lgsquadlem2  15235  bdcvv  15419  bdsnss  15435  bdop  15437  bj-vprc  15458  bdinex1g  15463  bdssexg  15466  bj-inex  15469  bj-zfpair2  15472  bj-uniexg  15480  bdunexb  15482  bj-unexg  15483  bj-indint  15493  bj-ssom  15498  bj-om  15499  bj-2inf  15500  bj-bdfindis  15509  bj-nn0suc0  15512  bj-nnelirr  15515  bj-inf2vnlem1  15532  bj-inf2vnlem2  15533  bj-omex2  15539  bj-nn0sucALT  15540  bj-findis  15541  ss1oel2o  15554  pw1nct  15563  nninfsellemeq  15574  exmidsbthrlem  15582