Theorem vex 2715

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

Syntax hints:   e. wcel 2128   _Vcvv 2712

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714

This theorem is referenced by:  elv  2716  elvd  2717  isset  2718  eqvisset  2722  ralv  2729  rexv  2730  reuv  2731  rmov  2732  rabab  2733  sbhypf  2761  ceqex  2839  ralab  2872  rexab  2874  mo2icl  2891  reu8  2908  csbvarg  3059  csbiebg  3073  sbcnestgf  3082  sbnfc2  3091  ddifnel  3238  ddifstab  3239  csbing  3314  unssdif  3342  unssin  3346  inssun  3347  invdif  3349  vn0  3404  vn0m  3405  eqv  3413  abvor0dc  3417  sbss  3502  velpw  3550  elpwg  3551  velsn  3577  vsnid  3592  exsnrex  3601  dftp2  3608  prmg  3680  prnzg  3683  snssg  3692  difprsnss  3694  sneqrg  3725  preq12bg  3736  pwprss  3768  pwtpss  3769  pwv  3771  unipr  3786  uniprg  3787  unisng  3789  elintg  3815  elintrabg  3820  intss1  3822  ssint  3823  intmin  3827  intss  3828  intssunim  3829  intmin4  3835  intab  3836  intun  3838  intpr  3839  intprg  3840  uniintsnr  3843  iinconstm  3858  iuniin  3859  iinss1  3861  dfiin2g  3882  dfiunv2  3885  ssiinf  3898  iinss  3900  iinss2  3901  0iin  3907  iinab  3910  iundif2ss  3914  iindif2m  3916  iinin2m  3917  iinuniss  3931  sspwuni  3933  pwpwab  3936  iinpw  3939  iunpwss  3940  brab1  4011  csbopabg  4042  mptv  4061  trint  4077  vnex  4095  inex1g  4100  ssexg  4103  inteximm  4110  inuni  4116  repizf2  4122  axpweq  4131  bnd2  4133  pwuni  4152  exmidundif  4166  exmidundifim  4167  zfpair2  4169  rext  4174  sspwb  4175  unipw  4176  ssextss  4179  euabex  4184  mss  4185  exss  4186  opth  4196  opthg  4197  copsexg  4203  copsex4g  4206  moop2  4210  euotd  4213  opabid  4216  elopab  4217  opelopabsbALT  4218  opelopabsb  4219  opabm  4239  pwin  4241  pwunss  4242  epelg  4249  epel  4251  pofun  4271  epse  4301  tron  4341  sucel  4369  suctr  4380  vuniex  4397  uniexg  4398  unexb  4400  snnex  4406  pwnex  4407  uniuni  4409  eusvnf  4411  eusvnfb  4412  iunpw  4438  unon  4468  ordunisuc2r  4471  ordtri2or2exmidlem  4483  onsucelsucexmidlem  4486  ordsucunielexmid  4488  elirr  4498  en2lp  4511  dtruex  4516  onintexmid  4530  reg3exmidlemwe  4536  dcextest  4538  finds  4557  finds2  4558  elomssom  4562  limom  4571  0nelxp  4611  opelxp  4613  opeliunxp  4638  elvv  4645  elvvv  4646  elvvuni  4647  xpsspw  4695  relopabi  4709  opabid2  4714  difopab  4716  xpiindim  4720  raliunxp  4724  rexiunxp  4725  ralxpf  4729  rexxpf  4730  relop  4733  cnvco  4768  dfrn2  4771  dfdm4  4775  dmss  4782  dmin  4791  dmiun  4792  dmuni  4793  dm0  4797  dmi  4798  reldm0  4801  elreldm  4809  elrnmpt1  4834  dmrnssfld  4846  dmcoss  4852  dmcosseq  4854  opelresg  4870  resieq  4873  dmres  4884  elres  4899  relssres  4901  resopab  4907  resiexg  4908  iss  4909  dfres2  4915  dfima2  4927  imadmrn  4935  imai  4939  csbima12g  4944  elimasng  4951  args  4952  epini  4954  iniseg  4955  dfse2  4956  exse2  4957  cotr  4964  issref  4965  cnvsym  4966  intasym  4967  asymref  4968  intirr  4969  brcodir  4970  codir  4971  qfto  4972  poirr2  4975  cnvopab  4984  cnv0  4986  cnvi  4987  cnvdif  4989  rniun  4993  dminss  4997  imainss  4998  inimasn  5000  xpmlem  5003  dmxpss  5013  rnxpid  5017  ssrnres  5025  rninxp  5026  dminxp  5027  cnvcnv3  5032  dfrel2  5033  dmsnm  5048  dmsnopg  5054  cnvcnvsn  5059  dmsnsnsng  5060  cnvsng  5068  elxp4  5070  elxp5  5071  cnvresima  5072  dfco2  5082  dfco2a  5083  cores  5086  resco  5087  imaco  5088  rnco  5089  coiun  5092  co02  5096  coi1  5098  coass  5101  relssdmrn  5103  unielrel  5110  ressn  5123  cnviinm  5124  cnvpom  5125  cnvsom  5126  uniabio  5142  iotaval  5143  iotass  5149  sniota  5159  csbiotag  5160  dffun2  5177  dffun7  5194  dffun8  5195  dffun9  5196  funopg  5201  funssres  5209  funun  5211  funcnvsn  5212  funinsn  5216  funcnv2  5227  funcnv  5228  funcnv3  5229  funcnveq  5230  fun2cnv  5231  funcnvuni  5236  imadif  5247  funimaexglem  5250  isarep1  5253  2elresin  5278  fnres  5283  fcnvres  5350  fconstg  5363  fun11iun  5432  f1osng  5452  dffv3g  5461  fvssunirng  5480  sefvex  5486  fv3  5488  fvres  5489  nfunsn  5499  funimass4  5516  ssimaexg  5527  dmfco  5533  fvopab6  5561  fndmdif  5569  fvelrn  5595  dffo4  5612  f1ompt  5615  fmptco  5630  fsn  5636  fsng  5637  dfmpt  5641  dfmptg  5643  fnressn  5650  fressnfv  5651  fvsng  5660  resfunexg  5685  funfvima3  5695  idref  5702  abrexco  5704  imaiun  5705  dff13  5713  foeqcnvco  5735  f1eqcocnv  5736  fliftcnv  5740  isocnv2  5757  isoini  5763  isose  5766  riotav  5779  csbriotag  5786  acexmidlem2  5815  oprabid  5847  csbov123g  5853  0neqopab  5860  brabvv  5861  dfoprab2  5862  rnoprab  5898  eloprabga  5902  mpov  5905  f1opw  6021  opabex3d  6063  opabex3  6064  ofmres  6078  op1stg  6092  op2ndg  6093  1stval2  6097  2ndval2  6098  fo1st  6099  fo2nd  6100  f1stres  6101  f2ndres  6102  fo1stresm  6103  fo2ndresm  6104  xp1st  6107  xp2nd  6108  releldm2  6127  reldm  6128  sbcopeq1a  6129  csbopeq1a  6130  dfoprab3  6133  eloprabi  6138  mpomptsx  6139  dmmpossx  6141  fmpox  6142  mpofvex  6145  mpoexxg  6152  fmpoco  6157  df1st2  6160  df2nd2  6161  1stconst  6162  2ndconst  6163  dfmpo  6164  fo2ndf  6168  f1o2ndf1  6169  xporderlem  6172  cnvoprab  6175  f1od2  6176  brtpos2  6192  reldmtpos  6194  dmtpos  6197  rntpos  6198  ovtposg  6200  dftpos3  6203  dftpos4  6204  tpostpos  6205  tpossym  6217  tfrlem3  6252  tfrlem5  6255  tfrlem8  6259  tfrlemisucfn  6265  tfrlemisucaccv  6266  tfrlemibxssdm  6268  tfrlemibfn  6269  tfrlemibex  6270  tfrlemi14d  6274  tfrexlem  6275  tfr1onlem3  6279  tfr1onlemsucaccv  6282  tfr1onlembxssdm  6284  tfr1onlembfn  6285  tfr1onlemres  6290  tfri1dALT  6292  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  tfrcllembfn  6298  tfrcllemres  6303  tfrcl  6305  rdgtfr  6315  rdgruledefgg  6316  rdgivallem  6322  rdgon  6327  rdg0g  6329  frec0g  6338  frecabex  6339  frecabcl  6340  frectfr  6341  freccllem  6343  frecfcllem  6345  frecsuclem  6347  frecrdg  6349  oafnex  6384  sucinc  6385  fnoa  6387  oaexg  6388  omfnex  6389  fnom  6390  omexg  6391  fnoei  6392  oeiexg  6393  oeiv  6396  oacl  6400  omcl  6401  oeicl  6402  oav2  6403  nnsucelsuc  6431  nnsucuniel  6435  ercnv  6494  iserd  6499  eqerlem  6504  eqer  6505  ecdmn0m  6515  erth  6517  qsss  6532  ecid  6536  ecidg  6537  qsid  6538  iinerm  6545  qsel  6550  erovlem  6565  ecopovsym  6569  ecopover  6571  th3qlem2  6576  mapprc  6590  fnmap  6593  fnpm  6594  mapdm0  6601  mapval2  6616  mapsn  6628  mapsncnv  6633  mapsnf1o2  6634  ixpconstg  6645  ixpprc  6657  ixpin  6661  ixpiinm  6662  ixpssmap2g  6665  ixpssmapg  6666  elixpsn  6673  ixpsnf1o  6674  bren  6685  brdomg  6686  domen  6689  domeng  6690  idssen  6715  ener  6717  domtr  6723  ensn1g  6735  en1  6737  en1bg  6738  fundmen  6744  fundmeng  6745  mapsnen  6749  fiprc  6753  unen  6754  xpsnen  6759  xpsneng  6760  xpcomco  6764  xpcomeng  6766  xpassen  6768  xpdom2  6769  xpdom2g  6770  xpf1o  6782  mapen  6784  mapxpen  6786  xpmapenlem  6787  ssenen  6789  phplem4  6793  phplem3g  6794  nneneq  6795  php5  6796  phpm  6803  findcard  6826  findcard2  6827  findcard2s  6828  isinfinf  6835  ac6sfi  6836  exmidpw  6846  exmidpweq  6847  unfidisj  6859  fiintim  6866  xpfi  6867  fisseneq  6869  ssfirab  6871  snexxph  6887  fidcenumlemr  6892  sbthlemi10  6903  isbth  6904  ssfii  6911  fi0  6912  fiss  6914  cnvinfex  6954  eqinfti  6956  infvalti  6958  infglbti  6961  infmoti  6964  ordiso2  6969  djuf1olem  6987  djuss  7004  ctm  7043  ctssdccl  7045  ctssdclemr  7046  finomni  7066  exmidomni  7068  fodjuomnilemdc  7070  pm54.43  7108  exmidfodomrlemim  7119  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  acfun  7125  ccfunen  7167  cc2lem  7169  cc3  7171  indpi  7245  dfplpq2  7257  enq0sym  7335  enq0ref  7336  enq0tr  7337  nqnq0pi  7341  nqnq0  7344  mulnnnq0  7353  nqprm  7445  nqprrnd  7446  nqprdisj  7447  nqprloc  7448  nqprl  7454  nqpru  7455  addnqprlemrl  7460  addnqprlemru  7461  addnqprlemfl  7462  addnqprlemfu  7463  mulnqprlemrl  7476  mulnqprlemru  7477  mulnqprlemfl  7478  mulnqprlemfu  7479  ltnqpr  7496  ltnqpri  7497  archpr  7546  cauappcvgprlemladdfu  7557  cauappcvgprlemladdfl  7558  cauappcvgprlem2  7563  caucvgprlemladdfu  7580  caucvgprlem2  7583  caucvgprprlemopu  7602  suplocexprlemmu  7621  suplocexprlemdisj  7623  suplocexprlemloc  7624  suplocexprlemub  7626  cnm  7735  ltresr  7742  peano1nnnn  7755  peano2nnnn  7756  axcnre  7784  axpre-apti  7788  renfdisj  7920  dfinfre  8810  1nn  8827  peano2nn  8828  indstr  9487  cnref1o  9541  ioof  9857  fzpr  9961  frec2uzrand  10286  frec2uzf1od  10287  frecuzrdgtcl  10293  frecuzrdgfunlem  10300  frecfzennn  10307  ser3le  10399  hashinfom  10634  hashunlem  10660  hashun  10661  hashxp  10682  hashfacen  10689  zfz1isolem1  10693  zfz1iso  10694  shftfvalg  10700  ovshftex  10701  shftfibg  10702  shftfval  10703  shftfib  10705  shftfn  10706  2shfti  10713  shftvalg  10718  shftval4g  10719  maxabslemval  11090  fimaxre2  11108  xrmaxiflemval  11129  fclim  11173  climshft  11183  zsumdc  11263  fsum3  11266  fsum2dlemstep  11313  fsumcnv  11316  fisumcom2  11317  fisum0diag2  11326  fsumconst  11333  modfsummodlemstep  11336  fsumabs  11344  fsumrelem  11350  fsumiun  11356  ntrivcvgap  11427  fprod2dlemstep  11501  fprodcnv  11504  fprodcom2fi  11505  fprodmodd  11520  algrf  11902  qredeu  11954  isprm2  11974  prmind2  11977  ennnfonelemex  12115  ennnfonelemrn  12120  exmidunben  12127  ctinfom  12129  ctinf  12131  qnnen  12132  enctlem  12133  ctiunctlemfo  12140  slotslfn  12176  restfn  12315  elrest  12318  bastg  12421  distop  12445  topnex  12446  epttop  12450  tgrest  12529  resttopon  12531  restco  12534  cnrest2  12596  cnptopresti  12598  cnptoprest  12599  cnptoprest2  12600  txuni2  12616  txbas  12618  eltx  12619  txcnp  12631  txcnmpt  12633  txrest  12636  txdis1cn  12638  txlm  12639  cnmpt1st  12648  cnmpt2nd  12649  txhmeo  12679  txswaphmeolem  12680  xmetec  12797  metrest  12866  reldvg  13008  dvfgg  13017  dvcj  13033  pilem3  13064  bdcvv  13392  bdsnss  13408  bdop  13410  bj-vprc  13431  bdinex1g  13436  bdssexg  13439  bj-inex  13442  bj-zfpair2  13445  bj-uniexg  13453  bdunexb  13455  bj-unexg  13456  bj-indint  13466  bj-ssom  13471  bj-om  13472  bj-2inf  13473  bj-bdfindis  13482  bj-nn0suc0  13485  bj-nnelirr  13488  bj-inf2vnlem1  13505  bj-inf2vnlem2  13506  bj-omex2  13512  bj-nn0sucALT  13513  bj-findis  13514  ss1oel2o  13526  pw1nct  13536  nninfsellemeq  13549  exmidsbthrlem  13556