Theorem vex 2766

Description: All setvar variables are sets (see isset 2769). 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 1715	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2765	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2307	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 146	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2167  Vcvv 2763

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elv  2767  elvd  2768  isset  2769  eqvisset  2773  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rabab  2784  sbhypf  2813  ceqex  2891  ralab  2924  rexab  2926  mo2icl  2943  reu8  2960  csbvarg  3112  csbiebg  3127  sbcnestgf  3136  sbnfc2  3145  ddifnel  3295  ddifstab  3296  csbing  3371  unssdif  3399  unssin  3403  inssun  3404  invdif  3406  vn0  3462  vn0m  3463  eqv  3471  abvor0dc  3475  sbss  3559  velpw  3613  elpwg  3614  velsn  3640  vsnid  3655  exsnrex  3665  dftp2  3672  prmg  3744  prnzg  3747  snssgOLD  3759  difprsnss  3761  sneqrg  3793  preq12bg  3804  pwprss  3836  pwtpss  3837  pwv  3839  unipr  3854  uniprg  3855  unisng  3857  elintg  3883  elintrabg  3888  intss1  3890  ssint  3891  intmin  3895  intss  3896  intssunim  3897  intmin4  3903  intab  3904  intun  3906  intpr  3907  intprg  3908  uniintsnr  3911  iinconstm  3926  iuniin  3927  iinss1  3929  dfiin2g  3950  dfiunv2  3953  ssiinf  3967  iinss  3969  iinss2  3970  0iin  3976  iinab  3979  iundif2ss  3983  iindif2m  3985  iinin2m  3986  iinuniss  4000  sspwuni  4002  pwpwab  4005  iinpw  4008  iunpwss  4009  brab1  4081  csbopabg  4112  mptv  4131  trint  4147  vnex  4165  inex1g  4170  ssexg  4173  inteximm  4183  inuni  4189  repizf2  4196  axpweq  4205  bnd2  4207  pwuni  4226  exmidundif  4240  exmidundifim  4241  zfpair2  4244  rext  4249  sspwb  4250  unipw  4251  ssextss  4254  euabex  4259  mss  4260  exss  4261  opth  4271  opthg  4272  copsexg  4278  copsex4g  4281  moop2  4285  euotd  4288  opabid  4291  elopab  4293  opelopabsbALT  4294  opelopabsb  4295  opabm  4316  pwin  4318  pwunss  4319  epelg  4326  epel  4328  pofun  4348  epse  4378  tron  4418  sucel  4446  suctr  4457  vuniex  4474  uniexg  4475  unexb  4478  snnex  4484  pwnex  4485  uniuni  4487  eusvnf  4489  eusvnfb  4490  iunpw  4516  unon  4548  ordunisuc2r  4551  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsucunielexmid  4568  elirr  4578  en2lp  4591  dtruex  4596  onintexmid  4610  reg3exmidlemwe  4616  dcextest  4618  finds  4637  finds2  4638  elomssom  4642  limom  4651  0nelxp  4692  opelxp  4694  opeliunxp  4719  elvv  4726  elvvv  4727  elvvuni  4728  xpsspw  4776  relopabiv  4790  relopabi  4792  opabid2  4798  difopab  4800  xpiindim  4804  raliunxp  4808  rexiunxp  4809  ralxpf  4813  rexxpf  4814  relop  4817  cnvco  4852  dfrn2  4855  dfdm4  4859  dmss  4866  dmin  4875  dmiun  4876  dmuni  4877  dm0  4881  dmi  4882  reldm0  4885  elreldm  4893  elrnmpt1  4918  dmrnssfld  4930  dmcoss  4936  dmcosseq  4938  opelresg  4954  resieq  4957  dmres  4968  elres  4983  relssres  4985  resopab  4991  resiexg  4992  iss  4993  dfres2  4999  restidsing  5003  dfima2  5012  imadmrn  5020  imai  5026  csbima12g  5031  elimasng  5038  args  5039  epini  5041  iniseg  5042  dfse2  5043  exse2  5044  cotr  5052  issref  5053  cnvsym  5054  intasym  5055  asymref  5056  intirr  5057  brcodir  5058  codir  5059  qfto  5060  poirr2  5063  cnvopab  5072  cnv0  5074  cnvi  5075  cnvdif  5077  rniun  5081  dminss  5085  imainss  5086  inimasn  5088  xpmlem  5091  dmxpss  5101  rnxpid  5105  ssrnres  5113  rninxp  5114  dminxp  5115  cnvcnv3  5120  dfrel2  5121  dmsnm  5136  dmsnopg  5142  cnvcnvsn  5147  dmsnsnsng  5148  cnvsng  5156  elxp4  5158  elxp5  5159  cnvresima  5160  dfco2  5170  dfco2a  5171  cores  5174  resco  5175  imaco  5176  rnco  5177  coiun  5180  co02  5184  coi1  5186  coass  5189  relssdmrn  5191  unielrel  5198  ressn  5211  cnviinm  5212  cnvpom  5213  cnvsom  5214  uniabio  5230  iotaval  5231  iotass  5237  sniota  5250  csbiotag  5252  dffun2  5269  dffun7  5286  dffun8  5287  dffun9  5288  funopg  5293  funssres  5301  funun  5303  funcnvsn  5304  funinsn  5308  funcnv2  5319  funcnv  5320  funcnv3  5321  funcnveq  5322  fun2cnv  5323  funcnvuni  5328  imadif  5339  funimaexglem  5342  isarep1  5345  2elresin  5372  fnres  5377  fcnvres  5444  fconstg  5457  fun11iun  5528  f1osng  5548  dffv3g  5557  fvssunirng  5576  sefvex  5582  fv3  5584  fvres  5585  nfunsn  5596  funimass4  5614  ssimaexg  5626  dmfco  5632  fvopab6  5661  fndmdif  5670  fvelrn  5696  dffo4  5713  f1ompt  5716  fmptco  5731  fsn  5737  fsng  5738  dfmpt  5742  dfmptg  5744  fnressn  5751  fressnfv  5752  fvsng  5761  resfunexg  5786  funfvima3  5799  idref  5806  abrexco  5809  imaiun  5810  dff13  5818  foeqcnvco  5840  f1eqcocnv  5841  fliftcnv  5845  isocnv2  5862  isoini  5868  isose  5871  riotav  5886  csbriotag  5893  acexmidlem2  5922  oprabid  5957  csbov123g  5964  0neqopab  5971  brabvv  5972  dfoprab2  5973  rnoprab  6009  eloprabga  6013  mpov  6016  f1opw  6134  opabex3d  6187  opabex3  6188  ofmres  6202  uchoice  6204  op1stg  6217  op2ndg  6218  1stval2  6222  2ndval2  6223  fo1st  6224  fo2nd  6225  f1stres  6226  f2ndres  6227  fo1stresm  6228  fo2ndresm  6229  xp1st  6232  xp2nd  6233  releldm2  6252  reldm  6253  sbcopeq1a  6254  csbopeq1a  6255  dfoprab3  6258  eloprabi  6263  mpomptsx  6264  dmmpossx  6266  fmpox  6267  mpofvex  6272  mpoexxg  6277  fmpoco  6283  df1st2  6286  df2nd2  6287  1stconst  6288  2ndconst  6289  dfmpo  6290  fo2ndf  6294  f1o2ndf1  6295  xporderlem  6298  cnvoprab  6301  f1od2  6302  brtpos2  6318  reldmtpos  6320  dmtpos  6323  rntpos  6324  ovtposg  6326  dftpos3  6329  dftpos4  6330  tpostpos  6331  tpossym  6343  tfrlem3  6378  tfrlem5  6381  tfrlem8  6385  tfrlemisucfn  6391  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemibex  6396  tfrlemi14d  6400  tfrexlem  6401  tfr1onlem3  6405  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemres  6429  tfrcl  6431  rdgtfr  6441  rdgruledefgg  6442  rdgivallem  6448  rdgon  6453  rdg0g  6455  frec0g  6464  frecabex  6465  frecabcl  6466  frectfr  6467  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  oafnex  6511  sucinc  6512  fnoa  6514  oaexg  6515  omfnex  6516  fnom  6517  omexg  6518  fnoei  6519  oeiexg  6520  oeiv  6523  oacl  6527  omcl  6528  oeicl  6529  oav2  6530  nnsucelsuc  6558  nnsucuniel  6562  ercnv  6622  iserd  6627  eqerlem  6632  eqer  6633  ecdmn0m  6645  erth  6647  qsss  6662  ecid  6666  ecidg  6667  qsid  6668  iinerm  6675  qsel  6680  erovlem  6695  ecopovsym  6699  ecopover  6701  th3qlem2  6706  mapprc  6720  fnmap  6723  fnpm  6724  mapdm0  6731  mapval2  6746  mapsn  6758  mapsncnv  6763  mapsnf1o2  6764  ixpconstg  6775  ixpprc  6787  ixpin  6791  ixpiinm  6792  ixpssmap2g  6795  ixpssmapg  6796  elixpsn  6803  ixpsnf1o  6804  bren  6815  brdomg  6816  domen  6819  domeng  6820  idssen  6845  ener  6847  domtr  6853  ensn1g  6865  en1  6867  en1bg  6868  fundmen  6874  fundmeng  6875  mapsnen  6879  fiprc  6883  unen  6884  xpsnen  6889  xpsneng  6890  xpcomco  6894  xpcomeng  6896  xpassen  6898  xpdom2  6899  xpdom2g  6900  pw2f1odc  6905  xpf1o  6914  mapen  6916  mapxpen  6918  xpmapenlem  6919  ssenen  6921  phplem4  6925  phplem3g  6926  nneneq  6927  php5  6928  phpm  6935  findcard  6958  findcard2  6959  findcard2s  6960  isinfinf  6967  ac6sfi  6968  exmidpw  6978  exmidpweq  6979  exmidpw2en  6982  unfidisj  6992  fiintim  7001  xpfi  7002  fisseneq  7004  ssfirab  7006  snexxph  7025  fidcenumlemr  7030  sbthlemi10  7041  isbth  7042  ssfii  7049  fi0  7050  fiss  7052  cnvinfex  7093  eqinfti  7095  infvalti  7097  infglbti  7100  infmoti  7103  ordiso2  7110  djuf1olem  7128  djuss  7145  ctm  7184  ctssdccl  7186  ctssdclemr  7187  finomni  7215  exmidomni  7217  fodjuomnilemdc  7219  nninfwlpoimlemginf  7251  pm54.43  7271  exmidfodomrlemim  7282  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  finacn  7289  acfun  7292  ccfunen  7349  cc2lem  7351  cc3  7353  acnccim  7357  indpi  7428  dfplpq2  7440  enq0sym  7518  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  nqnq0  7527  mulnnnq0  7536  nqprm  7628  nqprrnd  7629  nqprdisj  7630  nqprloc  7631  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  ltnqpr  7679  ltnqpri  7680  archpr  7729  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlem2  7746  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemopu  7785  suplocexprlemmu  7804  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  cnm  7918  ltresr  7925  peano1nnnn  7938  peano2nnnn  7939  axcnre  7967  axpre-apti  7971  renfdisj  8105  dfinfre  9002  1nn  9020  peano2nn  9021  indstr  9686  cnref1o  9744  ioof  10065  fzpr  10171  frec2uzrand  10516  frec2uzf1od  10517  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  frecfzennn  10537  seqp1g  10577  seqclg  10583  seqf1og  10632  seqfeq4g  10642  ser3le  10648  hashinfom  10889  hashunlem  10915  hashun  10916  hashxp  10937  hashfacen  10947  zfz1isolem1  10951  zfz1iso  10952  wrdexb  10966  shftfvalg  11002  ovshftex  11003  shftfibg  11004  shftfval  11005  shftfib  11007  shftfn  11008  2shfti  11015  shftvalg  11020  shftval4g  11021  maxabslemval  11392  fimaxre2  11411  xrmaxiflemval  11434  fclim  11478  climshft  11488  zsumdc  11568  fsum3  11571  fsum2dlemstep  11618  fsumcnv  11621  fisumcom2  11622  fisum0diag2  11631  fsumconst  11638  modfsummodlemstep  11641  fsumabs  11649  fsumrelem  11655  fsumiun  11661  ntrivcvgap  11732  fprod2dlemstep  11806  fprodcnv  11809  fprodcom2fi  11810  fprodmodd  11825  nninfct  12235  algrf  12240  qredeu  12292  isprm2  12312  prmind2  12315  4sqlemafi  12591  4sqlem12  12598  ennnfonelemex  12658  ennnfonelemrn  12663  exmidunben  12670  ctinfom  12672  ctinf  12674  qnnen  12675  enctlem  12676  ctiunctlemfo  12683  slotslfn  12731  setscomd  12746  restfn  12947  elrest  12950  ptex  12968  prdsex  12973  prdsvallem  12976  prdsval  12977  prdsbaslemss  12978  prdsbas  12980  imasex  13009  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfnlemg  13018  fnpr2ob  13044  ismgm  13061  plusffng  13069  fn0g  13079  fngsum  13092  gsumsplit1r  13102  gsumprval  13103  issgrp  13107  ismnddef  13122  gsumfzz  13199  gsumfzcl  13203  mulgnngsum  13335  subgintm  13406  releqgg  13428  eqgex  13429  eqgfval  13430  eqgval  13431  isghm  13451  fnmgp  13556  isrng  13568  isring  13634  ringn0  13694  opprrngbg  13712  opprsubgg  13718  opprunitd  13744  dfrhm2  13788  rhmex  13791  opprsubrngg  13845  subrngintm  13846  subrngpropd  13850  subrgpropd  13887  isdomn  13903  opprdomnbg  13908  scaffng  13943  rmodislmodlem  13984  rmodislmod  13985  lssex  13988  lsssn0  14004  lss1d  14017  lssintclm  14018  ellspsn  14051  rlmfn  14087  isridl  14138  blfn  14185  mopnset  14186  metuex  14189  znval  14270  znleval  14287  psrval  14298  fnpsr  14299  bastg  14383  distop  14407  topnex  14408  epttop  14412  tgrest  14491  resttopon  14493  restco  14496  cnrest2  14558  cnptopresti  14560  cnptoprest  14561  cnptoprest2  14562  txuni2  14578  txbas  14580  eltx  14581  txcnp  14593  txcnmpt  14595  txrest  14598  txdis1cn  14600  txlm  14601  cnmpt1st  14610  cnmpt2nd  14611  txhmeo  14641  txswaphmeolem  14642  xmetec  14759  metrest  14828  reldvg  15001  dvfgg  15010  dvcj  15031  dvmptfsum  15047  elply2  15057  pilem3  15105  lgsquadlem1  15404  lgsquadlem2  15405  bdcvv  15589  bdsnss  15605  bdop  15607  bj-vprc  15628  bdinex1g  15633  bdssexg  15636  bj-inex  15639  bj-zfpair2  15642  bj-uniexg  15650  bdunexb  15652  bj-unexg  15653  bj-indint  15663  bj-ssom  15668  bj-om  15669  bj-2inf  15670  bj-bdfindis  15679  bj-nn0suc0  15682  bj-nnelirr  15685  bj-inf2vnlem1  15702  bj-inf2vnlem2  15703  bj-omex2  15709  bj-nn0sucALT  15710  bj-findis  15711  ss1oel2o  15724  domomsubct  15734  pw1nct  15736  nninfsellemeq  15747  exmidsbthrlem  15757