Theorem vex 2740

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

Syntax hints:   e. wcel 2148   _Vcvv 2737

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739

This theorem is referenced by:  elv  2741  elvd  2742  isset  2743  eqvisset  2747  ralv  2754  rexv  2755  reuv  2756  rmov  2757  rabab  2758  sbhypf  2786  ceqex  2864  ralab  2897  rexab  2899  mo2icl  2916  reu8  2933  csbvarg  3085  csbiebg  3099  sbcnestgf  3108  sbnfc2  3117  ddifnel  3266  ddifstab  3267  csbing  3342  unssdif  3370  unssin  3374  inssun  3375  invdif  3377  vn0  3433  vn0m  3434  eqv  3442  abvor0dc  3446  sbss  3531  velpw  3582  elpwg  3583  velsn  3609  vsnid  3624  exsnrex  3634  dftp2  3641  prmg  3713  prnzg  3716  snssgOLD  3728  difprsnss  3730  sneqrg  3762  preq12bg  3773  pwprss  3805  pwtpss  3806  pwv  3808  unipr  3823  uniprg  3824  unisng  3826  elintg  3852  elintrabg  3857  intss1  3859  ssint  3860  intmin  3864  intss  3865  intssunim  3866  intmin4  3872  intab  3873  intun  3875  intpr  3876  intprg  3877  uniintsnr  3880  iinconstm  3895  iuniin  3896  iinss1  3898  dfiin2g  3919  dfiunv2  3922  ssiinf  3936  iinss  3938  iinss2  3939  0iin  3945  iinab  3948  iundif2ss  3952  iindif2m  3954  iinin2m  3955  iinuniss  3969  sspwuni  3971  pwpwab  3974  iinpw  3977  iunpwss  3978  brab1  4050  csbopabg  4081  mptv  4100  trint  4116  vnex  4134  inex1g  4139  ssexg  4142  inteximm  4149  inuni  4155  repizf2  4162  axpweq  4171  bnd2  4173  pwuni  4192  exmidundif  4206  exmidundifim  4207  zfpair2  4210  rext  4215  sspwb  4216  unipw  4217  ssextss  4220  euabex  4225  mss  4226  exss  4227  opth  4237  opthg  4238  copsexg  4244  copsex4g  4247  moop2  4251  euotd  4254  opabid  4257  elopab  4258  opelopabsbALT  4259  opelopabsb  4260  opabm  4280  pwin  4282  pwunss  4283  epelg  4290  epel  4292  pofun  4312  epse  4342  tron  4382  sucel  4410  suctr  4421  vuniex  4438  uniexg  4439  unexb  4442  snnex  4448  pwnex  4449  uniuni  4451  eusvnf  4453  eusvnfb  4454  iunpw  4480  unon  4510  ordunisuc2r  4513  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  ordsucunielexmid  4530  elirr  4540  en2lp  4553  dtruex  4558  onintexmid  4572  reg3exmidlemwe  4578  dcextest  4580  finds  4599  finds2  4600  elomssom  4604  limom  4613  0nelxp  4654  opelxp  4656  opeliunxp  4681  elvv  4688  elvvv  4689  elvvuni  4690  xpsspw  4738  relopabi  4752  opabid2  4758  difopab  4760  xpiindim  4764  raliunxp  4768  rexiunxp  4769  ralxpf  4773  rexxpf  4774  relop  4777  cnvco  4812  dfrn2  4815  dfdm4  4819  dmss  4826  dmin  4835  dmiun  4836  dmuni  4837  dm0  4841  dmi  4842  reldm0  4845  elreldm  4853  elrnmpt1  4878  dmrnssfld  4890  dmcoss  4896  dmcosseq  4898  opelresg  4914  resieq  4917  dmres  4928  elres  4943  relssres  4945  resopab  4951  resiexg  4952  iss  4953  dfres2  4959  restidsing  4963  dfima2  4972  imadmrn  4980  imai  4984  csbima12g  4989  elimasng  4996  args  4997  epini  4999  iniseg  5000  dfse2  5001  exse2  5002  cotr  5010  issref  5011  cnvsym  5012  intasym  5013  asymref  5014  intirr  5015  brcodir  5016  codir  5017  qfto  5018  poirr2  5021  cnvopab  5030  cnv0  5032  cnvi  5033  cnvdif  5035  rniun  5039  dminss  5043  imainss  5044  inimasn  5046  xpmlem  5049  dmxpss  5059  rnxpid  5063  ssrnres  5071  rninxp  5072  dminxp  5073  cnvcnv3  5078  dfrel2  5079  dmsnm  5094  dmsnopg  5100  cnvcnvsn  5105  dmsnsnsng  5106  cnvsng  5114  elxp4  5116  elxp5  5117  cnvresima  5118  dfco2  5128  dfco2a  5129  cores  5132  resco  5133  imaco  5134  rnco  5135  coiun  5138  co02  5142  coi1  5144  coass  5147  relssdmrn  5149  unielrel  5156  ressn  5169  cnviinm  5170  cnvpom  5171  cnvsom  5172  uniabio  5188  iotaval  5189  iotass  5195  sniota  5207  csbiotag  5209  dffun2  5226  dffun7  5243  dffun8  5244  dffun9  5245  funopg  5250  funssres  5258  funun  5260  funcnvsn  5261  funinsn  5265  funcnv2  5276  funcnv  5277  funcnv3  5278  funcnveq  5279  fun2cnv  5280  funcnvuni  5285  imadif  5296  funimaexglem  5299  isarep1  5302  2elresin  5327  fnres  5332  fcnvres  5399  fconstg  5412  fun11iun  5482  f1osng  5502  dffv3g  5511  fvssunirng  5530  sefvex  5536  fv3  5538  fvres  5539  nfunsn  5549  funimass4  5566  ssimaexg  5578  dmfco  5584  fvopab6  5612  fndmdif  5621  fvelrn  5647  dffo4  5664  f1ompt  5667  fmptco  5682  fsn  5688  fsng  5689  dfmpt  5693  dfmptg  5695  fnressn  5702  fressnfv  5703  fvsng  5712  resfunexg  5737  funfvima3  5750  idref  5757  abrexco  5759  imaiun  5760  dff13  5768  foeqcnvco  5790  f1eqcocnv  5791  fliftcnv  5795  isocnv2  5812  isoini  5818  isose  5821  riotav  5835  csbriotag  5842  acexmidlem2  5871  oprabid  5906  csbov123g  5912  0neqopab  5919  brabvv  5920  dfoprab2  5921  rnoprab  5957  eloprabga  5961  mpov  5964  f1opw  6077  opabex3d  6121  opabex3  6122  ofmres  6136  op1stg  6150  op2ndg  6151  1stval2  6155  2ndval2  6156  fo1st  6157  fo2nd  6158  f1stres  6159  f2ndres  6160  fo1stresm  6161  fo2ndresm  6162  xp1st  6165  xp2nd  6166  releldm2  6185  reldm  6186  sbcopeq1a  6187  csbopeq1a  6188  dfoprab3  6191  eloprabi  6196  mpomptsx  6197  dmmpossx  6199  fmpox  6200  mpofvex  6203  mpoexxg  6210  fmpoco  6216  df1st2  6219  df2nd2  6220  1stconst  6221  2ndconst  6222  dfmpo  6223  fo2ndf  6227  f1o2ndf1  6228  xporderlem  6231  cnvoprab  6234  f1od2  6235  brtpos2  6251  reldmtpos  6253  dmtpos  6256  rntpos  6257  ovtposg  6259  dftpos3  6262  dftpos4  6263  tpostpos  6264  tpossym  6276  tfrlem3  6311  tfrlem5  6314  tfrlem8  6318  tfrlemisucfn  6324  tfrlemisucaccv  6325  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrlemibex  6329  tfrlemi14d  6333  tfrexlem  6334  tfr1onlem3  6338  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemres  6349  tfri1dALT  6351  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemres  6362  tfrcl  6364  rdgtfr  6374  rdgruledefgg  6375  rdgivallem  6381  rdgon  6386  rdg0g  6388  frec0g  6397  frecabex  6398  frecabcl  6399  frectfr  6400  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecrdg  6408  oafnex  6444  sucinc  6445  fnoa  6447  oaexg  6448  omfnex  6449  fnom  6450  omexg  6451  fnoei  6452  oeiexg  6453  oeiv  6456  oacl  6460  omcl  6461  oeicl  6462  oav2  6463  nnsucelsuc  6491  nnsucuniel  6495  ercnv  6555  iserd  6560  eqerlem  6565  eqer  6566  ecdmn0m  6576  erth  6578  qsss  6593  ecid  6597  ecidg  6598  qsid  6599  iinerm  6606  qsel  6611  erovlem  6626  ecopovsym  6630  ecopover  6632  th3qlem2  6637  mapprc  6651  fnmap  6654  fnpm  6655  mapdm0  6662  mapval2  6677  mapsn  6689  mapsncnv  6694  mapsnf1o2  6695  ixpconstg  6706  ixpprc  6718  ixpin  6722  ixpiinm  6723  ixpssmap2g  6726  ixpssmapg  6727  elixpsn  6734  ixpsnf1o  6735  bren  6746  brdomg  6747  domen  6750  domeng  6751  idssen  6776  ener  6778  domtr  6784  ensn1g  6796  en1  6798  en1bg  6799  fundmen  6805  fundmeng  6806  mapsnen  6810  fiprc  6814  unen  6815  xpsnen  6820  xpsneng  6821  xpcomco  6825  xpcomeng  6827  xpassen  6829  xpdom2  6830  xpdom2g  6831  xpf1o  6843  mapen  6845  mapxpen  6847  xpmapenlem  6848  ssenen  6850  phplem4  6854  phplem3g  6855  nneneq  6856  php5  6857  phpm  6864  findcard  6887  findcard2  6888  findcard2s  6889  isinfinf  6896  ac6sfi  6897  exmidpw  6907  exmidpweq  6908  unfidisj  6920  fiintim  6927  xpfi  6928  fisseneq  6930  ssfirab  6932  snexxph  6948  fidcenumlemr  6953  sbthlemi10  6964  isbth  6965  ssfii  6972  fi0  6973  fiss  6975  cnvinfex  7016  eqinfti  7018  infvalti  7020  infglbti  7023  infmoti  7026  ordiso2  7033  djuf1olem  7051  djuss  7068  ctm  7107  ctssdccl  7109  ctssdclemr  7110  finomni  7137  exmidomni  7139  fodjuomnilemdc  7141  nninfwlpoimlemginf  7173  pm54.43  7188  exmidfodomrlemim  7199  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  acfun  7205  ccfunen  7262  cc2lem  7264  cc3  7266  indpi  7340  dfplpq2  7352  enq0sym  7430  enq0ref  7431  enq0tr  7432  nqnq0pi  7436  nqnq0  7439  mulnnnq0  7448  nqprm  7540  nqprrnd  7541  nqprdisj  7542  nqprloc  7543  nqprl  7549  nqpru  7550  addnqprlemrl  7555  addnqprlemru  7556  addnqprlemfl  7557  addnqprlemfu  7558  mulnqprlemrl  7571  mulnqprlemru  7572  mulnqprlemfl  7573  mulnqprlemfu  7574  ltnqpr  7591  ltnqpri  7592  archpr  7641  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlem2  7658  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemopu  7697  suplocexprlemmu  7716  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  cnm  7830  ltresr  7837  peano1nnnn  7850  peano2nnnn  7851  axcnre  7879  axpre-apti  7883  renfdisj  8015  dfinfre  8911  1nn  8928  peano2nn  8929  indstr  9591  cnref1o  9648  ioof  9969  fzpr  10074  frec2uzrand  10402  frec2uzf1od  10403  frecuzrdgtcl  10409  frecuzrdgfunlem  10416  frecfzennn  10423  ser3le  10515  hashinfom  10753  hashunlem  10779  hashun  10780  hashxp  10801  hashfacen  10811  zfz1isolem1  10815  zfz1iso  10816  shftfvalg  10822  ovshftex  10823  shftfibg  10824  shftfval  10825  shftfib  10827  shftfn  10828  2shfti  10835  shftvalg  10840  shftval4g  10841  maxabslemval  11212  fimaxre2  11230  xrmaxiflemval  11253  fclim  11297  climshft  11307  zsumdc  11387  fsum3  11390  fsum2dlemstep  11437  fsumcnv  11440  fisumcom2  11441  fisum0diag2  11450  fsumconst  11457  modfsummodlemstep  11460  fsumabs  11468  fsumrelem  11474  fsumiun  11480  ntrivcvgap  11551  fprod2dlemstep  11625  fprodcnv  11628  fprodcom2fi  11629  fprodmodd  11644  algrf  12039  qredeu  12091  isprm2  12111  prmind2  12114  ennnfonelemex  12409  ennnfonelemrn  12414  exmidunben  12421  ctinfom  12423  ctinf  12425  qnnen  12426  enctlem  12427  ctiunctlemfo  12434  slotslfn  12482  setscomd  12497  restfn  12686  elrest  12689  ptex  12707  prdsex  12712  imasex  12720  imasival  12721  imasbas  12722  imasplusg  12723  imasmulr  12724  imasaddfnlemg  12729  fnpr2ob  12753  ismgm  12770  plusffng  12778  fn0g  12788  issgrp  12803  ismnddef  12813  subgintm  13051  releqgg  13073  eqgfval  13074  eqgval  13075  fnmgp  13125  isring  13176  ringn0  13230  opprunitd  13272  subrgpropd  13369  bastg  13492  distop  13516  topnex  13517  epttop  13521  tgrest  13600  resttopon  13602  restco  13605  cnrest2  13667  cnptopresti  13669  cnptoprest  13670  cnptoprest2  13671  txuni2  13687  txbas  13689  eltx  13690  txcnp  13702  txcnmpt  13704  txrest  13707  txdis1cn  13709  txlm  13710  cnmpt1st  13719  cnmpt2nd  13720  txhmeo  13750  txswaphmeolem  13751  xmetec  13868  metrest  13937  reldvg  14079  dvfgg  14088  dvcj  14104  pilem3  14135  bdcvv  14529  bdsnss  14545  bdop  14547  bj-vprc  14568  bdinex1g  14573  bdssexg  14576  bj-inex  14579  bj-zfpair2  14582  bj-uniexg  14590  bdunexb  14592  bj-unexg  14593  bj-indint  14603  bj-ssom  14608  bj-om  14609  bj-2inf  14610  bj-bdfindis  14619  bj-nn0suc0  14622  bj-nnelirr  14625  bj-inf2vnlem1  14642  bj-inf2vnlem2  14643  bj-omex2  14649  bj-nn0sucALT  14650  bj-findis  14651  ss1oel2o  14663  pw1nct  14672  nninfsellemeq  14683  exmidsbthrlem  14690