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  8016  dfinfre  8912  1nn  8929  peano2nn  8930  indstr  9592  cnref1o  9649  ioof  9970  fzpr  10076  frec2uzrand  10404  frec2uzf1od  10405  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  frecfzennn  10425  ser3le  10517  hashinfom  10757  hashunlem  10783  hashun  10784  hashxp  10805  hashfacen  10815  zfz1isolem1  10819  zfz1iso  10820  shftfvalg  10826  ovshftex  10827  shftfibg  10828  shftfval  10829  shftfib  10831  shftfn  10832  2shfti  10839  shftvalg  10844  shftval4g  10845  maxabslemval  11216  fimaxre2  11234  xrmaxiflemval  11257  fclim  11301  climshft  11311  zsumdc  11391  fsum3  11394  fsum2dlemstep  11441  fsumcnv  11444  fisumcom2  11445  fisum0diag2  11454  fsumconst  11461  modfsummodlemstep  11464  fsumabs  11472  fsumrelem  11478  fsumiun  11484  ntrivcvgap  11555  fprod2dlemstep  11629  fprodcnv  11632  fprodcom2fi  11633  fprodmodd  11648  algrf  12044  qredeu  12096  isprm2  12116  prmind2  12119  ennnfonelemex  12414  ennnfonelemrn  12419  exmidunben  12426  ctinfom  12428  ctinf  12430  qnnen  12431  enctlem  12432  ctiunctlemfo  12439  slotslfn  12487  setscomd  12502  restfn  12691  elrest  12694  ptex  12712  prdsex  12717  imasex  12725  imasival  12726  imasbas  12727  imasplusg  12728  imasmulr  12729  imasaddfnlemg  12734  fnpr2ob  12758  ismgm  12775  plusffng  12783  fn0g  12793  issgrp  12808  ismnddef  12818  subgintm  13056  releqgg  13078  eqgfval  13079  eqgval  13080  fnmgp  13130  isring  13181  ringn0  13235  opprunitd  13277  subrgpropd  13367  scaffng  13397  bastg  13531  distop  13555  topnex  13556  epttop  13560  tgrest  13639  resttopon  13641  restco  13644  cnrest2  13706  cnptopresti  13708  cnptoprest  13709  cnptoprest2  13710  txuni2  13726  txbas  13728  eltx  13729  txcnp  13741  txcnmpt  13743  txrest  13746  txdis1cn  13748  txlm  13749  cnmpt1st  13758  cnmpt2nd  13759  txhmeo  13789  txswaphmeolem  13790  xmetec  13907  metrest  13976  reldvg  14118  dvfgg  14127  dvcj  14143  pilem3  14174  bdcvv  14579  bdsnss  14595  bdop  14597  bj-vprc  14618  bdinex1g  14623  bdssexg  14626  bj-inex  14629  bj-zfpair2  14632  bj-uniexg  14640  bdunexb  14642  bj-unexg  14643  bj-indint  14653  bj-ssom  14658  bj-om  14659  bj-2inf  14660  bj-bdfindis  14669  bj-nn0suc0  14672  bj-nnelirr  14675  bj-inf2vnlem1  14692  bj-inf2vnlem2  14693  bj-omex2  14699  bj-nn0sucALT  14700  bj-findis  14701  ss1oel2o  14713  pw1nct  14722  nninfsellemeq  14733  exmidsbthrlem  14740