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

This proof depends on syntax axioms:   ∈ wcel 2209  Vcvv 2821

This proof depends on 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 proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used 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  3726  vsnid  3741  exsnrex  3751  dftp2  3758  prmg  3835  prnzg  3838  snssgOLD  3851  difprsnss  3853  sneqrg  3887  preq12bg  3898  pwprss  3931  pwtpss  3932  pwv  3934  unipr  3949  uniprg  3950  unisng  3952  elintg  3978  elintrabg  3983  intss1  3985  ssint  3986  intmin  3990  intss  3991  intssunim  3992  intmin4  3998  intab  3999  intun  4001  intpr  4002  intprg  4003  uniintsnr  4006  iinconstm  4021  iuniin  4022  iinss1  4024  dfiin2g  4045  dfiunv2  4048  ssiinf  4062  iinss  4064  iinss2  4065  0iin  4071  iinab  4074  iundif2ss  4078  iindif2m  4080  iinin2m  4081  iinuniss  4095  sspwuni  4097  pwpwab  4100  iinpw  4103  iunpwss  4104  brab1  4178  csbopabg  4209  mptv  4228  trint  4244  vnex  4264  inex1g  4269  ssexg  4272  inteximm  4285  inuni  4291  repizf2  4299  axpweq  4308  bnd2  4310  pwuni  4329  exmidundif  4343  exmidundifim  4344  zfpair2  4347  rext  4355  sspwb  4356  unipw  4357  ssextss  4360  euabex  4365  mss  4366  exss  4367  opth  4377  opthg  4378  copsexg  4384  copsex4g  4387  moop2  4392  euotd  4395  opabid  4398  elopab  4400  opelopabsbALT  4401  opelopabsb  4402  opabm  4423  pwin  4427  pwunss  4428  epelg  4435  epel  4437  pofun  4457  epse  4487  tron  4527  sucel  4555  suctr  4566  vuniex  4584  uniexg  4585  unexb  4588  snnex  4594  pwnex  4595  uniuni  4597  eusvnf  4599  eusvnfb  4600  iunpw  4626  unon  4658  ordunisuc2r  4661  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsucunielexmid  4678  elirr  4688  en2lp  4701  dtruex  4706  onintexmid  4720  reg3exmidlemwe  4726  dcextest  4728  finds  4747  finds2  4748  elomssom  4752  limom  4761  0nelxp  4802  opelxp  4804  opeliunxp  4830  elvv  4837  elvvv  4838  elvvuni  4839  xpsspw  4887  relopabiv  4903  relopabi  4905  opabid2  4911  difopab  4913  xpiindim  4917  raliunxp  4921  rexiunxp  4922  ralxpf  4926  rexxpf  4927  relop  4930  cnvco  4965  dfrn2  4968  dfdm4  4973  dmss  4980  dmin  4989  dmiun  4990  dmuni  4991  dm0  4995  dmi  4996  reldm0  4999  reldmm  5000  elreldm  5008  elrnmpt1  5033  dmrnssfld  5045  dmcoss  5052  dmcosseq  5054  opelresg  5070  resieq  5073  dmres  5084  elres  5099  relssres  5101  resopab  5107  resiexg  5108  iss  5109  dfres2  5115  restidsing  5119  dfima2  5128  imadmrn  5136  imai  5143  csbima12g  5148  elimasng  5155  args  5156  epini  5158  iniseg  5159  dfse2  5160  exse2  5161  cotr  5169  issref  5170  cnvsym  5171  intasym  5172  asymref  5173  intirr  5174  brcodir  5175  codir  5176  qfto  5177  poirr2  5180  cnvopab  5189  cnv0  5191  cnvi  5192  cnvdif  5194  rniun  5198  dminss  5202  imainss  5203  inimasn  5205  xpmlem  5208  dmxpss  5218  rnxpid  5222  ssrnres  5230  rninxp  5231  dminxp  5232  cnvcnv3  5237  dfrel2  5238  dmsnm  5253  dmsnopg  5259  cnvcnvsn  5264  dmsnsnsng  5265  cnvsng  5273  elxp4  5275  elxp5  5276  cnvresima  5277  dfco2  5287  dfco2a  5288  cores  5291  resco  5292  imaco  5293  rnco  5294  coiun  5297  co02  5301  coi1  5303  coass  5306  relssdmrn  5308  unielrel  5315  ressn  5328  cnviinm  5329  cnvpom  5330  cnvsom  5331  uniabio  5348  iotaval  5349  iotass  5355  sniota  5368  csbiotag  5370  dffun2  5387  dffun7  5404  dffun8  5405  dffun9  5406  funopg  5411  funssres  5420  funun  5422  funcnvsn  5426  funinsn  5430  funcnv2  5441  funcnv  5442  funcnv3  5443  funcnveq  5444  fun2cnv  5445  funcnvuni  5450  imadif  5461  funimaexglem  5464  isarep1  5467  2elresin  5494  fnres  5500  fcnvres  5575  fconstg  5589  fun11iun  5660  f1osng  5682  dffv3g  5691  fvssunirng  5710  sefvex  5716  fv3  5718  fvres  5719  nfunsn  5733  funimass4  5753  ssimaexg  5765  dmfco  5773  fvopab6  5805  fndmdif  5814  fvelrn  5839  dffo4  5856  f1ompt  5859  fmptco  5874  fsn  5880  fsng  5881  fsn2g  5883  dfmpt  5886  dfmptg  5888  funopsn  5891  funop  5892  funopdmsn  5895  fnressn  5901  fressnfv  5902  fvsng  5911  resfunexg  5936  funfvima3  5952  idref  5962  abrexco  5965  imaiun  5966  dff13  5974  foeqcnvco  5996  f1eqcocnv  5997  fliftcnv  6001  isocnv2  6018  isoini  6024  isose  6027  riotav  6044  csbriotag  6052  acexmidlem2  6082  oprabid  6117  csbov123g  6124  0neqopab  6133  brabvv  6134  dfoprab2  6135  rnoprab  6171  eloprabga  6175  mpov  6178  f1opw  6297  opabex3d  6350  opabex3  6351  abrexss  6358  ofmres  6369  uchoice  6371  op1stg  6384  op2ndg  6385  1stval2  6389  2ndval2  6390  fo1st  6391  fo2nd  6392  f1stres  6393  f2ndres  6394  fo1stresm  6395  fo2ndresm  6396  xp1st  6399  xp2nd  6400  releldm2  6419  reldm  6420  sbcopeq1a  6421  csbopeq1a  6422  dfoprab3  6425  opabn1stprc  6429  eloprabi  6432  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  mpoexxg  6446  fmpoco  6452  df1st2  6455  df2nd2  6456  1stconst  6457  2ndconst  6458  dfmpo  6459  fo2ndf  6463  f1o2ndf1  6464  xporderlem  6467  cnvoprab  6470  f1od2  6471  suppval1  6479  cnvimadfsn  6485  suppimacnvfn  6486  brtpos2  6522  reldmtpos  6524  dmtpos  6527  rntpos  6528  ovtposg  6530  dftpos3  6533  dftpos4  6534  tpostpos  6535  tpossym  6547  tfrlem3  6582  tfrlem5  6585  tfrlem8  6589  tfrlemisucfn  6595  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemibex  6600  tfrlemi14d  6604  tfrexlem  6605  tfr1onlem3  6609  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  tfrcl  6635  rdgtfr  6645  rdgruledefgg  6646  rdgivallem  6652  rdgon  6657  rdg0g  6659  frec0g  6668  frecabex  6669  frecabcl  6670  frectfr  6671  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  oafnex  6717  sucinc  6718  fnoa  6720  oaexg  6721  omfnex  6722  fnom  6723  omexg  6724  fnoei  6725  oeiexg  6726  oeiv  6729  oacl  6733  omcl  6734  oeicl  6735  oav2  6736  nnsucelsuc  6764  nnsucuniel  6768  ercnv  6828  iserd  6833  eqerlem  6838  eqer  6839  ecdmn0m  6851  erth  6853  qsss  6868  ecid  6872  ecidg  6873  qsid  6874  iinerm  6881  qsel  6886  erovlem  6901  ecopovsym  6905  ecopover  6907  th3qlem2  6912  mapprc  6926  fnmap  6929  fnpm  6930  mapdm0  6937  mapfset  6945  mapfoss  6947  fsetsspwxp  6948  fsetdmprc0  6950  mapval2  6959  mapsnd  6970  mapsn  6972  mapsncnv  6977  mapsnf1o2  6978  ixpconstg  6989  ixpprc  7001  ixpin  7005  ixpiinm  7006  ixpssmap2g  7009  ixpssmapg  7010  elixpsn  7017  ixpsnf1o  7018  bren  7030  brdomg  7032  domen  7035  domeng  7036  idssen  7063  domssr  7064  ener  7066  domtr  7072  ensn1g  7084  en1  7086  en1bg  7087  fundmen  7094  fundmeng  7095  mapsnend  7099  mapsnen  7100  fiprc  7104  unen  7105  rex2dom  7110  en2m  7113  dom1o  7116  xpsnen  7119  xpsneng  7120  xpcomco  7124  xpcomeng  7126  xpassen  7128  xpdom2  7129  xpdom2g  7130  pw2f1odc  7135  xpf1o  7144  mapen  7146  mapxpen  7148  xpmapenlem  7149  mapunen  7151  ssenen  7152  phplem4  7156  phplem3g  7157  nneneq  7158  php5  7159  phpm  7167  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  ac6sfi  7202  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  unfidisj  7229  fiintim  7238  xpfi  7239  fisseneq  7242  ssfirab  7244  mapfi  7261  snexxph  7267  fidcenumlemr  7272  sbthlemi10  7283  isbth  7284  ssfii  7308  fi0  7309  fiss  7311  f1setfi  7317  cnvinfex  7358  eqinfti  7360  infvalti  7362  infglbti  7365  infmoti  7368  ordiso2  7375  djuf1olem  7393  djuss  7410  ctm  7449  ctssdccl  7451  ctssdclemr  7452  finomni  7480  exmidomni  7482  fodjuomnilemdc  7484  nninfwlpoimlemginf  7516  pm54.43  7536  pr2cv1  7541  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  finacn  7560  acfun  7563  ccfunen  7630  cc2lem  7632  cc3  7634  acnccim  7638  indpi  7709  dfplpq2  7721  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  mulnnnq0  7817  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  ltnqpr  7960  ltnqpri  7961  archpr  8010  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemopu  8066  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  cnm  8199  ltresr  8206  peano1nnnn  8219  peano2nnnn  8220  axcnre  8248  axpre-apti  8252  renfdisj  8385  dfinfre  9287  1nn  9316  peano2nn  9317  indstr  9995  cnref1o  10053  ioof  10375  fzpr  10486  frec2uzrand  10844  frec2uzf1od  10845  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  frecfzennn  10865  seqp1g  10905  seqclg  10911  seqf1og  10960  seqfeq4g  10970  ser3le  10976  hashinfom  11219  hashunlem  11246  hashun  11247  hashxp  11269  hashmap  11270  hashfibclem  11284  hashfacen  11286  hashf1lem1  11287  hashf1lem2  11288  hashf1  11289  zfz1isolem1  11294  zfz1iso  11295  fundm2domnop0  11302  wrdexb  11318  fnpfx  11451  cats1un  11495  wrdind  11496  wrd2ind  11497  shftfvalg  11585  ovshftex  11586  shftfibg  11587  shftfval  11588  shftfib  11590  shftfn  11591  2shfti  11598  shftvalg  11603  shftval4g  11604  maxabslemval  11976  fimaxre2  11995  xrmaxiflemval  12018  fclim  12062  climshft  12072  zsumdc  12153  fsum3  12156  fsum2dlemstep  12203  fsumcnv  12206  fisumcom2  12207  fisum0diag2  12216  fsumconst  12223  modfsummodlemstep  12226  fsumabs  12234  fsumrelem  12240  fsumiun  12246  ntrivcvgap  12317  fprod2dlemstep  12391  fprodcnv  12394  fprodcom2fi  12395  fprodmodd  12410  nninfct  12820  algrf  12825  qredeu  12877  isprm2  12897  prmind2  12900  4sqlemafi  13176  4sqlem12  13183  ballotfilemcdc  13225  ballotfilemsf1o  13259  ballotfilem7  13281  ennnfonelemex  13307  ennnfonelemrn  13312  exmidunben  13319  ctinfom  13321  ctinf  13323  qnnen  13324  enctlem  13325  ctiunctlemfo  13332  slotslfn  13380  setscomd  13395  restfn  13599  elrest  13602  ptex  13620  prdsvallem  13623  imasex  13628  imasival  13629  imasbas  13630  imasplusg  13631  imasmulr  13632  imasaddfnlemg  13637  fnpr2ob  13663  ismgm  13679  plusffng  13687  fn0g  13697  fngzsum  13710  gzsumsplit1r  13717  issgrp  13720  ismnddef  13733  gzsumcl  13806  mulgnngzsum  13932  subgintm  14003  releqgg  14025  eqgex  14026  eqgfval  14027  eqgval  14028  isghm  14048  gsumvalfi  14154  prdsex  14174  prdsval  14175  prdsbaslemss  14176  prdsbas  14178  fnmgp  14221  isrng  14235  isring  14306  ringn0  14367  opprrngbg  14385  opprsubgg  14392  opprunitd  14419  dfrhm2  14463  rhmex  14466  opprsubrngg  14521  subrngintm  14522  subrngpropd  14526  subrgpropd  14563  isdomn  14580  opprdomnbg  14585  scaffng  14648  rmodislmodlem  14689  rmodislmod  14690  lssex  14693  lsssn0  14709  lss1d  14722  lssintclm  14723  ellspsn  14756  rlmfn  14792  isridl  14843  blfn  14890  mopnset  14891  metuex  14894  znval  14973  znleval  14990  psrval  15052  fnpsr  15053  mplvalcoe  15083  fnmpl  15086  bastg  15164  distop  15188  topnex  15189  epttop  15193  tgrest  15272  resttopon  15274  restco  15277  cnrest2  15339  cnptopresti  15341  cnptoprest  15342  cnptoprest2  15343  txuni2  15359  txbas  15361  eltx  15362  txcnp  15374  txcnmpt  15376  txrest  15379  txdis1cn  15381  txlm  15382  cnmpt1st  15391  cnmpt2nd  15392  txhmeo  15422  txswaphmeolem  15423  xmetec  15540  metrest  15609  reldvg  15782  dvfgg  15791  dvcj  15812  dvmptfsum  15828  elply2  15838  pilem3  15887  lgsquadlem1  16208  lgsquadlem2  16209  upgrex  16356  upgr1een  16377  umgredg  16398  umgredgnlp  16405  usgredgreu  16469  uspgredg2vtxeu  16471  ushgredgedg  16479  ushgredgedgloop  16481  griedg0ssusgr  16504  uhgrspansubgrlem  16529  upgrspanop  16536  umgrspanop  16537  usgrspanop  16538  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlk1walkdom  16612  eulerpathum  16734  depindlem1  16759  bdcvv  16895  bdsnss  16911  bdop  16913  bj-vprc  16934  bdinex1g  16939  bdssexg  16942  bj-inex  16945  bj-zfpair2  16948  bj-uniexg  16956  bdunexb  16958  bj-unexg  16959  bj-indint  16969  bj-ssom  16974  bj-om  16975  bj-2inf  16976  bj-bdfindis  16985  bj-nn0suc0  16988  bj-nnelirr  16991  bj-inf2vnlem1  17008  bj-inf2vnlem2  17009  bj-omex2  17015  bj-nn0sucALT  17016  bj-findis  17017  ss1oel2o  17029  domomsubct  17043  pw1nct  17045  nninfsellemeq  17069  exmidsbthrlem  17079