Theorem vex 2824

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

Syntax hints:   ∈ wcel 2209  Vcvv 2821

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  elv  2825  elvd  2826  el2v  2827  isset  2828  eqvisset  2832  ralv  2839  rexv  2840  reuv  2841  rmov  2842  rabab  2843  sbhypf  2872  ceqex  2953  ralab  2986  rexab  2988  mo2icl  3005  reu8  3022  csbvarg  3175  csbiebg  3190  sbcnestgf  3199  sbnfc2  3208  ddifnel  3360  ddifstab  3361  csbing  3438  unssdif  3466  unssin  3470  inssun  3471  invdif  3473  vn0  3532  vn0m  3533  eqv  3541  abvor0dc  3545  sbss  3635  velpw  3695  elpwg  3696  velsn  3725  vsnid  3740  exsnrex  3750  dftp2  3757  prmg  3833  prnzg  3836  snssgOLD  3849  difprsnss  3851  sneqrg  3885  preq12bg  3896  pwprss  3929  pwtpss  3930  pwv  3932  unipr  3947  uniprg  3948  unisng  3950  elintg  3976  elintrabg  3981  intss1  3983  ssint  3984  intmin  3988  intss  3989  intssunim  3990  intmin4  3996  intab  3997  intun  3999  intpr  4000  intprg  4001  uniintsnr  4004  iinconstm  4019  iuniin  4020  iinss1  4022  dfiin2g  4043  dfiunv2  4046  ssiinf  4060  iinss  4062  iinss2  4063  0iin  4069  iinab  4072  iundif2ss  4076  iindif2m  4078  iinin2m  4079  iinuniss  4093  sspwuni  4095  pwpwab  4098  iinpw  4101  iunpwss  4102  brab1  4176  csbopabg  4207  mptv  4226  trint  4242  vnex  4262  inex1g  4267  ssexg  4270  inteximm  4283  inuni  4289  repizf2  4297  axpweq  4306  bnd2  4308  pwuni  4327  exmidundif  4341  exmidundifim  4342  zfpair2  4345  rext  4353  sspwb  4354  unipw  4355  ssextss  4358  euabex  4363  mss  4364  exss  4365  opth  4375  opthg  4376  copsexg  4382  copsex4g  4385  moop2  4390  euotd  4393  opabid  4396  elopab  4398  opelopabsbALT  4399  opelopabsb  4400  opabm  4421  pwin  4425  pwunss  4426  epelg  4433  epel  4435  pofun  4455  epse  4485  tron  4525  sucel  4553  suctr  4564  vuniex  4582  uniexg  4583  unexb  4586  snnex  4592  pwnex  4593  uniuni  4595  eusvnf  4597  eusvnfb  4598  iunpw  4624  unon  4656  ordunisuc2r  4659  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  ordsucunielexmid  4676  elirr  4686  en2lp  4699  dtruex  4704  onintexmid  4718  reg3exmidlemwe  4724  dcextest  4726  finds  4745  finds2  4746  elomssom  4750  limom  4759  0nelxp  4800  opelxp  4802  opeliunxp  4828  elvv  4835  elvvv  4836  elvvuni  4837  xpsspw  4885  relopabiv  4901  relopabi  4903  opabid2  4909  difopab  4911  xpiindim  4915  raliunxp  4919  rexiunxp  4920  ralxpf  4924  rexxpf  4925  relop  4928  cnvco  4963  dfrn2  4966  dfdm4  4971  dmss  4978  dmin  4987  dmiun  4988  dmuni  4989  dm0  4993  dmi  4994  reldm0  4997  reldmm  4998  elreldm  5006  elrnmpt1  5031  dmrnssfld  5043  dmcoss  5050  dmcosseq  5052  opelresg  5068  resieq  5071  dmres  5082  elres  5097  relssres  5099  resopab  5105  resiexg  5106  iss  5107  dfres2  5113  restidsing  5117  dfima2  5126  imadmrn  5134  imai  5141  csbima12g  5146  elimasng  5153  args  5154  epini  5156  iniseg  5157  dfse2  5158  exse2  5159  cotr  5167  issref  5168  cnvsym  5169  intasym  5170  asymref  5171  intirr  5172  brcodir  5173  codir  5174  qfto  5175  poirr2  5178  cnvopab  5187  cnv0  5189  cnvi  5190  cnvdif  5192  rniun  5196  dminss  5200  imainss  5201  inimasn  5203  xpmlem  5206  dmxpss  5216  rnxpid  5220  ssrnres  5228  rninxp  5229  dminxp  5230  cnvcnv3  5235  dfrel2  5236  dmsnm  5251  dmsnopg  5257  cnvcnvsn  5262  dmsnsnsng  5263  cnvsng  5271  elxp4  5273  elxp5  5274  cnvresima  5275  dfco2  5285  dfco2a  5286  cores  5289  resco  5290  imaco  5291  rnco  5292  coiun  5295  co02  5299  coi1  5301  coass  5304  relssdmrn  5306  unielrel  5313  ressn  5326  cnviinm  5327  cnvpom  5328  cnvsom  5329  uniabio  5346  iotaval  5347  iotass  5353  sniota  5366  csbiotag  5368  dffun2  5385  dffun7  5402  dffun8  5403  dffun9  5404  funopg  5409  funssres  5418  funun  5420  funcnvsn  5424  funinsn  5428  funcnv2  5439  funcnv  5440  funcnv3  5441  funcnveq  5442  fun2cnv  5443  funcnvuni  5448  imadif  5459  funimaexglem  5462  isarep1  5465  2elresin  5492  fnres  5498  fcnvres  5573  fconstg  5587  fun11iun  5658  f1osng  5680  dffv3g  5689  fvssunirng  5708  sefvex  5714  fv3  5716  fvres  5717  nfunsn  5730  funimass4  5750  ssimaexg  5762  dmfco  5770  fvopab6  5799  fndmdif  5808  fvelrn  5833  dffo4  5850  f1ompt  5853  fmptco  5868  fsn  5874  fsng  5875  fsn2g  5877  dfmpt  5880  dfmptg  5882  funopsn  5885  funop  5886  funopdmsn  5889  fnressn  5895  fressnfv  5896  fvsng  5905  resfunexg  5930  funfvima3  5946  idref  5956  abrexco  5959  imaiun  5960  dff13  5968  foeqcnvco  5990  f1eqcocnv  5991  fliftcnv  5995  isocnv2  6012  isoini  6018  isose  6021  riotav  6038  csbriotag  6046  acexmidlem2  6076  oprabid  6111  csbov123g  6118  0neqopab  6127  brabvv  6128  dfoprab2  6129  rnoprab  6165  eloprabga  6169  mpov  6172  f1opw  6291  opabex3d  6344  opabex3  6345  abrexss  6352  ofmres  6363  uchoice  6365  op1stg  6378  op2ndg  6379  1stval2  6383  2ndval2  6384  fo1st  6385  fo2nd  6386  f1stres  6387  f2ndres  6388  fo1stresm  6389  fo2ndresm  6390  xp1st  6393  xp2nd  6394  releldm2  6413  reldm  6414  sbcopeq1a  6415  csbopeq1a  6416  dfoprab3  6419  opabn1stprc  6423  eloprabi  6426  mpomptsx  6427  dmmpossx  6429  fmpox  6430  mpofvex  6435  mpoexxg  6440  fmpoco  6446  df1st2  6449  df2nd2  6450  1stconst  6451  2ndconst  6452  dfmpo  6453  fo2ndf  6457  f1o2ndf1  6458  xporderlem  6461  cnvoprab  6464  f1od2  6465  suppval1  6473  cnvimadfsn  6479  suppimacnvfn  6480  brtpos2  6516  reldmtpos  6518  dmtpos  6521  rntpos  6522  ovtposg  6524  dftpos3  6527  dftpos4  6528  tpostpos  6529  tpossym  6541  tfrlem3  6576  tfrlem5  6579  tfrlem8  6583  tfrlemisucfn  6589  tfrlemisucaccv  6590  tfrlemibxssdm  6592  tfrlemibfn  6593  tfrlemibex  6594  tfrlemi14d  6598  tfrexlem  6599  tfr1onlem3  6603  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfr1onlemres  6614  tfri1dALT  6616  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllembfn  6622  tfrcllemres  6627  tfrcl  6629  rdgtfr  6639  rdgruledefgg  6640  rdgivallem  6646  rdgon  6651  rdg0g  6653  frec0g  6662  frecabex  6663  frecabcl  6664  frectfr  6665  freccllem  6667  frecfcllem  6669  frecsuclem  6671  frecrdg  6673  oafnex  6711  sucinc  6712  fnoa  6714  oaexg  6715  omfnex  6716  fnom  6717  omexg  6718  fnoei  6719  oeiexg  6720  oeiv  6723  oacl  6727  omcl  6728  oeicl  6729  oav2  6730  nnsucelsuc  6758  nnsucuniel  6762  ercnv  6822  iserd  6827  eqerlem  6832  eqer  6833  ecdmn0m  6845  erth  6847  qsss  6862  ecid  6866  ecidg  6867  qsid  6868  iinerm  6875  qsel  6880  erovlem  6895  ecopovsym  6899  ecopover  6901  th3qlem2  6906  mapprc  6920  fnmap  6923  fnpm  6924  mapdm0  6931  mapfset  6939  mapfoss  6941  fsetsspwxp  6942  fsetdmprc0  6944  mapval2  6953  mapsnd  6964  mapsn  6966  mapsncnv  6971  mapsnf1o2  6972  ixpconstg  6983  ixpprc  6995  ixpin  6999  ixpiinm  7000  ixpssmap2g  7003  ixpssmapg  7004  elixpsn  7011  ixpsnf1o  7012  bren  7024  brdomg  7026  domen  7029  domeng  7030  idssen  7057  domssr  7058  ener  7060  domtr  7066  ensn1g  7078  en1  7080  en1bg  7081  fundmen  7088  fundmeng  7089  mapsnend  7093  mapsnen  7094  fiprc  7098  unen  7099  rex2dom  7104  en2m  7107  dom1o  7110  xpsnen  7113  xpsneng  7114  xpcomco  7118  xpcomeng  7120  xpassen  7122  xpdom2  7123  xpdom2g  7124  pw2f1odc  7129  xpf1o  7138  mapen  7140  mapxpen  7142  xpmapenlem  7143  mapunen  7145  ssenen  7146  phplem4  7150  phplem3g  7151  nneneq  7152  php5  7153  phpm  7161  findcard  7186  findcard2  7187  findcard2s  7188  isinfinf  7195  ac6sfi  7196  exmidpw  7209  exmidpweq  7210  exmidpw2en  7213  unfidisj  7223  fiintim  7232  xpfi  7233  fisseneq  7236  ssfirab  7238  mapfi  7255  snexxph  7261  fidcenumlemr  7266  sbthlemi10  7277  isbth  7278  ssfii  7302  fi0  7303  fiss  7305  f1setfi  7311  cnvinfex  7352  eqinfti  7354  infvalti  7356  infglbti  7359  infmoti  7362  ordiso2  7369  djuf1olem  7387  djuss  7404  ctm  7443  ctssdccl  7445  ctssdclemr  7446  finomni  7474  exmidomni  7476  fodjuomnilemdc  7478  nninfwlpoimlemginf  7510  pm54.43  7530  pr2cv1  7535  exmidfodomrlemim  7547  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  finacn  7554  acfun  7557  ccfunen  7624  cc2lem  7626  cc3  7628  acnccim  7632  indpi  7703  dfplpq2  7715  enq0sym  7793  enq0ref  7794  enq0tr  7795  nqnq0pi  7799  nqnq0  7802  mulnnnq0  7811  nqprm  7903  nqprrnd  7904  nqprdisj  7905  nqprloc  7906  nqprl  7912  nqpru  7913  addnqprlemrl  7918  addnqprlemru  7919  addnqprlemfl  7920  addnqprlemfu  7921  mulnqprlemrl  7934  mulnqprlemru  7935  mulnqprlemfl  7936  mulnqprlemfu  7937  ltnqpr  7954  ltnqpri  7955  archpr  8004  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlem2  8021  caucvgprlemladdfu  8038  caucvgprlem2  8041  caucvgprprlemopu  8060  suplocexprlemmu  8079  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemub  8084  cnm  8193  ltresr  8200  peano1nnnn  8213  peano2nnnn  8214  axcnre  8242  axpre-apti  8246  renfdisj  8379  dfinfre  9280  1nn  9298  peano2nn  9299  indstr  9976  cnref1o  10034  ioof  10356  fzpr  10467  frec2uzrand  10825  frec2uzf1od  10826  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  frecfzennn  10846  seqp1g  10886  seqclg  10892  seqf1og  10941  seqfeq4g  10951  ser3le  10957  hashinfom  11200  hashunlem  11227  hashun  11228  hashxp  11250  hashmap  11251  hashfibclem  11265  hashfacen  11267  hashf1lem1  11268  hashf1lem2  11269  hashf1  11270  zfz1isolem1  11275  zfz1iso  11276  fundm2domnop0  11283  wrdexb  11299  fnpfx  11432  cats1un  11476  wrdind  11477  wrd2ind  11478  shftfvalg  11566  ovshftex  11567  shftfibg  11568  shftfval  11569  shftfib  11571  shftfn  11572  2shfti  11579  shftvalg  11584  shftval4g  11585  maxabslemval  11957  fimaxre2  11976  xrmaxiflemval  11999  fclim  12043  climshft  12053  zsumdc  12134  fsum3  12137  fsum2dlemstep  12184  fsumcnv  12187  fisumcom2  12188  fisum0diag2  12197  fsumconst  12204  modfsummodlemstep  12207  fsumabs  12215  fsumrelem  12221  fsumiun  12227  ntrivcvgap  12298  fprod2dlemstep  12372  fprodcnv  12375  fprodcom2fi  12376  fprodmodd  12391  nninfct  12801  algrf  12806  qredeu  12858  isprm2  12878  prmind2  12881  4sqlemafi  13157  4sqlem12  13164  ballotfilemcdc  13206  ballotfilemsf1o  13240  ballotfilem7  13262  ennnfonelemex  13288  ennnfonelemrn  13293  exmidunben  13300  ctinfom  13302  ctinf  13304  qnnen  13305  enctlem  13306  ctiunctlemfo  13313  slotslfn  13361  setscomd  13376  restfn  13580  elrest  13583  ptex  13601  prdsvallem  13604  imasex  13609  imasival  13610  imasbas  13611  imasplusg  13612  imasmulr  13613  imasaddfnlemg  13618  fnpr2ob  13644  ismgm  13660  plusffng  13668  fn0g  13678  fngzsum  13691  gzsumsplit1r  13698  issgrp  13701  ismnddef  13714  gzsumcl  13787  mulgnngzsum  13913  subgintm  13984  releqgg  14006  eqgex  14007  eqgfval  14008  eqgval  14009  isghm  14029  gsumvalfi  14135  prdsex  14155  prdsval  14156  prdsbaslemss  14157  prdsbas  14159  fnmgp  14202  isrng  14216  isring  14287  ringn0  14348  opprrngbg  14366  opprsubgg  14373  opprunitd  14400  dfrhm2  14444  rhmex  14447  opprsubrngg  14502  subrngintm  14503  subrngpropd  14507  subrgpropd  14544  isdomn  14561  opprdomnbg  14566  scaffng  14629  rmodislmodlem  14670  rmodislmod  14671  lssex  14674  lsssn0  14690  lss1d  14703  lssintclm  14704  ellspsn  14737  rlmfn  14773  isridl  14824  blfn  14871  mopnset  14872  metuex  14875  znval  14954  znleval  14971  psrval  15033  fnpsr  15034  mplvalcoe  15064  fnmpl  15067  bastg  15145  distop  15169  topnex  15170  epttop  15174  tgrest  15253  resttopon  15255  restco  15258  cnrest2  15320  cnptopresti  15322  cnptoprest  15323  cnptoprest2  15324  txuni2  15340  txbas  15342  eltx  15343  txcnp  15355  txcnmpt  15357  txrest  15360  txdis1cn  15362  txlm  15363  cnmpt1st  15372  cnmpt2nd  15373  txhmeo  15403  txswaphmeolem  15404  xmetec  15521  metrest  15590  reldvg  15763  dvfgg  15772  dvcj  15793  dvmptfsum  15809  elply2  15819  pilem3  15867  lgsquadlem1  16179  lgsquadlem2  16180  upgrex  16327  upgr1een  16348  umgredg  16369  umgredgnlp  16376  usgredgreu  16440  uspgredg2vtxeu  16442  ushgredgedg  16450  ushgredgedgloop  16452  griedg0ssusgr  16475  uhgrspansubgrlem  16500  upgrspanop  16507  umgrspanop  16508  usgrspanop  16509  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlk1walkdom  16583  eulerpathum  16705  depindlem1  16730  bdcvv  16866  bdsnss  16882  bdop  16884  bj-vprc  16905  bdinex1g  16910  bdssexg  16913  bj-inex  16916  bj-zfpair2  16919  bj-uniexg  16927  bdunexb  16929  bj-unexg  16930  bj-indint  16940  bj-ssom  16945  bj-om  16946  bj-2inf  16947  bj-bdfindis  16956  bj-nn0suc0  16959  bj-nnelirr  16962  bj-inf2vnlem1  16979  bj-inf2vnlem2  16980  bj-omex2  16986  bj-nn0sucALT  16987  bj-findis  16988  ss1oel2o  17000  domomsubct  17014  pw1nct  17016  nninfsellemeq  17031  exmidsbthrlem  17041