Theorem vex 2689

Description: All setvar variables are sets (see isset 2692). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	⊢ 𝑥 ∈ V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		equid 1677	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2688	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2250	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 145	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 1480  Vcvv 2686

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 2121

This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688

This theorem is referenced by:  elv  2690  elvd  2691  isset  2692  eqvisset  2696  ralv  2703  rexv  2704  reuv  2705  rmov  2706  rabab  2707  sbhypf  2735  ceqex  2812  ralab  2844  rexab  2846  mo2icl  2863  reu8  2880  csbvarg  3030  csbiebg  3042  sbcnestgf  3051  sbnfc2  3060  ddifnel  3207  ddifstab  3208  csbing  3283  unssdif  3311  unssin  3315  inssun  3316  invdif  3318  vn0  3373  vn0m  3374  eqv  3382  abvor0dc  3386  sbss  3471  velpw  3517  elpwg  3518  velsn  3544  vsnid  3557  exsnrex  3566  dftp2  3572  prmg  3644  prnzg  3647  snssg  3656  difprsnss  3658  sneqrg  3689  preq12bg  3700  pwprss  3732  pwtpss  3733  pwv  3735  unipr  3750  uniprg  3751  unisng  3753  elintg  3779  elintrabg  3784  intss1  3786  ssint  3787  intmin  3791  intss  3792  intssunim  3793  intmin4  3799  intab  3800  intun  3802  intpr  3803  intprg  3804  uniintsnr  3807  iinconstm  3822  iuniin  3823  iinss1  3825  dfiin2g  3846  dfiunv2  3849  ssiinf  3862  iinss  3864  iinss2  3865  0iin  3871  iinab  3874  iundif2ss  3878  iindif2m  3880  iinin2m  3881  iinuniss  3895  sspwuni  3897  pwpwab  3900  iinpw  3903  iunpwss  3904  brab1  3975  csbopabg  4006  mptv  4025  trint  4041  vnex  4059  inex1g  4064  ssexg  4067  inteximm  4074  inuni  4080  repizf2  4086  axpweq  4095  bnd2  4097  pwuni  4116  exmidundif  4129  exmidundifim  4130  zfpair2  4132  rext  4137  sspwb  4138  unipw  4139  ssextss  4142  euabex  4147  mss  4148  exss  4149  opth  4159  opthg  4160  copsexg  4166  copsex4g  4169  moop2  4173  euotd  4176  opabid  4179  elopab  4180  opelopabsbALT  4181  opelopabsb  4182  opabm  4202  pwin  4204  pwunss  4205  epelg  4212  epel  4214  pofun  4234  epse  4264  tron  4304  sucel  4332  suctr  4343  vuniex  4360  uniexg  4361  unexb  4363  snnex  4369  pwnex  4370  uniuni  4372  eusvnf  4374  eusvnfb  4375  iunpw  4401  unon  4427  ordunisuc2r  4430  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsucunielexmid  4446  elirr  4456  en2lp  4469  dtruex  4474  onintexmid  4487  reg3exmidlemwe  4493  dcextest  4495  finds  4514  finds2  4515  elnn  4519  limom  4527  0nelxp  4567  opelxp  4569  opeliunxp  4594  elvv  4601  elvvv  4602  elvvuni  4603  xpsspw  4651  relopabi  4665  opabid2  4670  difopab  4672  xpiindim  4676  raliunxp  4680  rexiunxp  4681  ralxpf  4685  rexxpf  4686  relop  4689  cnvco  4724  dfrn2  4727  dfdm4  4731  dmss  4738  dmin  4747  dmiun  4748  dmuni  4749  dm0  4753  dmi  4754  reldm0  4757  elreldm  4765  elrnmpt1  4790  dmrnssfld  4802  dmcoss  4808  dmcosseq  4810  opelresg  4826  resieq  4829  dmres  4840  elres  4855  relssres  4857  resopab  4863  resiexg  4864  iss  4865  dfres2  4871  dfima2  4883  imadmrn  4891  imai  4895  csbima12g  4900  elimasng  4907  args  4908  epini  4910  iniseg  4911  dfse2  4912  exse2  4913  cotr  4920  issref  4921  cnvsym  4922  intasym  4923  asymref  4924  intirr  4925  brcodir  4926  codir  4927  qfto  4928  poirr2  4931  cnvopab  4940  cnv0  4942  cnvi  4943  cnvdif  4945  rniun  4949  dminss  4953  imainss  4954  inimasn  4956  xpmlem  4959  dmxpss  4969  rnxpid  4973  ssrnres  4981  rninxp  4982  dminxp  4983  cnvcnv3  4988  dfrel2  4989  dmsnm  5004  dmsnopg  5010  cnvcnvsn  5015  dmsnsnsng  5016  cnvsng  5024  elxp4  5026  elxp5  5027  cnvresima  5028  dfco2  5038  dfco2a  5039  cores  5042  resco  5043  imaco  5044  rnco  5045  coiun  5048  co02  5052  coi1  5054  coass  5057  relssdmrn  5059  unielrel  5066  ressn  5079  cnviinm  5080  cnvpom  5081  cnvsom  5082  uniabio  5098  iotaval  5099  iotass  5105  sniota  5115  csbiotag  5116  dffun2  5133  dffun7  5150  dffun8  5151  dffun9  5152  funopg  5157  funssres  5165  funun  5167  funcnvsn  5168  funinsn  5172  funcnv2  5183  funcnv  5184  funcnv3  5185  funcnveq  5186  fun2cnv  5187  funcnvuni  5192  imadif  5203  funimaexglem  5206  isarep1  5209  2elresin  5234  fnres  5239  fcnvres  5306  fconstg  5319  fun11iun  5388  f1osng  5408  dffv3g  5417  fvssunirng  5436  sefvex  5442  fv3  5444  fvres  5445  nfunsn  5455  funimass4  5472  ssimaexg  5483  dmfco  5489  fvopab6  5517  fndmdif  5525  fvelrn  5551  dffo4  5568  f1ompt  5571  fmptco  5586  fsn  5592  fsng  5593  dfmpt  5597  dfmptg  5599  fnressn  5606  fressnfv  5607  fvsng  5616  resfunexg  5641  funfvima3  5651  idref  5658  abrexco  5660  imaiun  5661  dff13  5669  foeqcnvco  5691  f1eqcocnv  5692  fliftcnv  5696  isocnv2  5713  isoini  5719  isose  5722  riotav  5735  csbriotag  5742  acexmidlem2  5771  oprabid  5803  csbov123g  5809  0neqopab  5816  brabvv  5817  dfoprab2  5818  rnoprab  5854  eloprabga  5858  mpov  5861  f1opw  5977  opabex3d  6019  opabex3  6020  ofmres  6034  op1stg  6048  op2ndg  6049  1stval2  6053  2ndval2  6054  fo1st  6055  fo2nd  6056  f1stres  6057  f2ndres  6058  fo1stresm  6059  fo2ndresm  6060  xp1st  6063  xp2nd  6064  releldm2  6083  reldm  6084  sbcopeq1a  6085  csbopeq1a  6086  dfoprab3  6089  eloprabi  6094  mpomptsx  6095  dmmpossx  6097  fmpox  6098  mpofvex  6101  mpoexxg  6108  fmpoco  6113  df1st2  6116  df2nd2  6117  1stconst  6118  2ndconst  6119  dfmpo  6120  fo2ndf  6124  f1o2ndf1  6125  xporderlem  6128  cnvoprab  6131  f1od2  6132  brtpos2  6148  reldmtpos  6150  dmtpos  6153  rntpos  6154  ovtposg  6156  dftpos3  6159  dftpos4  6160  tpostpos  6161  tpossym  6173  tfrlem3  6208  tfrlem5  6211  tfrlem8  6215  tfrlemisucfn  6221  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemibex  6226  tfrlemi14d  6230  tfrexlem  6231  tfr1onlem3  6235  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  tfrcl  6261  rdgtfr  6271  rdgruledefgg  6272  rdgivallem  6278  rdgon  6283  rdg0g  6285  frec0g  6294  frecabex  6295  frecabcl  6296  frectfr  6297  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  oafnex  6340  sucinc  6341  fnoa  6343  oaexg  6344  omfnex  6345  fnom  6346  omexg  6347  fnoei  6348  oeiexg  6349  oeiv  6352  oacl  6356  omcl  6357  oeicl  6358  oav2  6359  nnsucelsuc  6387  nnsucuniel  6391  ercnv  6450  iserd  6455  eqerlem  6460  eqer  6461  ecdmn0m  6471  erth  6473  qsss  6488  ecid  6492  ecidg  6493  qsid  6494  iinerm  6501  qsel  6506  erovlem  6521  ecopovsym  6525  ecopover  6527  th3qlem2  6532  mapprc  6546  fnmap  6549  fnpm  6550  mapdm0  6557  mapval2  6572  mapsn  6584  mapsncnv  6589  mapsnf1o2  6590  ixpconstg  6601  ixpprc  6613  ixpin  6617  ixpiinm  6618  ixpssmap2g  6621  ixpssmapg  6622  elixpsn  6629  ixpsnf1o  6630  bren  6641  brdomg  6642  domen  6645  domeng  6646  idssen  6671  ener  6673  domtr  6679  ensn1g  6691  en1  6693  en1bg  6694  fundmen  6700  fundmeng  6701  mapsnen  6705  fiprc  6709  unen  6710  xpsnen  6715  xpsneng  6716  xpcomco  6720  xpcomeng  6722  xpassen  6724  xpdom2  6725  xpdom2g  6726  xpf1o  6738  mapen  6740  mapxpen  6742  xpmapenlem  6743  ssenen  6745  phplem4  6749  phplem3g  6750  nneneq  6751  php5  6752  phpm  6759  findcard  6782  findcard2  6783  findcard2s  6784  isinfinf  6791  ac6sfi  6792  exmidpw  6802  unfidisj  6810  fiintim  6817  xpfi  6818  fisseneq  6820  ssfirab  6822  snexxph  6838  fidcenumlemr  6843  sbthlemi10  6854  isbth  6855  ssfii  6862  fi0  6863  fiss  6865  cnvinfex  6905  eqinfti  6907  infvalti  6909  infglbti  6912  infmoti  6915  ordiso2  6920  djuf1olem  6938  djuss  6955  ctm  6994  ctssdccl  6996  ctssdclemr  6997  finomni  7012  exmidomni  7014  fodjuomnilemdc  7016  pm54.43  7046  exmidfodomrlemim  7057  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  ccfunen  7079  indpi  7150  dfplpq2  7162  enq0sym  7240  enq0ref  7241  enq0tr  7242  nqnq0pi  7246  nqnq0  7249  mulnnnq0  7258  nqprm  7350  nqprrnd  7351  nqprdisj  7352  nqprloc  7353  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  ltnqpr  7401  ltnqpri  7402  archpr  7451  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlem2  7468  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemopu  7507  suplocexprlemmu  7526  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  cnm  7640  ltresr  7647  peano1nnnn  7660  peano2nnnn  7661  axcnre  7689  axpre-apti  7693  renfdisj  7824  dfinfre  8714  1nn  8731  peano2nn  8732  indstr  9388  cnref1o  9440  ioof  9754  fzpr  9857  frec2uzrand  10178  frec2uzf1od  10179  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  frecfzennn  10199  ser3le  10291  hashinfom  10524  hashunlem  10550  hashun  10551  hashxp  10572  hashfacen  10579  zfz1isolem1  10583  zfz1iso  10584  shftfvalg  10590  ovshftex  10591  shftfibg  10592  shftfval  10593  shftfib  10595  shftfn  10596  2shfti  10603  shftvalg  10608  shftval4g  10609  maxabslemval  10980  fimaxre2  10998  xrmaxiflemval  11019  fclim  11063  climshft  11073  zsumdc  11153  fsum3  11156  fsum2dlemstep  11203  fsumcnv  11206  fisumcom2  11207  fisum0diag2  11216  fsumconst  11223  modfsummodlemstep  11226  fsumabs  11234  fsumrelem  11240  fsumiun  11246  ntrivcvgap  11317  algrf  11726  qredeu  11778  isprm2  11798  prmind2  11801  ennnfonelemex  11927  ennnfonelemrn  11932  exmidunben  11939  ctinfom  11941  ctinf  11943  qnnen  11944  enctlem  11945  ctiunctlemfo  11952  slotslfn  11985  restfn  12124  elrest  12127  bastg  12230  distop  12254  topnex  12255  epttop  12259  tgrest  12338  resttopon  12340  restco  12343  cnrest2  12405  cnptopresti  12407  cnptoprest  12408  cnptoprest2  12409  txuni2  12425  txbas  12427  eltx  12428  txcnp  12440  txcnmpt  12442  txrest  12445  txdis1cn  12447  txlm  12448  cnmpt1st  12457  cnmpt2nd  12458  txhmeo  12488  txswaphmeolem  12489  xmetec  12606  metrest  12675  reldvg  12817  dvfgg  12826  dvcj  12842  pilem3  12864  bdcvv  13055  bdsnss  13071  bdop  13073  bj-vprc  13094  bdinex1g  13099  bdssexg  13102  bj-inex  13105  bj-zfpair2  13108  bj-uniexg  13116  bdunexb  13118  bj-unexg  13119  bj-indint  13129  bj-ssom  13134  bj-om  13135  bj-2inf  13136  bj-bdfindis  13145  bj-nn0suc0  13148  bj-nnelirr  13151  bj-inf2vnlem1  13168  bj-inf2vnlem2  13169  bj-omex2  13175  bj-nn0sucALT  13176  bj-findis  13177  ss1oel2o  13189  nninfsellemeq  13210  exmidsbthrlem  13217