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  4234  inuni  4240  repizf2  4247  axpweq  4256  bnd2  4258  pwuni  4277  exmidundif  4291  exmidundifim  4292  zfpair2  4295  rext  4302  sspwb  4303  unipw  4304  ssextss  4307  euabex  4312  mss  4313  exss  4314  opth  4324  opthg  4325  copsexg  4331  copsex4g  4334  moop2  4339  euotd  4342  opabid  4345  elopab  4347  opelopabsbALT  4348  opelopabsb  4349  opabm  4370  pwin  4374  pwunss  4375  epelg  4382  epel  4384  pofun  4404  epse  4434  tron  4474  sucel  4502  suctr  4513  vuniex  4530  uniexg  4531  unexb  4534  snnex  4540  pwnex  4541  uniuni  4543  eusvnf  4545  eusvnfb  4546  iunpw  4572  unon  4604  ordunisuc2r  4607  ordtri2or2exmidlem  4619  onsucelsucexmidlem  4622  ordsucunielexmid  4624  elirr  4634  en2lp  4647  dtruex  4652  onintexmid  4666  reg3exmidlemwe  4672  dcextest  4674  finds  4693  finds2  4694  elomssom  4698  limom  4707  0nelxp  4748  opelxp  4750  opeliunxp  4776  elvv  4783  elvvv  4784  elvvuni  4785  xpsspw  4833  relopabiv  4848  relopabi  4850  opabid2  4856  difopab  4858  xpiindim  4862  raliunxp  4866  rexiunxp  4867  ralxpf  4871  rexxpf  4872  relop  4875  cnvco  4910  dfrn2  4913  dfdm4  4918  dmss  4925  dmin  4934  dmiun  4935  dmuni  4936  dm0  4940  dmi  4941  reldm0  4944  reldmm  4945  elreldm  4953  elrnmpt1  4978  dmrnssfld  4990  dmcoss  4997  dmcosseq  4999  opelresg  5015  resieq  5018  dmres  5029  elres  5044  relssres  5046  resopab  5052  resiexg  5053  iss  5054  dfres2  5060  restidsing  5064  dfima2  5073  imadmrn  5081  imai  5087  csbima12g  5092  elimasng  5099  args  5100  epini  5102  iniseg  5103  dfse2  5104  exse2  5105  cotr  5113  issref  5114  cnvsym  5115  intasym  5116  asymref  5117  intirr  5118  brcodir  5119  codir  5120  qfto  5121  poirr2  5124  cnvopab  5133  cnv0  5135  cnvi  5136  cnvdif  5138  rniun  5142  dminss  5146  imainss  5147  inimasn  5149  xpmlem  5152  dmxpss  5162  rnxpid  5166  ssrnres  5174  rninxp  5175  dminxp  5176  cnvcnv3  5181  dfrel2  5182  dmsnm  5197  dmsnopg  5203  cnvcnvsn  5208  dmsnsnsng  5209  cnvsng  5217  elxp4  5219  elxp5  5220  cnvresima  5221  dfco2  5231  dfco2a  5232  cores  5235  resco  5236  imaco  5237  rnco  5238  coiun  5241  co02  5245  coi1  5247  coass  5250  relssdmrn  5252  unielrel  5259  ressn  5272  cnviinm  5273  cnvpom  5274  cnvsom  5275  uniabio  5292  iotaval  5293  iotass  5299  sniota  5312  csbiotag  5314  dffun2  5331  dffun7  5348  dffun8  5349  dffun9  5350  funopg  5355  funssres  5363  funun  5365  funcnvsn  5369  funinsn  5373  funcnv2  5384  funcnv  5385  funcnv3  5386  funcnveq  5387  fun2cnv  5388  funcnvuni  5393  imadif  5404  funimaexglem  5407  isarep1  5410  2elresin  5437  fnres  5443  fcnvres  5514  fconstg  5527  fun11iun  5598  f1osng  5619  dffv3g  5628  fvssunirng  5647  sefvex  5653  fv3  5655  fvres  5656  nfunsn  5669  funimass4  5689  ssimaexg  5701  dmfco  5707  fvopab6  5736  fndmdif  5745  fvelrn  5771  dffo4  5788  f1ompt  5791  fmptco  5806  fsn  5812  fsng  5813  dfmpt  5817  dfmptg  5819  funopsn  5822  funop  5823  funopdmsn  5826  fnressn  5832  fressnfv  5833  fvsng  5842  resfunexg  5867  funfvima3  5880  idref  5889  abrexco  5892  imaiun  5893  dff13  5901  foeqcnvco  5923  f1eqcocnv  5924  fliftcnv  5928  isocnv2  5945  isoini  5951  isose  5954  riotav  5969  csbriotag  5977  acexmidlem2  6007  oprabid  6042  csbov123g  6049  0neqopab  6058  brabvv  6059  dfoprab2  6060  rnoprab  6096  eloprabga  6100  mpov  6103  f1opw  6222  opabex3d  6275  opabex3  6276  ofmres  6290  uchoice  6292  op1stg  6305  op2ndg  6306  1stval2  6310  2ndval2  6311  fo1st  6312  fo2nd  6313  f1stres  6314  f2ndres  6315  fo1stresm  6316  fo2ndresm  6317  xp1st  6320  xp2nd  6321  releldm2  6340  reldm  6341  sbcopeq1a  6342  csbopeq1a  6343  dfoprab3  6346  opabn1stprc  6350  eloprabi  6353  mpomptsx  6354  dmmpossx  6356  fmpox  6357  mpofvex  6362  mpoexxg  6367  fmpoco  6373  df1st2  6376  df2nd2  6377  1stconst  6378  2ndconst  6379  dfmpo  6380  fo2ndf  6384  f1o2ndf1  6385  xporderlem  6388  cnvoprab  6391  f1od2  6392  brtpos2  6408  reldmtpos  6410  dmtpos  6413  rntpos  6414  ovtposg  6416  dftpos3  6419  dftpos4  6420  tpostpos  6421  tpossym  6433  tfrlem3  6468  tfrlem5  6471  tfrlem8  6475  tfrlemisucfn  6481  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemibfn  6485  tfrlemibex  6486  tfrlemi14d  6490  tfrexlem  6491  tfr1onlem3  6495  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemres  6506  tfri1dALT  6508  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemres  6519  tfrcl  6521  rdgtfr  6531  rdgruledefgg  6532  rdgivallem  6538  rdgon  6543  rdg0g  6545  frec0g  6554  frecabex  6555  frecabcl  6556  frectfr  6557  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecrdg  6565  oafnex  6603  sucinc  6604  fnoa  6606  oaexg  6607  omfnex  6608  fnom  6609  omexg  6610  fnoei  6611  oeiexg  6612  oeiv  6615  oacl  6619  omcl  6620  oeicl  6621  oav2  6622  nnsucelsuc  6650  nnsucuniel  6654  ercnv  6714  iserd  6719  eqerlem  6724  eqer  6725  ecdmn0m  6737  erth  6739  qsss  6754  ecid  6758  ecidg  6759  qsid  6760  iinerm  6767  qsel  6772  erovlem  6787  ecopovsym  6791  ecopover  6793  th3qlem2  6798  mapprc  6812  fnmap  6815  fnpm  6816  mapdm0  6823  mapval2  6838  mapsn  6850  mapsncnv  6855  mapsnf1o2  6856  ixpconstg  6867  ixpprc  6879  ixpin  6883  ixpiinm  6884  ixpssmap2g  6887  ixpssmapg  6888  elixpsn  6895  ixpsnf1o  6896  bren  6908  brdomg  6910  domen  6913  domeng  6914  idssen  6941  domssr  6942  ener  6944  domtr  6950  ensn1g  6962  en1  6964  en1bg  6965  fundmen  6972  fundmeng  6973  mapsnen  6977  fiprc  6981  unen  6982  rex2dom  6984  en2m  6987  dom1o  6990  xpsnen  6993  xpsneng  6994  xpcomco  6998  xpcomeng  7000  xpassen  7002  xpdom2  7003  xpdom2g  7004  pw2f1odc  7009  xpf1o  7018  mapen  7020  mapxpen  7022  xpmapenlem  7023  ssenen  7025  phplem4  7029  phplem3g  7030  nneneq  7031  php5  7032  phpm  7040  findcard  7063  findcard2  7064  findcard2s  7065  isinfinf  7072  ac6sfi  7073  exmidpw  7086  exmidpweq  7087  exmidpw2en  7090  unfidisj  7100  fiintim  7109  xpfi  7110  fisseneq  7112  ssfirab  7114  snexxph  7133  fidcenumlemr  7138  sbthlemi10  7149  isbth  7150  ssfii  7157  fi0  7158  fiss  7160  cnvinfex  7201  eqinfti  7203  infvalti  7205  infglbti  7208  infmoti  7211  ordiso2  7218  djuf1olem  7236  djuss  7253  ctm  7292  ctssdccl  7294  ctssdclemr  7295  finomni  7323  exmidomni  7325  fodjuomnilemdc  7327  nninfwlpoimlemginf  7359  pm54.43  7379  pr2cv1  7384  exmidfodomrlemim  7395  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  finacn  7402  acfun  7405  ccfunen  7466  cc2lem  7468  cc3  7470  acnccim  7474  indpi  7545  dfplpq2  7557  enq0sym  7635  enq0ref  7636  enq0tr  7637  nqnq0pi  7641  nqnq0  7644  mulnnnq0  7653  nqprm  7745  nqprrnd  7746  nqprdisj  7747  nqprloc  7748  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  addnqprlemfl  7762  addnqprlemfu  7763  mulnqprlemrl  7776  mulnqprlemru  7777  mulnqprlemfl  7778  mulnqprlemfu  7779  ltnqpr  7796  ltnqpri  7797  archpr  7846  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlem2  7863  caucvgprlemladdfu  7880  caucvgprlem2  7883  caucvgprprlemopu  7902  suplocexprlemmu  7921  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  cnm  8035  ltresr  8042  peano1nnnn  8055  peano2nnnn  8056  axcnre  8084  axpre-apti  8088  renfdisj  8222  dfinfre  9119  1nn  9137  peano2nn  9138  indstr  9805  cnref1o  9863  ioof  10184  fzpr  10290  frec2uzrand  10644  frec2uzf1od  10645  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  frecfzennn  10665  seqp1g  10705  seqclg  10711  seqf1og  10760  seqfeq4g  10770  ser3le  10776  hashinfom  11017  hashunlem  11043  hashun  11044  hashxp  11066  hashfacen  11076  zfz1isolem1  11080  zfz1iso  11081  fundm2domnop0  11085  wrdexb  11101  fnpfx  11230  cats1un  11274  wrdind  11275  wrd2ind  11276  shftfvalg  11350  ovshftex  11351  shftfibg  11352  shftfval  11353  shftfib  11355  shftfn  11356  2shfti  11363  shftvalg  11368  shftval4g  11369  maxabslemval  11740  fimaxre2  11759  xrmaxiflemval  11782  fclim  11826  climshft  11836  zsumdc  11916  fsum3  11919  fsum2dlemstep  11966  fsumcnv  11969  fisumcom2  11970  fisum0diag2  11979  fsumconst  11986  modfsummodlemstep  11989  fsumabs  11997  fsumrelem  12003  fsumiun  12009  ntrivcvgap  12080  fprod2dlemstep  12154  fprodcnv  12157  fprodcom2fi  12158  fprodmodd  12173  nninfct  12583  algrf  12588  qredeu  12640  isprm2  12660  prmind2  12663  4sqlemafi  12939  4sqlem12  12946  ennnfonelemex  13006  ennnfonelemrn  13011  exmidunben  13018  ctinfom  13020  ctinf  13022  qnnen  13023  enctlem  13024  ctiunctlemfo  13031  slotslfn  13079  setscomd  13094  restfn  13297  elrest  13300  ptex  13318  prdsex  13323  prdsvallem  13326  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfnlemg  13368  fnpr2ob  13394  ismgm  13411  plusffng  13419  fn0g  13429  fngsum  13442  gsumsplit1r  13452  gsumprval  13453  issgrp  13457  ismnddef  13472  gsumfzz  13549  gsumfzcl  13553  mulgnngsum  13685  subgintm  13756  releqgg  13778  eqgex  13779  eqgfval  13780  eqgval  13781  isghm  13801  fnmgp  13906  isrng  13918  isring  13984  ringn0  14044  opprrngbg  14062  opprsubgg  14068  opprunitd  14095  dfrhm2  14139  rhmex  14142  opprsubrngg  14196  subrngintm  14197  subrngpropd  14201  subrgpropd  14238  isdomn  14254  opprdomnbg  14259  scaffng  14294  rmodislmodlem  14335  rmodislmod  14336  lssex  14339  lsssn0  14355  lss1d  14368  lssintclm  14369  ellspsn  14402  rlmfn  14438  isridl  14489  blfn  14536  mopnset  14537  metuex  14540  znval  14621  znleval  14638  psrval  14651  fnpsr  14652  mplvalcoe  14675  fnmpl  14678  bastg  14756  distop  14780  topnex  14781  epttop  14785  tgrest  14864  resttopon  14866  restco  14869  cnrest2  14931  cnptopresti  14933  cnptoprest  14934  cnptoprest2  14935  txuni2  14951  txbas  14953  eltx  14954  txcnp  14966  txcnmpt  14968  txrest  14971  txdis1cn  14973  txlm  14974  cnmpt1st  14983  cnmpt2nd  14984  txhmeo  15014  txswaphmeolem  15015  xmetec  15132  metrest  15201  reldvg  15374  dvfgg  15383  dvcj  15404  dvmptfsum  15420  elply2  15430  pilem3  15478  lgsquadlem1  15777  lgsquadlem2  15778  upgrex  15924  umgredg  15964  umgredgnlp  15971  usgredgreu  16035  uspgredg2vtxeu  16037  ushgredgedg  16045  ushgredgedgloop  16047  griedg0ssusgr  16070  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlk1walkdom  16131  bdcvv  16329  bdsnss  16345  bdop  16347  bj-vprc  16368  bdinex1g  16373  bdssexg  16376  bj-inex  16379  bj-zfpair2  16382  bj-uniexg  16390  bdunexb  16392  bj-unexg  16393  bj-indint  16403  bj-ssom  16408  bj-om  16409  bj-2inf  16410  bj-bdfindis  16419  bj-nn0suc0  16422  bj-nnelirr  16425  bj-inf2vnlem1  16442  bj-inf2vnlem2  16443  bj-omex2  16449  bj-nn0sucALT  16450  bj-findis  16451  ss1oel2o  16464  domomsubct  16480  pw1nct  16482  nninfsellemeq  16494  exmidsbthrlem  16504