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  4179  csbopabg  4210  mptv  4230  trint  4246  vnex  4266  inex1g  4271  ssexg  4274  inteximm  4287  inuni  4293  repizf2  4301  axpweq  4310  bnd2  4312  pwuni  4331  exmidundif  4345  exmidundifim  4346  zfpair2  4349  rext  4357  sspwb  4358  unipw  4359  ssextss  4362  euabex  4367  mss  4368  exss  4369  opth  4379  opthg  4380  copsexg  4386  copsex4g  4389  moop2  4394  euotd  4397  opabid  4400  elopab  4402  opelopabsbALT  4403  opelopabsb  4404  opabm  4425  pwin  4429  pwunss  4430  epelg  4437  epel  4439  pofun  4459  epse  4489  tron  4529  sucel  4557  suctr  4568  vuniex  4586  uniexg  4587  unexb  4590  snnex  4596  pwnex  4597  uniuni  4599  eusvnf  4601  eusvnfb  4602  iunpw  4628  unon  4660  ordunisuc2r  4663  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsucunielexmid  4680  elirr  4690  en2lp  4703  dtruex  4708  onintexmid  4722  reg3exmidlemwe  4728  dcextest  4730  finds  4749  finds2  4750  elomssom  4754  limom  4763  0nelxp  4804  opelxp  4806  opeliunxp  4832  elvv  4839  elvvv  4840  elvvuni  4841  xpsspw  4889  relopabiv  4905  relopabi  4907  opabid2  4913  difopab  4915  xpiindim  4919  raliunxp  4923  rexiunxp  4924  ralxpf  4928  rexxpf  4929  relop  4932  cnvco  4967  dfrn2  4970  dfdm4  4975  dmss  4982  dmin  4991  dmiun  4992  dmuni  4993  dm0  4997  dmi  4998  reldm0  5001  reldmm  5002  elreldm  5010  elrnmpt1  5035  dmrnssfld  5047  dmcoss  5054  dmcosseq  5056  opelresg  5072  resieq  5075  dmres  5086  elres  5101  relssres  5103  resopab  5110  resiexg  5111  iss  5112  dfres2  5118  restidsing  5122  dfima2  5131  imadmrn  5139  imai  5146  csbima12g  5151  elimasng  5158  args  5159  epini  5161  iniseg  5162  dfse2  5163  exse2  5164  cotr  5172  issref  5173  cnvsym  5174  intasym  5175  asymref  5176  intirr  5177  brcodir  5178  codir  5179  qfto  5180  poirr2  5183  cnvopab  5192  cnv0  5194  cnvi  5195  cnvdif  5197  rniun  5201  dminss  5205  imainss  5206  inimasn  5208  xpmlem  5211  dmxpss  5221  rnxpid  5225  ssrnres  5233  rninxp  5234  dminxp  5235  cnvcnv3  5240  dfrel2  5241  dmsnm  5256  dmsnopg  5262  cnvcnvsn  5267  dmsnsnsng  5268  cnvsng  5276  elxp4  5278  elxp5  5279  cnvresima  5280  dfco2  5290  dfco2a  5291  cores  5294  resco  5295  imaco  5296  rnco  5297  coiun  5300  co02  5304  coi1  5306  coass  5309  relssdmrn  5311  unielrel  5318  ressn  5331  cnviinm  5332  cnvpom  5333  cnvsom  5334  uniabio  5351  iotaval  5352  iotass  5358  sniota  5371  csbiotag  5373  dffun2  5390  dffun7  5407  dffun8  5408  dffun9  5409  funopg  5414  funssres  5423  funun  5425  funcnvsn  5429  funinsn  5433  funcnv2  5444  funcnv  5445  funcnv3  5446  funcnveq  5447  fun2cnv  5448  funcnvuni  5453  imadif  5464  funimaexglem  5467  isarep1  5470  2elresin  5497  fnres  5503  fcnvres  5578  fconstg  5592  fun11iun  5663  f1osng  5685  dffv3g  5694  fvssunirng  5713  sefvex  5719  fv3  5721  fvres  5722  nfunsn  5736  funimass4  5756  ssimaexg  5768  dmfco  5776  fvopab6  5808  fndmdif  5817  fvelrn  5842  dffo4  5859  f1ompt  5862  fmptco  5877  fsn  5883  fsng  5884  fsn2g  5886  dfmpt  5889  dfmptg  5891  funopsn  5894  funop  5895  funopdmsn  5898  fnressn  5904  fressnfv  5905  fvsng  5914  resfunexg  5939  funfvima3  5955  idref  5965  abrexco  5968  imaiun  5969  dff13  5977  foeqcnvco  5999  f1eqcocnv  6000  fliftcnv  6004  isocnv2  6021  isoini  6027  isose  6030  riotav  6047  csbriotag  6055  acexmidlem2  6085  oprabid  6120  csbov123g  6127  0neqopab  6136  brabvv  6137  dfoprab2  6138  rnoprab  6174  eloprabga  6178  mpov  6181  f1opw  6300  opabex3d  6354  opabex3  6355  abrexss  6362  ofmres  6373  uchoice  6375  op1stg  6388  op2ndg  6389  1stval2  6393  2ndval2  6394  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  fo1stresm  6399  fo2ndresm  6400  xp1st  6403  xp2nd  6404  releldm2  6423  reldm  6424  sbcopeq1a  6425  csbopeq1a  6426  dfoprab3  6429  opabn1stprc  6433  eloprabi  6436  mpomptsx  6437  dmmpossx  6439  fmpox  6440  mpofvex  6445  mpoexxg  6450  fmpoco  6456  df1st2  6459  df2nd2  6460  1stconst  6461  2ndconst  6462  dfmpo  6463  fo2ndf  6467  f1o2ndf1  6468  xporderlem  6471  cnvoprab  6474  f1od2  6475  suppval1  6483  cnvimadfsn  6489  suppimacnvfn  6490  brtpos2  6526  reldmtpos  6528  dmtpos  6531  rntpos  6532  ovtposg  6534  dftpos3  6537  dftpos4  6538  tpostpos  6539  tpossym  6551  tfrlem3  6586  tfrlem5  6589  tfrlem8  6593  tfrlemisucfn  6599  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemibex  6604  tfrlemi14d  6608  tfrexlem  6609  tfr1onlem3  6613  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  tfrcl  6639  rdgtfr  6649  rdgruledefgg  6650  rdgivallem  6656  rdgon  6661  rdg0g  6663  frec0g  6672  frecabex  6673  frecabcl  6674  frectfr  6675  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  oafnex  6721  sucinc  6722  fnoa  6724  oaexg  6725  omfnex  6726  fnom  6727  omexg  6728  fnoei  6729  oeiexg  6730  oeiv  6733  oacl  6737  omcl  6738  oeicl  6739  oav2  6740  nnsucelsuc  6768  nnsucuniel  6772  ercnv  6832  iserd  6837  eqerlem  6842  eqer  6843  ecdmn0m  6855  erth  6857  qsss  6872  ecid  6876  ecidg  6877  qsid  6878  iinerm  6885  qsel  6890  erovlem  6905  ecopovsym  6909  ecopover  6911  th3qlem2  6916  mapprc  6930  fnmap  6933  fnpm  6934  mapdm0  6941  mapfset  6949  mapfoss  6951  fsetsspwxp  6952  fsetdmprc0  6954  mapval2  6963  mapsnd  6975  mapsn  6977  mapsncnv  6982  mapsnf1o2  6983  ixpconstg  6994  ixpprc  7006  ixpin  7010  ixpiinm  7011  ixpssmap2g  7014  ixpssmapg  7015  elixpsn  7022  ixpsnf1o  7023  bren  7035  brdomg  7037  domen  7040  domeng  7041  idssen  7068  domssr  7069  ener  7071  domtr  7077  ensn1g  7089  en1  7091  en1bg  7092  fundmen  7099  fundmeng  7100  mapsnend  7104  mapsnen  7105  fiprc  7109  unen  7110  rex2dom  7115  en2m  7118  dom1o  7121  xpsnen  7124  xpsneng  7125  xpcomco  7129  xpcomeng  7131  xpassen  7133  xpdom2  7134  xpdom2g  7135  pw2f1odc  7140  xpf1o  7149  mapen  7151  mapxpen  7153  xpmapenlem  7154  mapunen  7156  ssenen  7157  phplem4  7161  phplem3g  7162  nneneq  7163  php5  7164  phpm  7172  findcard  7197  findcard2  7198  findcard2s  7199  isinfinf  7206  ac6sfi  7207  exmidpw  7220  exmidpweq  7221  exmidpw2en  7224  unfidisj  7234  fiintim  7243  xpfi  7244  fisseneq  7247  ssfirab  7249  mapfi  7266  snexxph  7273  fidcenumlemr  7278  sbthlemi10  7289  isbth  7290  ssfii  7314  fi0  7315  fiss  7317  f1setfi  7323  cnvinfex  7365  eqinfti  7367  infvalti  7369  infglbti  7372  infmoti  7375  ordiso2  7382  djuf1olem  7400  djuss  7417  ctm  7456  ctssdccl  7458  ctssdclemr  7459  finomni  7487  exmidomni  7489  fodjuomnilemdc  7491  nninfwlpoimlemginf  7523  pm54.43  7543  pr2cv1  7548  exmidfodomrlemim  7560  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  finacn  7567  acfun  7570  ccfunen  7637  cc2lem  7639  cc3  7641  acnccim  7645  indpi  7716  dfplpq2  7728  enq0sym  7806  enq0ref  7807  enq0tr  7808  nqnq0pi  7812  nqnq0  7815  mulnnnq0  7824  nqprm  7916  nqprrnd  7917  nqprdisj  7918  nqprloc  7919  nqprl  7925  nqpru  7926  addnqprlemrl  7931  addnqprlemru  7932  addnqprlemfl  7933  addnqprlemfu  7934  mulnqprlemrl  7947  mulnqprlemru  7948  mulnqprlemfl  7949  mulnqprlemfu  7950  ltnqpr  7967  ltnqpri  7968  archpr  8017  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlem2  8034  caucvgprlemladdfu  8051  caucvgprlem2  8054  caucvgprprlemopu  8073  suplocexprlemmu  8092  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  cnm  8206  ltresr  8213  peano1nnnn  8226  peano2nnnn  8227  axcnre  8255  axpre-apti  8259  renfdisj  8392  dfinfre  9295  1nn  9325  peano2nn  9326  indstr  10010  cnref1o  10069  ioof  10391  fzpr  10502  frec2uzrand  10864  frec2uzf1od  10865  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  frecfzennn  10885  seqp1g  10925  seqclg  10931  seqf1og  10980  seqfeq4g  10990  ser3le  10996  hashinfom  11240  hashunlem  11267  hashun  11268  hashxp  11290  hashmap  11291  hashfibclem  11305  hashfacen  11307  hashf1lem1  11308  hashf1lem2  11309  hashf1  11310  zfz1isolem1  11315  zfz1iso  11316  fundm2domnop0  11323  wrdexb  11339  fnpfx  11472  cats1un  11516  wrdind  11517  wrd2ind  11518  shftfvalg  11606  ovshftex  11607  shftfibg  11608  shftfval  11609  shftfib  11611  shftfn  11612  2shfti  11619  shftvalg  11624  shftval4g  11625  maxabslemval  11998  fimaxre2  12017  xrmaxiflemval  12042  fclim  12086  climshft  12096  zsumdc  12177  fsum3  12180  fsum2dlemstep  12227  fsumcnv  12230  fisumcom2  12231  fisum0diag2  12240  fsumconst  12247  modfsummodlemstep  12250  fsumabs  12258  fsumrelem  12264  fsumiun  12270  ntrivcvgap  12341  fprod2dlemstep  12415  fprodcnv  12418  fprodcom2fi  12419  fprodmodd  12434  nninfct  12844  algrf  12849  qredeu  12901  isprm2  12921  prmind2  12924  4sqlemafi  13204  4sqlem12  13211  ballotfilemcdc  13282  ballotfilemsf1o  13316  ballotfilem7  13338  ennnfonelemex  13364  ennnfonelemrn  13369  exmidunben  13376  ctinfom  13378  ctinf  13380  qnnen  13381  enctlem  13382  ctiunctlemfo  13389  slotslfn  13437  setscomd  13452  restfn  13657  elrest  13660  ptex  13678  prdsvallem  13681  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfnlemg  13695  fnpr2ob  13721  ismgm  13737  plusffng  13745  fn0g  13755  fngzsum  13768  gzsumsplit1r  13775  issgrp  13778  ismnddef  13791  gzsumcl  13864  mulgnngzsum  13990  subgintm  14061  releqgg  14083  eqgex  14084  eqgfval  14085  eqgval  14086  isghm  14106  gsumvalfi  14243  gsumsnfdcmn  14258  gsum2dfilem1  14272  gsum2dfilem2  14273  gsum2d2fi  14275  gsumcom2fi  14276  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  fnmgp  14327  isrng  14341  isring  14412  ringn0  14473  opprrngbg  14493  opprsubgg  14500  opprunitd  14527  dfrhm2  14571  rhmex  14574  opprsubrngg  14629  subrngintm  14630  subrngpropd  14634  subrgpropd  14671  isdomn  14688  opprdomnbg  14693  scaffng  14756  rmodislmodlem  14797  rmodislmod  14798  lssex  14801  lsssn0  14817  lss1d  14830  lssintclm  14831  ellspsn  14864  rlmfn  14900  isridl  14951  blfn  14998  mopnset  14999  metuex  15002  znval  15081  znleval  15098  psrval  15162  fnpsr  15163  mplvalcoe  15218  fnmpl  15221  bastg  15299  distop  15323  topnex  15324  epttop  15328  tgrest  15407  resttopon  15409  restco  15412  cnrest2  15474  cnptopresti  15476  cnptoprest  15477  cnptoprest2  15478  txuni2  15494  txbas  15496  eltx  15497  txcnp  15509  txcnmpt  15511  txrest  15514  txdis1cn  15516  txlm  15517  cnmpt1st  15526  cnmpt2nd  15527  txhmeo  15557  txswaphmeolem  15558  xmetec  15675  metrest  15744  reldvg  15917  dvfgg  15926  dvcj  15947  dvmptfsum  15963  elply2  15973  pilem3  16022  prmorcht  16294  lgsquadlem1  16413  lgsquadlem2  16414  upgrex  16561  upgr1een  16582  umgredg  16603  umgredgnlp  16610  usgredgreu  16674  uspgredg2vtxeu  16676  ushgredgedg  16684  ushgredgedgloop  16686  griedg0ssusgr  16709  uhgrspansubgrlem  16734  upgrspanop  16741  umgrspanop  16742  usgrspanop  16743  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlk1walkdom  16817  eulerpathum  16939  depindlem1  16964  bdcvv  17100  bdsnss  17116  bdop  17118  bj-vprc  17139  bdinex1g  17144  bdssexg  17147  bj-inex  17150  bj-zfpair2  17153  bj-uniexg  17161  bdunexb  17163  bj-unexg  17164  bj-indint  17174  bj-ssom  17179  bj-om  17180  bj-2inf  17181  bj-bdfindis  17190  bj-nn0suc0  17193  bj-nnelirr  17196  bj-inf2vnlem1  17213  bj-inf2vnlem2  17214  bj-omex2  17220  bj-nn0sucALT  17221  bj-findis  17222  ss1oel2o  17234  domomsubct  17248  pw1nct  17250  nninfsellemeq  17275  exmidsbthrlem  17285