Theorem vex 2560

Description: All setvar variables are sets (see isset 2561). 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 1589	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2559	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2148	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 134	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 1393  Vcvv 2557

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559

This theorem is referenced by:  isset  2561  eqvisset  2565  ralv  2571  rexv  2572  reuv  2573  rmov  2574  rabab  2575  sbhypf  2603  ceqex  2671  ralab  2701  rexab  2703  mo2icl  2720  reu8  2737  csbvarg  2877  csbiebg  2889  sbcnestgf  2897  sbnfc2  2906  ddifnel  3075  csbing  3144  unssdif  3172  unssin  3176  inssun  3177  invdif  3179  vn0  3231  vn0m  3232  eqv  3240  abvor0dc  3242  sbss  3329  selpw  3366  elpwg  3367  velsn  3392  vsnid  3403  exsnrex  3413  dftp2  3419  prmg  3489  prnzg  3492  snssg  3500  difprsnss  3502  sneqrg  3533  preq12bg  3544  pwprss  3576  pwtpss  3577  pwv  3579  unipr  3594  uniprg  3595  unisng  3597  elintg  3623  elintrabg  3628  intss1  3630  ssint  3631  intmin  3635  intss  3636  intssunim  3637  intmin4  3643  intab  3644  intun  3646  intpr  3647  intprg  3648  uniintsnr  3651  iinconstm  3666  iuniin  3667  iinss1  3669  dfiin2g  3690  dfiunv2  3693  ssiinf  3706  iinss  3708  iinss2  3709  0iin  3715  iinab  3718  iundif2ss  3722  iindif2m  3724  iinin2m  3725  iinuniss  3737  sspwuni  3739  iinpw  3742  iunpwss  3743  brab1  3809  csbopabg  3835  mptv  3853  trint  3869  trintssm  3870  vprc  3888  inex1g  3893  ssexg  3896  inteximm  3903  inuni  3909  repizf2  3915  axpweq  3924  bnd2  3926  pwexg  3933  pwuni  3943  zfpair2  3945  rext  3951  sspwb  3952  unipw  3953  ssextss  3956  euabex  3961  mss  3962  exss  3963  opth  3974  opthg  3975  copsexg  3981  copsex4g  3984  moop2  3988  euotd  3991  opabid  3994  elopab  3995  opelopabsbALT  3996  opelopabsb  3997  opabm  4017  pwin  4019  pwunss  4020  epelg  4027  epel  4029  pofun  4049  epse  4079  tron  4119  sucel  4147  suctr  4158  uniexg  4175  unexb  4177  snnex  4181  uniuni  4183  eusvnf  4185  eusvnfb  4186  iunpw  4211  unon  4237  ordunisuc2r  4240  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsucunielexmid  4256  elirr  4266  en2lp  4278  dtruex  4283  onintexmid  4297  reg3exmidlemwe  4303  finds  4323  finds2  4324  elnn  4328  limom  4336  0nelxp  4372  opelxp  4374  opeliunxp  4395  elvv  4402  elvvv  4403  elvvuni  4404  xpsspw  4450  relopabi  4463  opabid2  4467  difopab  4469  xpiindim  4473  raliunxp  4477  rexiunxp  4478  ralxpf  4482  rexxpf  4483  relop  4486  cnvco  4520  dfrn2  4523  dfdm4  4527  dmss  4534  dmin  4543  dmiun  4544  dmuni  4545  dm0  4549  dmi  4550  reldm0  4553  elreldm  4560  elrnmpt1  4585  dmrnssfld  4595  dmcoss  4601  dmcosseq  4603  opelresg  4619  resieq  4622  dmres  4632  elres  4646  relssres  4648  resopab  4652  resiexg  4653  iss  4654  dfres2  4658  dfima2  4670  imadmrn  4678  imai  4681  csbima12g  4686  elimasng  4693  args  4694  epini  4696  iniseg  4697  dfse2  4698  exse2  4699  cotr  4706  issref  4707  cnvsym  4708  intasym  4709  asymref  4710  intirr  4711  brcodir  4712  codir  4713  qfto  4714  poirr2  4717  cnvopab  4726  cnv0  4727  cnvi  4728  cnvdif  4730  rniun  4734  dminss  4738  imainss  4739  inimasn  4741  xpmlem  4744  dmxpss  4753  rnxpid  4755  ssrnres  4763  rninxp  4764  dminxp  4765  cnvcnv3  4770  dfrel2  4771  dmsnm  4786  dmsnopg  4792  cnvcnvsn  4797  dmsnsnsng  4798  cnvsng  4806  elxp4  4808  elxp5  4809  cnvresima  4810  dfco2  4820  dfco2a  4821  cores  4824  resco  4825  imaco  4826  rnco  4827  coiun  4830  co02  4834  coi1  4836  coass  4839  relssdmrn  4841  unielrel  4845  ressn  4858  cnviinm  4859  cnvpom  4860  cnvsom  4861  uniabio  4877  iotaval  4878  iotass  4884  sniota  4894  csbiotag  4895  dffun2  4912  dffun7  4928  dffun8  4929  dffun9  4930  funopg  4934  funssres  4942  funun  4944  funcnvsn  4945  funcnv2  4959  funcnv  4960  funcnv3  4961  funcnveq  4962  fun2cnv  4963  funcnvuni  4968  imadif  4979  funimaexglem  4982  isarep1  4985  2elresin  5010  fnres  5015  fcnvres  5073  fconstg  5083  fun11iun  5147  f1osng  5167  dffv3g  5174  fvssunirng  5190  sefvex  5196  fv3  5197  fvres  5198  nfunsn  5207  funimass4  5224  ssimaexg  5235  dmfco  5241  fvopab6  5264  fndmdif  5272  fvelrn  5298  dffo4  5315  f1ompt  5320  fmptco  5330  fsn  5335  fsng  5336  dfmpt  5340  dfmptg  5342  fnressn  5349  fressnfv  5350  fvsng  5359  resfunexg  5382  funfvima3  5392  idref  5396  abrexco  5398  imaiun  5399  dff13  5407  foeqcnvco  5430  f1eqcocnv  5431  fliftcnv  5435  isocnv2  5452  isoini  5457  isose  5460  riotav  5473  csbriotag  5480  acexmidlem2  5509  oprabid  5537  csbov123g  5543  0neqopab  5550  brabvv  5551  dfoprab2  5552  rnoprab  5587  eloprabga  5591  mpt2v  5594  f1opw  5707  opabex3d  5748  opabex3  5749  ofmres  5763  op1stg  5777  op2ndg  5778  1stval2  5782  2ndval2  5783  fo1st  5784  fo2nd  5785  f1stres  5786  f2ndres  5787  fo1stresm  5788  fo2ndresm  5789  xp1st  5792  xp2nd  5793  releldm2  5811  reldm  5812  sbcopeq1a  5813  csbopeq1a  5814  dfoprab3  5817  eloprabi  5822  mpt2mptsx  5823  dmmpt2ssx  5825  fmpt2x  5826  mpt2fvex  5829  mpt2exxg  5833  fmpt2co  5837  df1st2  5840  df2nd2  5841  1stconst  5842  2ndconst  5843  dfmpt2  5844  fo2ndf  5848  f1o2ndf1  5849  xporderlem  5852  brtpos2  5866  reldmtpos  5868  dmtpos  5871  rntpos  5872  ovtposg  5874  dftpos3  5877  dftpos4  5878  tpostpos  5879  tpossym  5891  tfrlem3  5926  tfrlem5  5930  tfrlem8  5934  tfrlemisucfn  5938  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemibex  5943  tfrlemi14d  5947  tfrexlem  5948  rdgtfr  5961  rdgruledefgg  5962  rdgivallem  5968  rdgon  5973  rdg0g  5975  frec0g  5983  frecabex  5984  frectfr  5985  frecsuclem3  5990  frecrdg  5992  oafnex  6024  sucinc  6025  fnoa  6027  oaexg  6028  omfnex  6029  fnom  6030  omexg  6031  fnoei  6032  oeiexg  6033  oeiv  6036  oacl  6040  omcl  6041  oeicl  6042  oav2  6043  nnsucelsuc  6070  ercnv  6127  iserd  6132  eqerlem  6137  eqer  6138  ecdmn0m  6148  erth  6150  qsss  6165  ecid  6169  ecidg  6170  qsid  6171  iinerm  6178  qsel  6183  erovlem  6198  ecopovsym  6202  ecopover  6204  th3qlem2  6209  bren  6228  brdomg  6229  domen  6232  domeng  6233  idssen  6257  ener  6259  domtr  6265  ensn1g  6277  en1  6279  en1bg  6280  fundmen  6286  fundmeng  6287  fiprc  6292  unen  6293  xpsnen  6295  xpsneng  6296  xpcomco  6300  xpcomeng  6302  xpassen  6304  xpdom2  6305  xpdom2g  6306  phplem4  6318  phplem3g  6319  nneneq  6320  php5  6321  phpm  6327  findcard  6345  findcard2  6346  findcard2s  6347  ac6sfi  6352  ordiso2  6357  indpi  6440  dfplpq2  6452  enq0sym  6530  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nqnq0  6539  mulnnnq0  6548  nqprm  6640  nqprrnd  6641  nqprdisj  6642  nqprloc  6643  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  ltnqpr  6691  ltnqpri  6692  archpr  6741  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlem2  6758  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemopu  6797  ltresr  6915  peano1nnnn  6928  peano2nnnn  6929  axcnre  6955  axpre-apti  6959  renfdisj  7079  1nn  7925  peano2nn  7926  indstr  8536  cnref1o  8582  ioof  8840  fzpr  8939  frec2uzzd  9186  frec2uzsucd  9187  frec2uzrand  9191  frec2uzf1od  9192  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdgfn  9198  frecuzrdgsuc  9201  frecfzennn  9203  serile  9253  shftfvalg  9419  ovshftex  9420  shftfibg  9421  shftfval  9422  shftfib  9424  shftfn  9425  2shfti  9432  shftvalg  9437  shftval4g  9438  fclim  9815  climshft  9825  bdcvv  9977  bdsnss  9993  bdop  9995  bj-vprc  10016  bdinex1g  10021  bdssexg  10024  bj-inex  10027  bj-zfpair2  10030  bj-uniexg  10038  bdunexb  10040  bj-unexg  10041  bj-indint  10055  bj-ssom  10060  bj-om  10061  bj-2inf  10062  bj-bdfindis  10072  bj-nn0suc0  10075  bj-nnelirr  10078  bj-inf2vnlem1  10095  bj-inf2vnlem2  10096  bj-omex2  10102  bj-nn0sucALT  10103  bj-findis  10104