Theorem vex 2530

Description: All setvar variables are sets (see isset 2531). 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 1563	. 2 ⊢ x = x
2		df-v 2529	. . 3 ⊢ V = {x ∣ x = x}
3	2	abeq2i 2122	. 2 ⊢ (x ∈ V ↔ x = x)
4	1, 3	mpbir 134	1 ⊢ x ∈ V

Syntax hints:   ∈ wcel 1367  Vcvv 2527

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 1310  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-4 1374  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-ext 1996

This theorem depends on definitions:  df-bi 110  df-sb 1620  df-clab 2001  df-cleq 2007  df-clel 2010  df-v 2529

This theorem is referenced by:  isset  2531  ralv  2540  rexv  2541  reuv  2542  rmov  2543  rabab  2544  sbhypf  2572  ceqex  2640  ralab  2670  rexab  2672  mo2icl  2689  reu8  2706  csbvarg  2846  csbiebg  2858  sbcnestgf  2866  sbnfc2  2875  ddifnel  3044  csbing  3113  unssdif  3141  unssin  3145  inssun  3146  invdif  3148  vn0  3200  vn0m  3201  eqv  3209  abvor0dc  3211  sbss  3298  selpw  3331  elpwg  3332  ssnid  3368  exsnrex  3377  dftp2  3383  prmg  3453  prnzg  3456  snssg  3464  difprsnss  3466  sneqrg  3497  preq12bg  3508  pwprss  3540  pwtpss  3541  pwv  3543  unipr  3558  uniprg  3559  unisng  3561  elintg  3587  elintrabg  3592  intss1  3594  ssint  3595  intmin  3599  intss  3600  intssunim  3601  intmin4  3607  intab  3608  intun  3610  intpr  3611  intprg  3612  uniintsnr  3615  iinconstm  3630  iuniin  3631  iinss1  3633  dfiin2g  3654  dfiunv2  3657  ssiinf  3670  iinss  3672  iinss2  3673  0iin  3679  iinab  3682  iundif2ss  3686  iindif2m  3688  iinin2m  3689  iinuniss  3701  sspwuni  3703  iinpw  3706  iunpwss  3707  brab1  3773  csbopabg  3799  mptv  3817  trint  3833  trintssm  3834  vprc  3852  inex1g  3857  ssexg  3860  inteximm  3867  inuni  3873  repizf2  3879  axpweq  3888  bnd2  3890  pwexg  3897  pwuni  3907  zfpair2  3909  rext  3915  sspwb  3916  unipw  3917  ssextss  3920  euabex  3925  mss  3926  exss  3927  opth  3938  opthg  3939  copsexg  3945  copsex4g  3948  moop2  3952  euotd  3955  opabid  3958  elopab  3959  opelopabsbALT  3960  opelopabsb  3961  opabm  3981  pwin  3983  pwunss  3984  epelg  3991  epel  3993  pofun  4013  epse  4037  tron  4058  sucel  4086  suctr  4097  uniexg  4114  unexb  4116  snnex  4120  uniuni  4122  eusvnf  4124  eusvnfb  4125  iunpw  4150  unon  4175  ordunisuc2r  4178  onsucelsucexmidlem  4187  ordsucunielexmid  4189  elirr  4197  en2lp  4205  dtruex  4210  finds  4239  finds2  4240  elnn  4244  limom  4252  0nelxp  4288  opelxp  4290  opeliunxp  4311  elvv  4318  elvvv  4319  elvvuni  4320  xpsspw  4366  relopabi  4379  opabid2  4383  difopab  4385  xpiindim  4389  raliunxp  4393  rexiunxp  4394  ralxpf  4398  rexxpf  4399  relop  4402  cnvco  4436  dfrn2  4439  dfdm4  4443  dmss  4450  dmin  4459  dmiun  4460  dmuni  4461  dm0  4465  dmi  4466  reldm0  4469  elreldm  4476  elrnmpt1  4501  dmrnssfld  4511  dmcoss  4517  dmcosseq  4519  opelresg  4535  resieq  4538  dmres  4548  elres  4562  relssres  4564  resopab  4568  resiexg  4569  iss  4570  dfres2  4574  dfima2  4586  imadmrn  4594  imai  4597  csbima12g  4602  elimasng  4609  args  4610  epini  4612  iniseg  4613  dfse2  4614  exse2  4615  cotr  4622  issref  4623  cnvsym  4624  intasym  4625  asymref  4626  intirr  4627  brcodir  4628  codir  4629  qfto  4630  poirr2  4633  cnvopab  4642  cnv0  4643  cnvi  4644  cnvdif  4646  rniun  4650  dminss  4654  imainss  4655  inimasn  4657  xpmlem  4660  dmxpss  4669  rnxpid  4671  ssrnres  4679  rninxp  4680  dminxp  4681  cnvcnv3  4686  dfrel2  4687  dmsnm  4702  dmsnopg  4708  cnvcnvsn  4713  dmsnsnsng  4714  cnvsng  4722  elxp4  4724  elxp5  4725  cnvresima  4726  dfco2  4736  dfco2a  4737  cores  4740  resco  4741  imaco  4742  rnco  4743  coiun  4746  co02  4750  coi1  4752  coass  4755  relssdmrn  4757  unielrel  4761  ressn  4774  cnviinm  4775  cnvpom  4776  cnvsom  4777  uniabio  4793  iotaval  4794  iotass  4800  sniota  4810  csbiotag  4811  dffun2  4828  dffun7  4843  dffun8  4844  dffun9  4845  funopg  4849  funssres  4857  funun  4859  funcnvsn  4860  funcnv2  4874  funcnv  4875  funcnv3  4876  funcnveq  4877  fun2cnv  4878  funcnvuni  4883  imadif  4894  funimaexglem  4897  isarep1  4900  2elresin  4925  fnres  4930  fcnvres  4987  fconstg  4997  fun11iun  5061  f1osng  5081  dffv3g  5088  fvssunirng  5104  sefvex  5110  fv3  5111  fvres  5112  nfunsn  5121  funimass4  5138  ssimaexg  5149  dmfco  5155  fvopab6  5178  fndmdif  5186  fvelrn  5212  dffo4  5229  f1ompt  5234  fmptco  5244  fsn  5249  fsng  5250  dfmpt  5254  dfmptg  5256  fnressn  5263  fressnfv  5264  fvsng  5273  resfunexg  5296  funfvima3  5306  idref  5310  abrexco  5312  imaiun  5313  dff13  5321  foeqcnvco  5344  f1eqcocnv  5345  fliftcnv  5349  isocnv2  5366  isoini  5371  isose  5374  riotav  5386  csbriotag  5393  acexmidlem2  5422  oprabid  5450  csbov123g  5455  0neqopab  5462  brabvv  5463  dfoprab2  5464  rnoprab  5499  eloprabga  5503  mpt2v  5506  f1opw  5619  opabex3d  5660  opabex3  5661  ofmres  5675  op1stg  5689  op2ndg  5690  1stval2  5694  2ndval2  5695  fo1st  5696  fo2nd  5697  f1stres  5698  f2ndres  5699  fo1stresm  5700  fo2ndresm  5701  xp1st  5704  xp2nd  5705  releldm2  5723  reldm  5724  sbcopeq1a  5725  csbopeq1a  5726  dfoprab3  5729  eloprabi  5734  mpt2mptsx  5735  dmmpt2ssx  5737  fmpt2x  5738  mpt2fvex  5741  mpt2exxg  5745  fmpt2co  5749  df1st2  5752  df2nd2  5753  1stconst  5754  2ndconst  5755  dfmpt2  5756  fo2ndf  5760  f1o2ndf1  5761  xporderlem  5763  brtpos2  5777  reldmtpos  5779  dmtpos  5782  rntpos  5783  ovtposg  5785  dftpos3  5788  dftpos4  5789  tpostpos  5790  tpossym  5802  tfrlem3  5837  tfrlem5  5841  tfrlem8  5845  tfrlemisucfn  5848  tfrlemisucaccv  5849  tfrlemibxssdm  5851  tfrlemibfn  5852  tfrlemibex  5853  tfrlemi14d  5857  tfrlemi14  5858  tfrexlem  5859  rdgruledefgg  5871  rdgivallem  5877  rdgon  5882  frecabex  5888  frectfr  5889  frec0g  5891  frecsuclem3  5895  oafnex  5928  sucinc  5929  fnoa  5931  oaexg  5932  omfnex  5933  fnom  5934  omexg  5935  fnoei  5936  oeiexg  5937  oeiv  5940  oa0  5941  oei0  5943  oacl  5944  omcl  5945  oeicl  5946  oav2  5947  nnsucelsuc  5974  ercnv  6027  iserd  6032  eqerlem  6037  eqer  6038  ecdmn0m  6048  erth  6050  qsss  6065  ecid  6069  ecidg  6070  qsid  6071  iinerm  6078  qsel  6083  erovlem  6098  ecopovsym  6102  ecopover  6104  th3qlem2  6109  dfplpq2  6200  enq0sym  6274  enq0ref  6275  enq0tr  6276  nqnq0pi  6280  nqnq0  6283  mulnnnq0  6292  nqprm  6384  nqprrnd  6385  nqprdisj  6386  nqprloc  6387  ltresr  6546  axcnre  6571  axpre-apti  6575  renfdisj  6680  1nn  7509  peano2nn  7510  bdcvv  8314  bdsnss  8330  bdop  8332  bj-vprc  8349  bdinex1g  8354  bdssexg  8357  bj-inex  8360  bj-zfpair2  8363  bj-uniexg  8371  bdunexb  8373  bj-unexg  8374  bj-indint  8388  bj-ssom  8392  bj-om  8393  bj-2inf  8394  bj-bdfindis  8403  bj-nn0suc0  8406  bj-nnelirr  8409  bj-inf2vnlem1  8422  bj-inf2vnlem2  8423  bj-omex2  8429  bj-nn0sucALT  8430  bj-findis  8431