Theorem vex 2802

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

Syntax hints:   ∈ wcel 2200  Vcvv 2799

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2801

This theorem is referenced by:  elv  2803  elvd  2804  el2v  2805  isset  2806  eqvisset  2810  ralv  2817  rexv  2818  reuv  2819  rmov  2820  rabab  2821  sbhypf  2850  ceqex  2930  ralab  2963  rexab  2965  mo2icl  2982  reu8  2999  csbvarg  3152  csbiebg  3167  sbcnestgf  3176  sbnfc2  3185  ddifnel  3335  ddifstab  3336  csbing  3411  unssdif  3439  unssin  3443  inssun  3444  invdif  3446  vn0  3502  vn0m  3503  eqv  3511  abvor0dc  3515  sbss  3599  velpw  3656  elpwg  3657  velsn  3683  vsnid  3698  exsnrex  3708  dftp2  3715  prmg  3789  prnzg  3792  snssgOLD  3804  difprsnss  3806  sneqrg  3840  preq12bg  3851  pwprss  3884  pwtpss  3885  pwv  3887  unipr  3902  uniprg  3903  unisng  3905  elintg  3931  elintrabg  3936  intss1  3938  ssint  3939  intmin  3943  intss  3944  intssunim  3945  intmin4  3951  intab  3952  intun  3954  intpr  3955  intprg  3956  uniintsnr  3959  iinconstm  3974  iuniin  3975  iinss1  3977  dfiin2g  3998  dfiunv2  4001  ssiinf  4015  iinss  4017  iinss2  4018  0iin  4024  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iinuniss  4048  sspwuni  4050  pwpwab  4053  iinpw  4056  iunpwss  4057  brab1  4131  csbopabg  4162  mptv  4181  trint  4197  vnex  4215  inex1g  4220  ssexg  4223  inteximm  4233  inuni  4239  repizf2  4246  axpweq  4255  bnd2  4257  pwuni  4276  exmidundif  4290  exmidundifim  4291  zfpair2  4294  rext  4301  sspwb  4302  unipw  4303  ssextss  4306  euabex  4311  mss  4312  exss  4313  opth  4323  opthg  4324  copsexg  4330  copsex4g  4333  moop2  4338  euotd  4341  opabid  4344  elopab  4346  opelopabsbALT  4347  opelopabsb  4348  opabm  4369  pwin  4373  pwunss  4374  epelg  4381  epel  4383  pofun  4403  epse  4433  tron  4473  sucel  4501  suctr  4512  vuniex  4529  uniexg  4530  unexb  4533  snnex  4539  pwnex  4540  uniuni  4542  eusvnf  4544  eusvnfb  4545  iunpw  4571  unon  4603  ordunisuc2r  4606  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsucunielexmid  4623  elirr  4633  en2lp  4646  dtruex  4651  onintexmid  4665  reg3exmidlemwe  4671  dcextest  4673  finds  4692  finds2  4693  elomssom  4697  limom  4706  0nelxp  4747  opelxp  4749  opeliunxp  4774  elvv  4781  elvvv  4782  elvvuni  4783  xpsspw  4831  relopabiv  4845  relopabi  4847  opabid2  4853  difopab  4855  xpiindim  4859  raliunxp  4863  rexiunxp  4864  ralxpf  4868  rexxpf  4869  relop  4872  cnvco  4907  dfrn2  4910  dfdm4  4915  dmss  4922  dmin  4931  dmiun  4932  dmuni  4933  dm0  4937  dmi  4938  reldm0  4941  reldmm  4942  elreldm  4950  elrnmpt1  4975  dmrnssfld  4987  dmcoss  4994  dmcosseq  4996  opelresg  5012  resieq  5015  dmres  5026  elres  5041  relssres  5043  resopab  5049  resiexg  5050  iss  5051  dfres2  5057  restidsing  5061  dfima2  5070  imadmrn  5078  imai  5084  csbima12g  5089  elimasng  5096  args  5097  epini  5099  iniseg  5100  dfse2  5101  exse2  5102  cotr  5110  issref  5111  cnvsym  5112  intasym  5113  asymref  5114  intirr  5115  brcodir  5116  codir  5117  qfto  5118  poirr2  5121  cnvopab  5130  cnv0  5132  cnvi  5133  cnvdif  5135  rniun  5139  dminss  5143  imainss  5144  inimasn  5146  xpmlem  5149  dmxpss  5159  rnxpid  5163  ssrnres  5171  rninxp  5172  dminxp  5173  cnvcnv3  5178  dfrel2  5179  dmsnm  5194  dmsnopg  5200  cnvcnvsn  5205  dmsnsnsng  5206  cnvsng  5214  elxp4  5216  elxp5  5217  cnvresima  5218  dfco2  5228  dfco2a  5229  cores  5232  resco  5233  imaco  5234  rnco  5235  coiun  5238  co02  5242  coi1  5244  coass  5247  relssdmrn  5249  unielrel  5256  ressn  5269  cnviinm  5270  cnvpom  5271  cnvsom  5272  uniabio  5289  iotaval  5290  iotass  5296  sniota  5309  csbiotag  5311  dffun2  5328  dffun7  5345  dffun8  5346  dffun9  5347  funopg  5352  funssres  5360  funun  5362  funcnvsn  5366  funinsn  5370  funcnv2  5381  funcnv  5382  funcnv3  5383  funcnveq  5384  fun2cnv  5385  funcnvuni  5390  imadif  5401  funimaexglem  5404  isarep1  5407  2elresin  5434  fnres  5440  fcnvres  5511  fconstg  5524  fun11iun  5595  f1osng  5616  dffv3g  5625  fvssunirng  5644  sefvex  5650  fv3  5652  fvres  5653  nfunsn  5666  funimass4  5686  ssimaexg  5698  dmfco  5704  fvopab6  5733  fndmdif  5742  fvelrn  5768  dffo4  5785  f1ompt  5788  fmptco  5803  fsn  5809  fsng  5810  dfmpt  5814  dfmptg  5816  funopsn  5819  funop  5820  funopdmsn  5823  fnressn  5829  fressnfv  5830  fvsng  5839  resfunexg  5864  funfvima3  5877  idref  5886  abrexco  5889  imaiun  5890  dff13  5898  foeqcnvco  5920  f1eqcocnv  5921  fliftcnv  5925  isocnv2  5942  isoini  5948  isose  5951  riotav  5966  csbriotag  5974  acexmidlem2  6004  oprabid  6039  csbov123g  6046  0neqopab  6055  brabvv  6056  dfoprab2  6057  rnoprab  6093  eloprabga  6097  mpov  6100  f1opw  6219  opabex3d  6272  opabex3  6273  ofmres  6287  uchoice  6289  op1stg  6302  op2ndg  6303  1stval2  6307  2ndval2  6308  fo1st  6309  fo2nd  6310  f1stres  6311  f2ndres  6312  fo1stresm  6313  fo2ndresm  6314  xp1st  6317  xp2nd  6318  releldm2  6337  reldm  6338  sbcopeq1a  6339  csbopeq1a  6340  dfoprab3  6343  eloprabi  6348  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  mpoexxg  6362  fmpoco  6368  df1st2  6371  df2nd2  6372  1stconst  6373  2ndconst  6374  dfmpo  6375  fo2ndf  6379  f1o2ndf1  6380  xporderlem  6383  cnvoprab  6386  f1od2  6387  brtpos2  6403  reldmtpos  6405  dmtpos  6408  rntpos  6409  ovtposg  6411  dftpos3  6414  dftpos4  6415  tpostpos  6416  tpossym  6428  tfrlem3  6463  tfrlem5  6466  tfrlem8  6470  tfrlemisucfn  6476  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemibex  6481  tfrlemi14d  6485  tfrexlem  6486  tfr1onlem3  6490  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  tfrcl  6516  rdgtfr  6526  rdgruledefgg  6527  rdgivallem  6533  rdgon  6538  rdg0g  6540  frec0g  6549  frecabex  6550  frecabcl  6551  frectfr  6552  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  oafnex  6598  sucinc  6599  fnoa  6601  oaexg  6602  omfnex  6603  fnom  6604  omexg  6605  fnoei  6606  oeiexg  6607  oeiv  6610  oacl  6614  omcl  6615  oeicl  6616  oav2  6617  nnsucelsuc  6645  nnsucuniel  6649  ercnv  6709  iserd  6714  eqerlem  6719  eqer  6720  ecdmn0m  6732  erth  6734  qsss  6749  ecid  6753  ecidg  6754  qsid  6755  iinerm  6762  qsel  6767  erovlem  6782  ecopovsym  6786  ecopover  6788  th3qlem2  6793  mapprc  6807  fnmap  6810  fnpm  6811  mapdm0  6818  mapval2  6833  mapsn  6845  mapsncnv  6850  mapsnf1o2  6851  ixpconstg  6862  ixpprc  6874  ixpin  6878  ixpiinm  6879  ixpssmap2g  6882  ixpssmapg  6883  elixpsn  6890  ixpsnf1o  6891  bren  6903  brdomg  6905  domen  6908  domeng  6909  idssen  6936  domssr  6937  ener  6939  domtr  6945  ensn1g  6957  en1  6959  en1bg  6960  fundmen  6967  fundmeng  6968  mapsnen  6972  fiprc  6976  unen  6977  rex2dom  6979  en2m  6982  dom1o  6985  xpsnen  6988  xpsneng  6989  xpcomco  6993  xpcomeng  6995  xpassen  6997  xpdom2  6998  xpdom2g  6999  pw2f1odc  7004  xpf1o  7013  mapen  7015  mapxpen  7017  xpmapenlem  7018  ssenen  7020  phplem4  7024  phplem3g  7025  nneneq  7026  php5  7027  phpm  7035  findcard  7058  findcard2  7059  findcard2s  7060  isinfinf  7067  ac6sfi  7068  exmidpw  7078  exmidpweq  7079  exmidpw2en  7082  unfidisj  7092  fiintim  7101  xpfi  7102  fisseneq  7104  ssfirab  7106  snexxph  7125  fidcenumlemr  7130  sbthlemi10  7141  isbth  7142  ssfii  7149  fi0  7150  fiss  7152  cnvinfex  7193  eqinfti  7195  infvalti  7197  infglbti  7200  infmoti  7203  ordiso2  7210  djuf1olem  7228  djuss  7245  ctm  7284  ctssdccl  7286  ctssdclemr  7287  finomni  7315  exmidomni  7317  fodjuomnilemdc  7319  nninfwlpoimlemginf  7351  pm54.43  7371  pr2cv1  7376  exmidfodomrlemim  7387  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  finacn  7394  acfun  7397  ccfunen  7458  cc2lem  7460  cc3  7462  acnccim  7466  indpi  7537  dfplpq2  7549  enq0sym  7627  enq0ref  7628  enq0tr  7629  nqnq0pi  7633  nqnq0  7636  mulnnnq0  7645  nqprm  7737  nqprrnd  7738  nqprdisj  7739  nqprloc  7740  nqprl  7746  nqpru  7747  addnqprlemrl  7752  addnqprlemru  7753  addnqprlemfl  7754  addnqprlemfu  7755  mulnqprlemrl  7768  mulnqprlemru  7769  mulnqprlemfl  7770  mulnqprlemfu  7771  ltnqpr  7788  ltnqpri  7789  archpr  7838  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlem2  7855  caucvgprlemladdfu  7872  caucvgprlem2  7875  caucvgprprlemopu  7894  suplocexprlemmu  7913  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  cnm  8027  ltresr  8034  peano1nnnn  8047  peano2nnnn  8048  axcnre  8076  axpre-apti  8080  renfdisj  8214  dfinfre  9111  1nn  9129  peano2nn  9130  indstr  9796  cnref1o  9854  ioof  10175  fzpr  10281  frec2uzrand  10635  frec2uzf1od  10636  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  frecfzennn  10656  seqp1g  10696  seqclg  10702  seqf1og  10751  seqfeq4g  10761  ser3le  10767  hashinfom  11008  hashunlem  11034  hashun  11035  hashxp  11056  hashfacen  11066  zfz1isolem1  11070  zfz1iso  11071  fundm2domnop0  11075  wrdexb  11091  fnpfx  11217  cats1un  11261  wrdind  11262  wrd2ind  11263  shftfvalg  11337  ovshftex  11338  shftfibg  11339  shftfval  11340  shftfib  11342  shftfn  11343  2shfti  11350  shftvalg  11355  shftval4g  11356  maxabslemval  11727  fimaxre2  11746  xrmaxiflemval  11769  fclim  11813  climshft  11823  zsumdc  11903  fsum3  11906  fsum2dlemstep  11953  fsumcnv  11956  fisumcom2  11957  fisum0diag2  11966  fsumconst  11973  modfsummodlemstep  11976  fsumabs  11984  fsumrelem  11990  fsumiun  11996  ntrivcvgap  12067  fprod2dlemstep  12141  fprodcnv  12144  fprodcom2fi  12145  fprodmodd  12160  nninfct  12570  algrf  12575  qredeu  12627  isprm2  12647  prmind2  12650  4sqlemafi  12926  4sqlem12  12933  ennnfonelemex  12993  ennnfonelemrn  12998  exmidunben  13005  ctinfom  13007  ctinf  13009  qnnen  13010  enctlem  13011  ctiunctlemfo  13018  slotslfn  13066  setscomd  13081  restfn  13284  elrest  13287  ptex  13305  prdsex  13310  prdsvallem  13313  prdsval  13314  prdsbaslemss  13315  prdsbas  13317  imasex  13346  imasival  13347  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfnlemg  13355  fnpr2ob  13381  ismgm  13398  plusffng  13406  fn0g  13416  fngsum  13429  gsumsplit1r  13439  gsumprval  13440  issgrp  13444  ismnddef  13459  gsumfzz  13536  gsumfzcl  13540  mulgnngsum  13672  subgintm  13743  releqgg  13765  eqgex  13766  eqgfval  13767  eqgval  13768  isghm  13788  fnmgp  13893  isrng  13905  isring  13971  ringn0  14031  opprrngbg  14049  opprsubgg  14055  opprunitd  14082  dfrhm2  14126  rhmex  14129  opprsubrngg  14183  subrngintm  14184  subrngpropd  14188  subrgpropd  14225  isdomn  14241  opprdomnbg  14246  scaffng  14281  rmodislmodlem  14322  rmodislmod  14323  lssex  14326  lsssn0  14342  lss1d  14355  lssintclm  14356  ellspsn  14389  rlmfn  14425  isridl  14476  blfn  14523  mopnset  14524  metuex  14527  znval  14608  znleval  14625  psrval  14638  fnpsr  14639  mplvalcoe  14662  fnmpl  14665  bastg  14743  distop  14767  topnex  14768  epttop  14772  tgrest  14851  resttopon  14853  restco  14856  cnrest2  14918  cnptopresti  14920  cnptoprest  14921  cnptoprest2  14922  txuni2  14938  txbas  14940  eltx  14941  txcnp  14953  txcnmpt  14955  txrest  14958  txdis1cn  14960  txlm  14961  cnmpt1st  14970  cnmpt2nd  14971  txhmeo  15001  txswaphmeolem  15002  xmetec  15119  metrest  15188  reldvg  15361  dvfgg  15370  dvcj  15391  dvmptfsum  15407  elply2  15417  pilem3  15465  lgsquadlem1  15764  lgsquadlem2  15765  upgrex  15911  umgredg  15951  umgredgnlp  15958  usgredgreu  16022  uspgredg2vtxeu  16024  ushgredgedg  16032  ushgredgedgloop  16034  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlk1walkdom  16080  bdcvv  16244  bdsnss  16260  bdop  16262  bj-vprc  16283  bdinex1g  16288  bdssexg  16291  bj-inex  16294  bj-zfpair2  16297  bj-uniexg  16305  bdunexb  16307  bj-unexg  16308  bj-indint  16318  bj-ssom  16323  bj-om  16324  bj-2inf  16325  bj-bdfindis  16334  bj-nn0suc0  16337  bj-nnelirr  16340  bj-inf2vnlem1  16357  bj-inf2vnlem2  16358  bj-omex2  16364  bj-nn0sucALT  16365  bj-findis  16366  ss1oel2o  16380  domomsubct  16396  pw1nct  16398  nninfsellemeq  16410  exmidsbthrlem  16420