Theorem vex 2636

Description: All setvar variables are sets (see isset 2639). 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 1641	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2635	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2205	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 145	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 1445  Vcvv 2633

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-v 2635

This theorem is referenced by:  elv  2637  elvd  2638  isset  2639  eqvisset  2643  ralv  2650  rexv  2651  reuv  2652  rmov  2653  rabab  2654  sbhypf  2682  ceqex  2758  ralab  2789  rexab  2791  mo2icl  2808  reu8  2825  csbvarg  2972  csbiebg  2984  sbcnestgf  2993  sbnfc2  3002  ddifnel  3146  ddifstab  3147  csbing  3222  unssdif  3250  unssin  3254  inssun  3255  invdif  3257  vn0  3312  vn0m  3313  eqv  3321  abvor0dc  3325  sbss  3410  selpw  3456  elpwg  3457  velsn  3483  vsnid  3496  exsnrex  3505  dftp2  3511  prmg  3583  prnzg  3586  snssg  3595  difprsnss  3597  sneqrg  3628  preq12bg  3639  pwprss  3671  pwtpss  3672  pwv  3674  unipr  3689  uniprg  3690  unisng  3692  elintg  3718  elintrabg  3723  intss1  3725  ssint  3726  intmin  3730  intss  3731  intssunim  3732  intmin4  3738  intab  3739  intun  3741  intpr  3742  intprg  3743  uniintsnr  3746  iinconstm  3761  iuniin  3762  iinss1  3764  dfiin2g  3785  dfiunv2  3788  ssiinf  3801  iinss  3803  iinss2  3804  0iin  3810  iinab  3813  iundif2ss  3817  iindif2m  3819  iinin2m  3820  iinuniss  3833  sspwuni  3835  pwpwab  3838  iinpw  3841  iunpwss  3842  brab1  3912  csbopabg  3938  mptv  3957  trint  3973  vnex  3991  inex1g  3996  ssexg  3999  inteximm  4006  inuni  4012  repizf2  4018  axpweq  4027  bnd2  4029  pwuni  4048  exmidundif  4058  exmidundifim  4059  zfpair2  4061  rext  4066  sspwb  4067  unipw  4068  ssextss  4071  euabex  4076  mss  4077  exss  4078  opth  4088  opthg  4089  copsexg  4095  copsex4g  4098  moop2  4102  euotd  4105  opabid  4108  elopab  4109  opelopabsbALT  4110  opelopabsb  4111  opabm  4131  pwin  4133  pwunss  4134  epelg  4141  epel  4143  pofun  4163  epse  4193  tron  4233  sucel  4261  suctr  4272  vuniex  4289  uniexg  4290  unexb  4292  snnex  4298  pwnex  4299  uniuni  4301  eusvnf  4303  eusvnfb  4304  iunpw  4330  unon  4356  ordunisuc2r  4359  ordtri2or2exmidlem  4370  onsucelsucexmidlem  4373  ordsucunielexmid  4375  elirr  4385  en2lp  4398  dtruex  4403  onintexmid  4416  reg3exmidlemwe  4422  dcextest  4424  finds  4443  finds2  4444  elnn  4448  limom  4456  0nelxp  4495  opelxp  4497  opeliunxp  4522  elvv  4529  elvvv  4530  elvvuni  4531  xpsspw  4579  relopabi  4593  opabid2  4598  difopab  4600  xpiindim  4604  raliunxp  4608  rexiunxp  4609  ralxpf  4613  rexxpf  4614  relop  4617  cnvco  4652  dfrn2  4655  dfdm4  4659  dmss  4666  dmin  4675  dmiun  4676  dmuni  4677  dm0  4681  dmi  4682  reldm0  4685  elreldm  4693  elrnmpt1  4718  dmrnssfld  4728  dmcoss  4734  dmcosseq  4736  opelresg  4752  resieq  4755  dmres  4766  elres  4781  relssres  4783  resopab  4789  resiexg  4790  iss  4791  dfres2  4797  dfima2  4809  imadmrn  4817  imai  4821  csbima12g  4826  elimasng  4833  args  4834  epini  4836  iniseg  4837  dfse2  4838  exse2  4839  cotr  4846  issref  4847  cnvsym  4848  intasym  4849  asymref  4850  intirr  4851  brcodir  4852  codir  4853  qfto  4854  poirr2  4857  cnvopab  4866  cnv0  4868  cnvi  4869  cnvdif  4871  rniun  4875  dminss  4879  imainss  4880  inimasn  4882  xpmlem  4885  dmxpss  4895  rnxpid  4899  ssrnres  4907  rninxp  4908  dminxp  4909  cnvcnv3  4914  dfrel2  4915  dmsnm  4930  dmsnopg  4936  cnvcnvsn  4941  dmsnsnsng  4942  cnvsng  4950  elxp4  4952  elxp5  4953  cnvresima  4954  dfco2  4964  dfco2a  4965  cores  4968  resco  4969  imaco  4970  rnco  4971  coiun  4974  co02  4978  coi1  4980  coass  4983  relssdmrn  4985  unielrel  4992  ressn  5005  cnviinm  5006  cnvpom  5007  cnvsom  5008  uniabio  5024  iotaval  5025  iotass  5031  sniota  5041  csbiotag  5042  dffun2  5059  dffun7  5076  dffun8  5077  dffun9  5078  funopg  5082  funssres  5090  funun  5092  funcnvsn  5093  funinsn  5097  funcnv2  5108  funcnv  5109  funcnv3  5110  funcnveq  5111  fun2cnv  5112  funcnvuni  5117  imadif  5128  funimaexglem  5131  isarep1  5134  2elresin  5159  fnres  5164  fcnvres  5229  fconstg  5242  fun11iun  5309  f1osng  5329  dffv3g  5336  fvssunirng  5355  sefvex  5361  fv3  5363  fvres  5364  nfunsn  5373  funimass4  5390  ssimaexg  5401  dmfco  5407  fvopab6  5435  fndmdif  5443  fvelrn  5469  dffo4  5486  f1ompt  5489  fmptco  5503  fsn  5508  fsng  5509  dfmpt  5513  dfmptg  5515  fnressn  5522  fressnfv  5523  fvsng  5532  resfunexg  5557  funfvima3  5567  idref  5574  abrexco  5576  imaiun  5577  dff13  5585  foeqcnvco  5607  f1eqcocnv  5608  fliftcnv  5612  isocnv2  5629  isoini  5635  isose  5638  riotav  5651  csbriotag  5658  acexmidlem2  5687  oprabid  5719  csbov123g  5725  0neqopab  5732  brabvv  5733  dfoprab2  5734  rnoprab  5769  eloprabga  5773  mpt2v  5776  f1opw  5889  opabex3d  5930  opabex3  5931  ofmres  5945  op1stg  5959  op2ndg  5960  1stval2  5964  2ndval2  5965  fo1st  5966  fo2nd  5967  f1stres  5968  f2ndres  5969  fo1stresm  5970  fo2ndresm  5971  xp1st  5974  xp2nd  5975  releldm2  5993  reldm  5994  sbcopeq1a  5995  csbopeq1a  5996  dfoprab3  5999  eloprabi  6004  mpt2mptsx  6005  dmmpt2ssx  6007  fmpt2x  6008  mpt2fvex  6011  mpt2exxg  6015  fmpt2co  6019  df1st2  6022  df2nd2  6023  1stconst  6024  2ndconst  6025  dfmpt2  6026  fo2ndf  6030  f1o2ndf1  6031  xporderlem  6034  cnvoprab  6037  f1od2  6038  brtpos2  6054  reldmtpos  6056  dmtpos  6059  rntpos  6060  ovtposg  6062  dftpos3  6065  dftpos4  6066  tpostpos  6067  tpossym  6079  tfrlem3  6114  tfrlem5  6117  tfrlem8  6121  tfrlemisucfn  6127  tfrlemisucaccv  6128  tfrlemibxssdm  6130  tfrlemibfn  6131  tfrlemibex  6132  tfrlemi14d  6136  tfrexlem  6137  tfr1onlem3  6141  tfr1onlemsucaccv  6144  tfr1onlembxssdm  6146  tfr1onlembfn  6147  tfr1onlemres  6152  tfri1dALT  6154  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllembfn  6160  tfrcllemres  6165  tfrcl  6167  rdgtfr  6177  rdgruledefgg  6178  rdgivallem  6184  rdgon  6189  rdg0g  6191  frec0g  6200  frecabex  6201  frecabcl  6202  frectfr  6203  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecrdg  6211  oafnex  6245  sucinc  6246  fnoa  6248  oaexg  6249  omfnex  6250  fnom  6251  omexg  6252  fnoei  6253  oeiexg  6254  oeiv  6257  oacl  6261  omcl  6262  oeicl  6263  oav2  6264  nnsucelsuc  6292  nnsucuniel  6296  ercnv  6353  iserd  6358  eqerlem  6363  eqer  6364  ecdmn0m  6374  erth  6376  qsss  6391  ecid  6395  ecidg  6396  qsid  6397  iinerm  6404  qsel  6409  erovlem  6424  ecopovsym  6428  ecopover  6430  th3qlem2  6435  mapprc  6449  fnmap  6452  fnpm  6453  mapdm0  6460  mapval2  6475  mapsn  6487  mapsncnv  6492  mapsnf1o2  6493  ixpconstg  6504  ixpprc  6516  ixpin  6520  ixpiinm  6521  ixpssmap2g  6524  ixpssmapg  6525  elixpsn  6532  ixpsnf1o  6533  bren  6544  brdomg  6545  domen  6548  domeng  6549  idssen  6574  ener  6576  domtr  6582  ensn1g  6594  en1  6596  en1bg  6597  fundmen  6603  fundmeng  6604  mapsnen  6608  fiprc  6612  unen  6613  xpsnen  6617  xpsneng  6618  xpcomco  6622  xpcomeng  6624  xpassen  6626  xpdom2  6627  xpdom2g  6628  xpf1o  6640  mapen  6642  mapxpen  6644  xpmapenlem  6645  ssenen  6647  phplem4  6651  phplem3g  6652  nneneq  6653  php5  6654  phpm  6661  findcard  6684  findcard2  6685  findcard2s  6686  isinfinf  6693  ac6sfi  6694  exmidpw  6704  unfidisj  6712  fiintim  6719  xpfi  6720  fisseneq  6722  ssfirab  6723  snexxph  6739  fidcenumlemr  6744  sbthlemi10  6755  isbth  6756  cnvinfex  6793  eqinfti  6795  infvalti  6797  infglbti  6800  infmoti  6803  ordiso2  6808  djuf1olem  6825  djuun  6840  djuss  6841  ctm  6871  finomni  6883  exmidomniim  6884  exmidomni  6885  fodjuomnilemdc  6887  pm54.43  6915  exmidfodomrlemim  6924  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  indpi  6998  dfplpq2  7010  enq0sym  7088  enq0ref  7089  enq0tr  7090  nqnq0pi  7094  nqnq0  7097  mulnnnq0  7106  nqprm  7198  nqprrnd  7199  nqprdisj  7200  nqprloc  7201  nqprl  7207  nqpru  7208  addnqprlemrl  7213  addnqprlemru  7214  addnqprlemfl  7215  addnqprlemfu  7216  mulnqprlemrl  7229  mulnqprlemru  7230  mulnqprlemfl  7231  mulnqprlemfu  7232  ltnqpr  7249  ltnqpri  7250  archpr  7299  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  cauappcvgprlem2  7316  caucvgprlemladdfu  7333  caucvgprlem2  7336  caucvgprprlemopu  7355  ltresr  7473  peano1nnnn  7486  peano2nnnn  7487  axcnre  7513  axpre-apti  7517  renfdisj  7643  dfinfre  8514  1nn  8531  peano2nn  8532  indstr  9180  cnref1o  9232  ioof  9537  fzpr  9640  frec2uzrand  9961  frec2uzf1od  9962  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  frecfzennn  9982  ser3le  10068  hashinfom  10301  hashunlem  10327  hashun  10328  hashxp  10349  hashfacen  10356  zfz1isolem1  10360  zfz1iso  10361  shftfvalg  10367  ovshftex  10368  shftfibg  10369  shftfval  10370  shftfib  10372  shftfn  10373  2shfti  10380  shftvalg  10385  shftval4g  10386  maxabslemval  10756  fimaxre2  10773  xrmaxiflemval  10793  fclim  10837  climshft  10847  zsumdc  10927  fsum3  10930  fsum2dlemstep  10977  fsumcnv  10980  fisumcom2  10981  fisum0diag2  10990  fsumconst  10997  modfsummodlemstep  11000  fsumabs  11008  fsumrelem  11014  fsumiun  11020  algrf  11454  qredeu  11506  isprm2  11526  prmind2  11529  slotslfn  11669  restfn  11808  elrest  11811  bastg  11913  distop  11937  topnex  11938  epttop  11942  tgrest  12021  resttopon  12023  restco  12026  cnrest2  12087  cnptopresti  12089  cnptoprest  12090  cnptoprest2  12091  xmetec  12223  metrest  12292  bdcvv  12465  bdsnss  12481  bdop  12483  bj-vprc  12504  bdinex1g  12509  bdssexg  12512  bj-inex  12515  bj-zfpair2  12518  bj-uniexg  12526  bdunexb  12528  bj-unexg  12529  bj-indint  12543  bj-ssom  12548  bj-om  12549  bj-2inf  12550  bj-bdfindis  12559  bj-nn0suc0  12562  bj-nnelirr  12565  bj-inf2vnlem1  12582  bj-inf2vnlem2  12583  bj-omex2  12589  bj-nn0sucALT  12590  bj-findis  12591  ss1oel2o  12603  nninfsellemeq  12620  exmidsbthrlem  12626