Theorem vex 2684

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

Syntax hints:   e. wcel 1480   _Vcvv 2681

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-v 2683

This theorem is referenced by:  elv  2685  elvd  2686  isset  2687  eqvisset  2691  ralv  2698  rexv  2699  reuv  2700  rmov  2701  rabab  2702  sbhypf  2730  ceqex  2807  ralab  2839  rexab  2841  mo2icl  2858  reu8  2875  csbvarg  3025  csbiebg  3037  sbcnestgf  3046  sbnfc2  3055  ddifnel  3202  ddifstab  3203  csbing  3278  unssdif  3306  unssin  3310  inssun  3311  invdif  3313  vn0  3368  vn0m  3369  eqv  3377  abvor0dc  3381  sbss  3466  velpw  3512  elpwg  3513  velsn  3539  vsnid  3552  exsnrex  3561  dftp2  3567  prmg  3639  prnzg  3642  snssg  3651  difprsnss  3653  sneqrg  3684  preq12bg  3695  pwprss  3727  pwtpss  3728  pwv  3730  unipr  3745  uniprg  3746  unisng  3748  elintg  3774  elintrabg  3779  intss1  3781  ssint  3782  intmin  3786  intss  3787  intssunim  3788  intmin4  3794  intab  3795  intun  3797  intpr  3798  intprg  3799  uniintsnr  3802  iinconstm  3817  iuniin  3818  iinss1  3820  dfiin2g  3841  dfiunv2  3844  ssiinf  3857  iinss  3859  iinss2  3860  0iin  3866  iinab  3869  iundif2ss  3873  iindif2m  3875  iinin2m  3876  iinuniss  3890  sspwuni  3892  pwpwab  3895  iinpw  3898  iunpwss  3899  brab1  3970  csbopabg  4001  mptv  4020  trint  4036  vnex  4054  inex1g  4059  ssexg  4062  inteximm  4069  inuni  4075  repizf2  4081  axpweq  4090  bnd2  4092  pwuni  4111  exmidundif  4124  exmidundifim  4125  zfpair2  4127  rext  4132  sspwb  4133  unipw  4134  ssextss  4137  euabex  4142  mss  4143  exss  4144  opth  4154  opthg  4155  copsexg  4161  copsex4g  4164  moop2  4168  euotd  4171  opabid  4174  elopab  4175  opelopabsbALT  4176  opelopabsb  4177  opabm  4197  pwin  4199  pwunss  4200  epelg  4207  epel  4209  pofun  4229  epse  4259  tron  4299  sucel  4327  suctr  4338  vuniex  4355  uniexg  4356  unexb  4358  snnex  4364  pwnex  4365  uniuni  4367  eusvnf  4369  eusvnfb  4370  iunpw  4396  unon  4422  ordunisuc2r  4425  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  ordsucunielexmid  4441  elirr  4451  en2lp  4464  dtruex  4469  onintexmid  4482  reg3exmidlemwe  4488  dcextest  4490  finds  4509  finds2  4510  elnn  4514  limom  4522  0nelxp  4562  opelxp  4564  opeliunxp  4589  elvv  4596  elvvv  4597  elvvuni  4598  xpsspw  4646  relopabi  4660  opabid2  4665  difopab  4667  xpiindim  4671  raliunxp  4675  rexiunxp  4676  ralxpf  4680  rexxpf  4681  relop  4684  cnvco  4719  dfrn2  4722  dfdm4  4726  dmss  4733  dmin  4742  dmiun  4743  dmuni  4744  dm0  4748  dmi  4749  reldm0  4752  elreldm  4760  elrnmpt1  4785  dmrnssfld  4797  dmcoss  4803  dmcosseq  4805  opelresg  4821  resieq  4824  dmres  4835  elres  4850  relssres  4852  resopab  4858  resiexg  4859  iss  4860  dfres2  4866  dfima2  4878  imadmrn  4886  imai  4890  csbima12g  4895  elimasng  4902  args  4903  epini  4905  iniseg  4906  dfse2  4907  exse2  4908  cotr  4915  issref  4916  cnvsym  4917  intasym  4918  asymref  4919  intirr  4920  brcodir  4921  codir  4922  qfto  4923  poirr2  4926  cnvopab  4935  cnv0  4937  cnvi  4938  cnvdif  4940  rniun  4944  dminss  4948  imainss  4949  inimasn  4951  xpmlem  4954  dmxpss  4964  rnxpid  4968  ssrnres  4976  rninxp  4977  dminxp  4978  cnvcnv3  4983  dfrel2  4984  dmsnm  4999  dmsnopg  5005  cnvcnvsn  5010  dmsnsnsng  5011  cnvsng  5019  elxp4  5021  elxp5  5022  cnvresima  5023  dfco2  5033  dfco2a  5034  cores  5037  resco  5038  imaco  5039  rnco  5040  coiun  5043  co02  5047  coi1  5049  coass  5052  relssdmrn  5054  unielrel  5061  ressn  5074  cnviinm  5075  cnvpom  5076  cnvsom  5077  uniabio  5093  iotaval  5094  iotass  5100  sniota  5110  csbiotag  5111  dffun2  5128  dffun7  5145  dffun8  5146  dffun9  5147  funopg  5152  funssres  5160  funun  5162  funcnvsn  5163  funinsn  5167  funcnv2  5178  funcnv  5179  funcnv3  5180  funcnveq  5181  fun2cnv  5182  funcnvuni  5187  imadif  5198  funimaexglem  5201  isarep1  5204  2elresin  5229  fnres  5234  fcnvres  5301  fconstg  5314  fun11iun  5381  f1osng  5401  dffv3g  5410  fvssunirng  5429  sefvex  5435  fv3  5437  fvres  5438  nfunsn  5448  funimass4  5465  ssimaexg  5476  dmfco  5482  fvopab6  5510  fndmdif  5518  fvelrn  5544  dffo4  5561  f1ompt  5564  fmptco  5579  fsn  5585  fsng  5586  dfmpt  5590  dfmptg  5592  fnressn  5599  fressnfv  5600  fvsng  5609  resfunexg  5634  funfvima3  5644  idref  5651  abrexco  5653  imaiun  5654  dff13  5662  foeqcnvco  5684  f1eqcocnv  5685  fliftcnv  5689  isocnv2  5706  isoini  5712  isose  5715  riotav  5728  csbriotag  5735  acexmidlem2  5764  oprabid  5796  csbov123g  5802  0neqopab  5809  brabvv  5810  dfoprab2  5811  rnoprab  5847  eloprabga  5851  mpov  5854  f1opw  5970  opabex3d  6012  opabex3  6013  ofmres  6027  op1stg  6041  op2ndg  6042  1stval2  6046  2ndval2  6047  fo1st  6048  fo2nd  6049  f1stres  6050  f2ndres  6051  fo1stresm  6052  fo2ndresm  6053  xp1st  6056  xp2nd  6057  releldm2  6076  reldm  6077  sbcopeq1a  6078  csbopeq1a  6079  dfoprab3  6082  eloprabi  6087  mpomptsx  6088  dmmpossx  6090  fmpox  6091  mpofvex  6094  mpoexxg  6101  fmpoco  6106  df1st2  6109  df2nd2  6110  1stconst  6111  2ndconst  6112  dfmpo  6113  fo2ndf  6117  f1o2ndf1  6118  xporderlem  6121  cnvoprab  6124  f1od2  6125  brtpos2  6141  reldmtpos  6143  dmtpos  6146  rntpos  6147  ovtposg  6149  dftpos3  6152  dftpos4  6153  tpostpos  6154  tpossym  6166  tfrlem3  6201  tfrlem5  6204  tfrlem8  6208  tfrlemisucfn  6214  tfrlemisucaccv  6215  tfrlemibxssdm  6217  tfrlemibfn  6218  tfrlemibex  6219  tfrlemi14d  6223  tfrexlem  6224  tfr1onlem3  6228  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemres  6239  tfri1dALT  6241  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemres  6252  tfrcl  6254  rdgtfr  6264  rdgruledefgg  6265  rdgivallem  6271  rdgon  6276  rdg0g  6278  frec0g  6287  frecabex  6288  frecabcl  6289  frectfr  6290  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecrdg  6298  oafnex  6333  sucinc  6334  fnoa  6336  oaexg  6337  omfnex  6338  fnom  6339  omexg  6340  fnoei  6341  oeiexg  6342  oeiv  6345  oacl  6349  omcl  6350  oeicl  6351  oav2  6352  nnsucelsuc  6380  nnsucuniel  6384  ercnv  6443  iserd  6448  eqerlem  6453  eqer  6454  ecdmn0m  6464  erth  6466  qsss  6481  ecid  6485  ecidg  6486  qsid  6487  iinerm  6494  qsel  6499  erovlem  6514  ecopovsym  6518  ecopover  6520  th3qlem2  6525  mapprc  6539  fnmap  6542  fnpm  6543  mapdm0  6550  mapval2  6565  mapsn  6577  mapsncnv  6582  mapsnf1o2  6583  ixpconstg  6594  ixpprc  6606  ixpin  6610  ixpiinm  6611  ixpssmap2g  6614  ixpssmapg  6615  elixpsn  6622  ixpsnf1o  6623  bren  6634  brdomg  6635  domen  6638  domeng  6639  idssen  6664  ener  6666  domtr  6672  ensn1g  6684  en1  6686  en1bg  6687  fundmen  6693  fundmeng  6694  mapsnen  6698  fiprc  6702  unen  6703  xpsnen  6708  xpsneng  6709  xpcomco  6713  xpcomeng  6715  xpassen  6717  xpdom2  6718  xpdom2g  6719  xpf1o  6731  mapen  6733  mapxpen  6735  xpmapenlem  6736  ssenen  6738  phplem4  6742  phplem3g  6743  nneneq  6744  php5  6745  phpm  6752  findcard  6775  findcard2  6776  findcard2s  6777  isinfinf  6784  ac6sfi  6785  exmidpw  6795  unfidisj  6803  fiintim  6810  xpfi  6811  fisseneq  6813  ssfirab  6815  snexxph  6831  fidcenumlemr  6836  sbthlemi10  6847  isbth  6848  ssfii  6855  fi0  6856  fiss  6858  cnvinfex  6898  eqinfti  6900  infvalti  6902  infglbti  6905  infmoti  6908  ordiso2  6913  djuf1olem  6931  djuss  6948  ctm  6987  ctssdccl  6989  ctssdclemr  6990  finomni  7005  exmidomni  7007  fodjuomnilemdc  7009  pm54.43  7039  exmidfodomrlemim  7050  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  acfun  7056  ccfunen  7072  indpi  7143  dfplpq2  7155  enq0sym  7233  enq0ref  7234  enq0tr  7235  nqnq0pi  7239  nqnq0  7242  mulnnnq0  7251  nqprm  7343  nqprrnd  7344  nqprdisj  7345  nqprloc  7346  nqprl  7352  nqpru  7353  addnqprlemrl  7358  addnqprlemru  7359  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemrl  7374  mulnqprlemru  7375  mulnqprlemfl  7376  mulnqprlemfu  7377  ltnqpr  7394  ltnqpri  7395  archpr  7444  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlem2  7461  caucvgprlemladdfu  7478  caucvgprlem2  7481  caucvgprprlemopu  7500  suplocexprlemmu  7519  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  cnm  7633  ltresr  7640  peano1nnnn  7653  peano2nnnn  7654  axcnre  7682  axpre-apti  7686  renfdisj  7817  dfinfre  8707  1nn  8724  peano2nn  8725  indstr  9381  cnref1o  9433  ioof  9747  fzpr  9850  frec2uzrand  10171  frec2uzf1od  10172  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  frecfzennn  10192  ser3le  10284  hashinfom  10517  hashunlem  10543  hashun  10544  hashxp  10565  hashfacen  10572  zfz1isolem1  10576  zfz1iso  10577  shftfvalg  10583  ovshftex  10584  shftfibg  10585  shftfval  10586  shftfib  10588  shftfn  10589  2shfti  10596  shftvalg  10601  shftval4g  10602  maxabslemval  10973  fimaxre2  10991  xrmaxiflemval  11012  fclim  11056  climshft  11066  zsumdc  11146  fsum3  11149  fsum2dlemstep  11196  fsumcnv  11199  fisumcom2  11200  fisum0diag2  11209  fsumconst  11216  modfsummodlemstep  11219  fsumabs  11227  fsumrelem  11233  fsumiun  11239  ntrivcvgap  11310  algrf  11715  qredeu  11767  isprm2  11787  prmind2  11790  ennnfonelemex  11916  ennnfonelemrn  11921  exmidunben  11928  ctinfom  11930  ctinf  11932  qnnen  11933  enctlem  11934  ctiunctlemfo  11941  slotslfn  11974  restfn  12113  elrest  12116  bastg  12219  distop  12243  topnex  12244  epttop  12248  tgrest  12327  resttopon  12329  restco  12332  cnrest2  12394  cnptopresti  12396  cnptoprest  12397  cnptoprest2  12398  txuni2  12414  txbas  12416  eltx  12417  txcnp  12429  txcnmpt  12431  txrest  12434  txdis1cn  12436  txlm  12437  cnmpt1st  12446  cnmpt2nd  12447  txhmeo  12477  txswaphmeolem  12478  xmetec  12595  metrest  12664  reldvg  12806  dvfgg  12815  dvcj  12831  pilem3  12853  bdcvv  13044  bdsnss  13060  bdop  13062  bj-vprc  13083  bdinex1g  13088  bdssexg  13091  bj-inex  13094  bj-zfpair2  13097  bj-uniexg  13105  bdunexb  13107  bj-unexg  13108  bj-indint  13118  bj-ssom  13123  bj-om  13124  bj-2inf  13125  bj-bdfindis  13134  bj-nn0suc0  13137  bj-nnelirr  13140  bj-inf2vnlem1  13157  bj-inf2vnlem2  13158  bj-omex2  13164  bj-nn0sucALT  13165  bj-findis  13166  ss1oel2o  13178  nninfsellemeq  13199  exmidsbthrlem  13206