Theorem vex 2554

Description: All setvar variables are sets (see isset 2555). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	⊢ x ∈ V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		equid 1586	. 2 ⊢ x = x
2		df-v 2553	. . 3 ⊢ V = {x ∣ x = x}
3	2	abeq2i 2145	. 2 ⊢ (x ∈ V ↔ x = x)
4	1, 3	mpbir 134	1 ⊢ x ∈ V

Syntax hints:   ∈ wcel 1390  Vcvv 2551

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553

This theorem is referenced by:  isset  2555  eqvisset  2559  ralv  2565  rexv  2566  reuv  2567  rmov  2568  rabab  2569  sbhypf  2597  ceqex  2665  ralab  2695  rexab  2697  mo2icl  2714  reu8  2731  csbvarg  2871  csbiebg  2883  sbcnestgf  2891  sbnfc2  2900  ddifnel  3069  csbing  3138  unssdif  3166  unssin  3170  inssun  3171  invdif  3173  vn0  3225  vn0m  3226  eqv  3234  abvor0dc  3236  sbss  3323  selpw  3358  elpwg  3359  ssnid  3395  exsnrex  3404  dftp2  3410  prmg  3480  prnzg  3483  snssg  3491  difprsnss  3493  sneqrg  3524  preq12bg  3535  pwprss  3567  pwtpss  3568  pwv  3570  unipr  3585  uniprg  3586  unisng  3588  elintg  3614  elintrabg  3619  intss1  3621  ssint  3622  intmin  3626  intss  3627  intssunim  3628  intmin4  3634  intab  3635  intun  3637  intpr  3638  intprg  3639  uniintsnr  3642  iinconstm  3657  iuniin  3658  iinss1  3660  dfiin2g  3681  dfiunv2  3684  ssiinf  3697  iinss  3699  iinss2  3700  0iin  3706  iinab  3709  iundif2ss  3713  iindif2m  3715  iinin2m  3716  iinuniss  3728  sspwuni  3730  iinpw  3733  iunpwss  3734  brab1  3800  csbopabg  3826  mptv  3844  trint  3860  trintssm  3861  vprc  3879  inex1g  3884  ssexg  3887  inteximm  3894  inuni  3900  repizf2  3906  axpweq  3915  bnd2  3917  pwexg  3924  pwuni  3934  zfpair2  3936  rext  3942  sspwb  3943  unipw  3944  ssextss  3947  euabex  3952  mss  3953  exss  3954  opth  3965  opthg  3966  copsexg  3972  copsex4g  3975  moop2  3979  euotd  3982  opabid  3985  elopab  3986  opelopabsbALT  3987  opelopabsb  3988  opabm  4008  pwin  4010  pwunss  4011  epelg  4018  epel  4020  pofun  4040  epse  4064  tron  4085  sucel  4113  suctr  4124  uniexg  4141  unexb  4143  snnex  4147  uniuni  4149  eusvnf  4151  eusvnfb  4152  iunpw  4177  unon  4202  ordunisuc2r  4205  onsucelsucexmidlem  4214  ordsucunielexmid  4216  elirr  4224  en2lp  4232  dtruex  4237  finds  4266  finds2  4267  elnn  4271  limom  4279  0nelxp  4315  opelxp  4317  opeliunxp  4338  elvv  4345  elvvv  4346  elvvuni  4347  xpsspw  4393  relopabi  4406  opabid2  4410  difopab  4412  xpiindim  4416  raliunxp  4420  rexiunxp  4421  ralxpf  4425  rexxpf  4426  relop  4429  cnvco  4463  dfrn2  4466  dfdm4  4470  dmss  4477  dmin  4486  dmiun  4487  dmuni  4488  dm0  4492  dmi  4493  reldm0  4496  elreldm  4503  elrnmpt1  4528  dmrnssfld  4538  dmcoss  4544  dmcosseq  4546  opelresg  4562  resieq  4565  dmres  4575  elres  4589  relssres  4591  resopab  4595  resiexg  4596  iss  4597  dfres2  4601  dfima2  4613  imadmrn  4621  imai  4624  csbima12g  4629  elimasng  4636  args  4637  epini  4639  iniseg  4640  dfse2  4641  exse2  4642  cotr  4649  issref  4650  cnvsym  4651  intasym  4652  asymref  4653  intirr  4654  brcodir  4655  codir  4656  qfto  4657  poirr2  4660  cnvopab  4669  cnv0  4670  cnvi  4671  cnvdif  4673  rniun  4677  dminss  4681  imainss  4682  inimasn  4684  xpmlem  4687  dmxpss  4696  rnxpid  4698  ssrnres  4706  rninxp  4707  dminxp  4708  cnvcnv3  4713  dfrel2  4714  dmsnm  4729  dmsnopg  4735  cnvcnvsn  4740  dmsnsnsng  4741  cnvsng  4749  elxp4  4751  elxp5  4752  cnvresima  4753  dfco2  4763  dfco2a  4764  cores  4767  resco  4768  imaco  4769  rnco  4770  coiun  4773  co02  4777  coi1  4779  coass  4782  relssdmrn  4784  unielrel  4788  ressn  4801  cnviinm  4802  cnvpom  4803  cnvsom  4804  uniabio  4820  iotaval  4821  iotass  4827  sniota  4837  csbiotag  4838  dffun2  4855  dffun7  4871  dffun8  4872  dffun9  4873  funopg  4877  funssres  4885  funun  4887  funcnvsn  4888  funcnv2  4902  funcnv  4903  funcnv3  4904  funcnveq  4905  fun2cnv  4906  funcnvuni  4911  imadif  4922  funimaexglem  4925  isarep1  4928  2elresin  4953  fnres  4958  fcnvres  5016  fconstg  5026  fun11iun  5090  f1osng  5110  dffv3g  5117  fvssunirng  5133  sefvex  5139  fv3  5140  fvres  5141  nfunsn  5150  funimass4  5167  ssimaexg  5178  dmfco  5184  fvopab6  5207  fndmdif  5215  fvelrn  5241  dffo4  5258  f1ompt  5263  fmptco  5273  fsn  5278  fsng  5279  dfmpt  5283  dfmptg  5285  fnressn  5292  fressnfv  5293  fvsng  5302  resfunexg  5325  funfvima3  5335  idref  5339  abrexco  5341  imaiun  5342  dff13  5350  foeqcnvco  5373  f1eqcocnv  5374  fliftcnv  5378  isocnv2  5395  isoini  5400  isose  5403  riotav  5416  csbriotag  5423  acexmidlem2  5452  oprabid  5480  csbov123g  5485  0neqopab  5492  brabvv  5493  dfoprab2  5494  rnoprab  5529  eloprabga  5533  mpt2v  5536  f1opw  5649  opabex3d  5690  opabex3  5691  ofmres  5705  op1stg  5719  op2ndg  5720  1stval2  5724  2ndval2  5725  fo1st  5726  fo2nd  5727  f1stres  5728  f2ndres  5729  fo1stresm  5730  fo2ndresm  5731  xp1st  5734  xp2nd  5735  releldm2  5753  reldm  5754  sbcopeq1a  5755  csbopeq1a  5756  dfoprab3  5759  eloprabi  5764  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  mpt2fvex  5771  mpt2exxg  5775  fmpt2co  5779  df1st2  5782  df2nd2  5783  1stconst  5784  2ndconst  5785  dfmpt2  5786  fo2ndf  5790  f1o2ndf1  5791  xporderlem  5793  brtpos2  5807  reldmtpos  5809  dmtpos  5812  rntpos  5813  ovtposg  5815  dftpos3  5818  dftpos4  5819  tpostpos  5820  tpossym  5832  tfrlem3  5867  tfrlem5  5871  tfrlem8  5875  tfrlemisucfn  5879  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemibex  5884  tfrlemi14d  5888  tfrexlem  5889  rdgtfr  5901  rdgruledefgg  5902  rdgivallem  5908  rdgon  5913  rdg0g  5915  frec0g  5922  frecabex  5923  frectfr  5924  frecsuclem3  5929  frecrdg  5931  oafnex  5963  sucinc  5964  fnoa  5966  oaexg  5967  omfnex  5968  fnom  5969  omexg  5970  fnoei  5971  oeiexg  5972  oeiv  5975  oacl  5979  omcl  5980  oeicl  5981  oav2  5982  nnsucelsuc  6009  ercnv  6063  iserd  6068  eqerlem  6073  eqer  6074  ecdmn0m  6084  erth  6086  qsss  6101  ecid  6105  ecidg  6106  qsid  6107  iinerm  6114  qsel  6119  erovlem  6134  ecopovsym  6138  ecopover  6140  th3qlem2  6145  bren  6164  brdomg  6165  domen  6168  domeng  6169  idssen  6193  ener  6195  domtr  6201  ensn1g  6213  en1  6215  en1bg  6216  fundmen  6222  fundmeng  6223  fiprc  6228  unen  6229  xpsnen  6231  xpsneng  6232  xpcomco  6236  xpcomeng  6238  xpassen  6240  xpdom2  6241  xpdom2g  6242  indpi  6326  dfplpq2  6338  enq0sym  6415  enq0ref  6416  enq0tr  6417  nqnq0pi  6421  nqnq0  6424  mulnnnq0  6433  nqprm  6525  nqprrnd  6526  nqprdisj  6527  nqprloc  6528  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  archpr  6615  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlem2  6632  caucvgprlemladdfu  6648  caucvgprlem2  6651  ltresr  6736  axcnre  6765  axpre-apti  6769  renfdisj  6876  1nn  7706  peano2nn  7707  indstr  8312  cnref1o  8357  ioof  8610  fzpr  8709  frec2uzzd  8867  frec2uzsucd  8868  frec2uzrand  8872  frec2uzf1od  8873  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdgfn  8879  frecuzrdgsuc  8882  frecfzennn  8884  bdcvv  9312  bdsnss  9328  bdop  9330  bj-vprc  9351  bdinex1g  9356  bdssexg  9359  bj-inex  9362  bj-zfpair2  9365  bj-uniexg  9373  bdunexb  9375  bj-unexg  9376  bj-indint  9390  bj-ssom  9395  bj-om  9396  bj-2inf  9397  bj-bdfindis  9407  bj-nn0suc0  9410  bj-nnelirr  9413  bj-inf2vnlem1  9430  bj-inf2vnlem2  9431  bj-omex2  9437  bj-nn0sucALT  9438  bj-findis  9439