Theorem vex 2604

Description: All setvar variables are sets (see isset 2605). 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 1629	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2603	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2189	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 144	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 1433  Vcvv 2601

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-v 2603

This theorem is referenced by:  isset  2605  eqvisset  2609  ralv  2616  rexv  2617  reuv  2618  rmov  2619  rabab  2620  sbhypf  2648  ceqex  2722  ralab  2752  rexab  2754  mo2icl  2771  reu8  2788  csbvarg  2933  csbiebg  2945  sbcnestgf  2953  sbnfc2  2962  ddifnel  3103  ddifstab  3104  csbing  3173  unssdif  3199  unssin  3203  inssun  3204  invdif  3206  vn0  3258  vn0m  3259  eqv  3267  abvor0dc  3269  sbss  3349  selpw  3389  elpwg  3390  velsn  3415  vsnid  3426  exsnrex  3435  dftp2  3441  prmg  3511  prnzg  3514  snssg  3522  difprsnss  3524  sneqrg  3554  preq12bg  3565  pwprss  3597  pwtpss  3598  pwv  3600  unipr  3615  uniprg  3616  unisng  3618  elintg  3644  elintrabg  3649  intss1  3651  ssint  3652  intmin  3656  intss  3657  intssunim  3658  intmin4  3664  intab  3665  intun  3667  intpr  3668  intprg  3669  uniintsnr  3672  iinconstm  3687  iuniin  3688  iinss1  3690  dfiin2g  3711  dfiunv2  3714  ssiinf  3727  iinss  3729  iinss2  3730  0iin  3736  iinab  3739  iundif2ss  3743  iindif2m  3745  iinin2m  3746  iinuniss  3758  sspwuni  3760  iinpw  3763  iunpwss  3764  brab1  3830  csbopabg  3856  mptv  3874  trint  3890  trintssmOLD  3892  vprc  3909  inex1g  3914  ssexg  3917  inteximm  3924  inuni  3930  repizf2  3936  axpweq  3945  bnd2  3947  pwexg  3954  pwuni  3963  zfpair2  3965  rext  3970  sspwb  3971  unipw  3972  ssextss  3975  euabex  3980  mss  3981  exss  3982  opth  3992  opthg  3993  copsexg  3999  copsex4g  4002  moop2  4006  euotd  4009  opabid  4012  elopab  4013  opelopabsbALT  4014  opelopabsb  4015  opabm  4035  pwin  4037  pwunss  4038  epelg  4045  epel  4047  pofun  4067  epse  4097  tron  4137  sucel  4165  suctr  4176  uniexg  4193  unexb  4195  snnex  4199  uniuni  4201  eusvnf  4203  eusvnfb  4204  iunpw  4229  unon  4255  ordunisuc2r  4258  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  ordsucunielexmid  4274  elirr  4284  en2lp  4297  dtruex  4302  onintexmid  4315  reg3exmidlemwe  4321  finds  4341  finds2  4342  elnn  4346  limom  4354  0nelxp  4390  opelxp  4392  opeliunxp  4413  elvv  4420  elvvv  4421  elvvuni  4422  xpsspw  4468  relopabi  4481  opabid2  4485  difopab  4487  xpiindim  4491  raliunxp  4495  rexiunxp  4496  ralxpf  4500  rexxpf  4501  relop  4504  cnvco  4538  dfrn2  4541  dfdm4  4545  dmss  4552  dmin  4561  dmiun  4562  dmuni  4563  dm0  4567  dmi  4568  reldm0  4571  elreldm  4578  elrnmpt1  4603  dmrnssfld  4613  dmcoss  4619  dmcosseq  4621  opelresg  4637  resieq  4640  dmres  4650  elres  4664  relssres  4666  resopab  4672  resiexg  4673  iss  4674  dfres2  4678  dfima2  4690  imadmrn  4698  imai  4701  csbima12g  4706  elimasng  4713  args  4714  epini  4716  iniseg  4717  dfse2  4718  exse2  4719  cotr  4726  issref  4727  cnvsym  4728  intasym  4729  asymref  4730  intirr  4731  brcodir  4732  codir  4733  qfto  4734  poirr2  4737  cnvopab  4746  cnv0  4747  cnvi  4748  cnvdif  4750  rniun  4754  dminss  4758  imainss  4759  inimasn  4761  xpmlem  4764  dmxpss  4773  rnxpid  4775  ssrnres  4783  rninxp  4784  dminxp  4785  cnvcnv3  4790  dfrel2  4791  dmsnm  4806  dmsnopg  4812  cnvcnvsn  4817  dmsnsnsng  4818  cnvsng  4826  elxp4  4828  elxp5  4829  cnvresima  4830  dfco2  4840  dfco2a  4841  cores  4844  resco  4845  imaco  4846  rnco  4847  coiun  4850  co02  4854  coi1  4856  coass  4859  relssdmrn  4861  unielrel  4865  ressn  4878  cnviinm  4879  cnvpom  4880  cnvsom  4881  uniabio  4897  iotaval  4898  iotass  4904  sniota  4914  csbiotag  4915  dffun2  4932  dffun7  4948  dffun8  4949  dffun9  4950  funopg  4954  funssres  4962  funun  4964  funcnvsn  4965  funcnv2  4979  funcnv  4980  funcnv3  4981  funcnveq  4982  fun2cnv  4983  funcnvuni  4988  imadif  4999  funimaexglem  5002  isarep1  5005  2elresin  5030  fnres  5035  fcnvres  5093  fconstg  5103  fun11iun  5167  f1osng  5187  dffv3g  5194  fvssunirng  5210  sefvex  5216  fv3  5218  fvres  5219  nfunsn  5228  funimass4  5245  ssimaexg  5256  dmfco  5262  fvopab6  5285  fndmdif  5293  fvelrn  5319  dffo4  5336  f1ompt  5341  fmptco  5351  fsn  5356  fsng  5357  dfmpt  5361  dfmptg  5363  fnressn  5370  fressnfv  5371  fvsng  5380  resfunexg  5403  funfvima3  5413  idref  5417  abrexco  5419  imaiun  5420  dff13  5428  foeqcnvco  5450  f1eqcocnv  5451  fliftcnv  5455  isocnv2  5472  isoini  5477  isose  5480  riotav  5493  csbriotag  5500  acexmidlem2  5529  oprabid  5557  csbov123g  5563  0neqopab  5570  brabvv  5571  dfoprab2  5572  rnoprab  5607  eloprabga  5611  mpt2v  5614  f1opw  5727  opabex3d  5768  opabex3  5769  ofmres  5783  op1stg  5797  op2ndg  5798  1stval2  5802  2ndval2  5803  fo1st  5804  fo2nd  5805  f1stres  5806  f2ndres  5807  fo1stresm  5808  fo2ndresm  5809  xp1st  5812  xp2nd  5813  releldm2  5831  reldm  5832  sbcopeq1a  5833  csbopeq1a  5834  dfoprab3  5837  eloprabi  5842  mpt2mptsx  5843  dmmpt2ssx  5845  fmpt2x  5846  mpt2fvex  5849  mpt2exxg  5853  fmpt2co  5857  df1st2  5860  df2nd2  5861  1stconst  5862  2ndconst  5863  dfmpt2  5864  fo2ndf  5868  f1o2ndf1  5869  xporderlem  5872  cnvoprab  5875  f1od2  5876  brtpos2  5889  reldmtpos  5891  dmtpos  5894  rntpos  5895  ovtposg  5897  dftpos3  5900  dftpos4  5901  tpostpos  5902  tpossym  5914  tfrlem3  5949  tfrlem5  5953  tfrlem8  5957  tfrlemisucfn  5961  tfrlemisucaccv  5962  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemibex  5966  tfrlemi14d  5970  tfrexlem  5971  rdgtfr  5984  rdgruledefgg  5985  rdgivallem  5991  rdgon  5996  rdg0g  5998  frec0g  6006  frecabex  6007  frectfr  6008  frecsuclem3  6013  frecrdg  6015  oafnex  6047  sucinc  6048  fnoa  6050  oaexg  6051  omfnex  6052  fnom  6053  omexg  6054  fnoei  6055  oeiexg  6056  oeiv  6059  oacl  6063  omcl  6064  oeicl  6065  oav2  6066  nnsucelsuc  6093  ercnv  6150  iserd  6155  eqerlem  6160  eqer  6161  ecdmn0m  6171  erth  6173  qsss  6188  ecid  6192  ecidg  6193  qsid  6194  iinerm  6201  qsel  6206  erovlem  6221  ecopovsym  6225  ecopover  6227  th3qlem2  6232  bren  6251  brdomg  6252  domen  6255  domeng  6256  idssen  6280  ener  6282  domtr  6288  ensn1g  6300  en1  6302  en1bg  6303  fundmen  6309  fundmeng  6310  fiprc  6315  unen  6316  xpsnen  6318  xpsneng  6319  xpcomco  6323  xpcomeng  6325  xpassen  6327  xpdom2  6328  xpdom2g  6329  phplem4  6341  phplem3g  6342  nneneq  6343  php5  6344  phpm  6351  findcard  6372  findcard2  6373  findcard2s  6374  ac6sfi  6379  cnvinfex  6431  eqinfti  6433  infvalti  6435  infglbti  6438  infmoti  6441  ordiso2  6446  pm54.43  6459  indpi  6532  dfplpq2  6544  enq0sym  6622  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nqnq0  6631  mulnnnq0  6640  nqprm  6732  nqprrnd  6733  nqprdisj  6734  nqprloc  6735  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  ltnqpr  6783  ltnqpri  6784  archpr  6833  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlem2  6850  caucvgprlemladdfu  6867  caucvgprlem2  6870  caucvgprprlemopu  6889  ltresr  7007  peano1nnnn  7020  peano2nnnn  7021  axcnre  7047  axpre-apti  7051  renfdisj  7172  dfinfre  8034  1nn  8050  peano2nn  8051  indstr  8681  cnref1o  8733  ioof  8994  fzpr  9094  frec2uzzd  9402  frec2uzsucd  9403  frec2uzrand  9407  frec2uzf1od  9408  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgrom  9412  frecuzrdgfn  9414  frecuzrdgsuc  9417  frecfzennn  9419  serile  9474  ibcval5  9690  shftfvalg  9706  ovshftex  9707  shftfibg  9708  shftfval  9709  shftfib  9711  shftfn  9712  2shfti  9719  shftvalg  9724  shftval4g  9725  rexfiuz  9875  maxabslemval  10094  fimaxre2  10109  fclim  10133  climshft  10143  qredeu  10479  isprm2  10499  prmind2  10502  bdcvv  10648  bdsnss  10664  bdop  10666  bj-vprc  10687  bdinex1g  10692  bdssexg  10695  bj-inex  10698  bj-zfpair2  10701  bj-uniexg  10709  bdunexb  10711  bj-unexg  10712  bj-indint  10726  bj-ssom  10731  bj-om  10732  bj-2inf  10733  bj-bdfindis  10742  bj-nn0suc0  10745  bj-nnelirr  10748  bj-inf2vnlem1  10765  bj-inf2vnlem2  10766  bj-omex2  10772  bj-nn0sucALT  10773  bj-findis  10774