Theorem vex 2538

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

Syntax hints:   ∈ wcel 1374  Vcvv 2535

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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-v 2537

This theorem is referenced by:  isset  2539  ralv  2548  rexv  2549  reuv  2550  rmov  2551  rabab  2552  sbhypf  2580  ceqex  2648  ralab  2678  rexab  2680  mo2icl  2697  reu8  2714  csbvarg  2854  csbiebg  2866  sbcnestgf  2874  sbnfc2  2883  ddifnel  3052  csbing  3121  unssdif  3149  unssin  3153  inssun  3154  invdif  3156  vn0  3208  vn0m  3209  eqv  3217  abvor0dc  3219  sbss  3308  selpw  3341  elpwg  3342  ssnid  3378  exsnrex  3387  dftp2  3393  prmg  3463  prnzg  3466  snssg  3474  difprsnss  3476  sneqrg  3507  preq12bg  3518  pwprss  3550  pwtpss  3551  pwv  3553  unipr  3568  uniprg  3569  unisng  3571  elintg  3597  elintrabg  3602  intss1  3604  ssint  3605  intmin  3609  intss  3610  intssunim  3611  intmin4  3617  intab  3618  intun  3620  intpr  3621  intprg  3622  uniintsnr  3625  iinconstm  3640  iuniin  3641  iinss1  3643  dfiin2g  3664  dfiunv2  3667  ssiinf  3680  iinss  3682  iinss2  3683  0iin  3689  iinab  3692  iundif2ss  3696  iindif2m  3698  iinin2m  3699  iinuniss  3711  sspwuni  3713  iinpw  3716  iunpwss  3717  brab1  3783  csbopabg  3809  mptv  3827  trint  3843  trintssm  3844  vprc  3862  inex1g  3867  ssexg  3870  inteximm  3877  inuni  3883  repizf2  3889  axpweq  3898  bnd2  3900  pwexg  3907  pwuni  3917  zfpair2  3919  rext  3925  sspwb  3926  unipw  3927  ssextss  3930  euabex  3935  mss  3936  exss  3937  opth  3948  opthg  3949  copsexg  3955  copsex4g  3958  moop2  3962  euotd  3965  opabid  3968  elopab  3969  opelopabsbALT  3970  opelopabsb  3971  opabm  3991  pwin  3993  pwunss  3994  epelg  4001  epel  4003  pofun  4023  epse  4047  tron  4068  sucel  4096  suctrALT  4107  uniexg  4125  unexb  4127  snnex  4131  uniuni  4133  eusvnf  4135  eusvnfb  4136  iunpw  4161  unon  4186  ordunisuc2r  4189  onsucelsucexmidlem  4198  ordsucunielexmid  4200  elirr  4208  en2lp  4216  dtruex  4221  finds  4250  finds2  4251  elnn  4255  limom  4263  0nelxp  4299  opelxp  4301  opeliunxp  4322  elvv  4329  elvvv  4330  elvvuni  4331  xpsspw  4377  relopabi  4390  opabid2  4394  difopab  4396  xpiindim  4400  raliunxp  4404  rexiunxp  4405  ralxpf  4409  rexxpf  4410  relop  4413  cnvco  4447  dfrn2  4450  dfdm4  4454  dmss  4461  dmin  4470  dmiun  4471  dmuni  4472  dm0  4476  dmi  4477  reldm0  4480  elreldm  4487  elrnmpt1  4512  dmrnssfld  4522  dmcoss  4528  dmcosseq  4530  opelresg  4546  resieq  4549  dmres  4559  elres  4573  relssres  4575  resopab  4579  resiexg  4580  iss  4581  dfres2  4585  dfima2  4597  imadmrn  4605  imai  4608  csbima12g  4613  elimasng  4620  args  4621  epini  4623  iniseg  4624  dfse2  4625  exse2  4626  cotr  4633  issref  4634  cnvsym  4635  intasym  4636  asymref  4637  intirr  4638  brcodir  4639  codir  4640  qfto  4641  poirr2  4644  cnvopab  4653  cnv0  4654  cnvi  4655  cnvdif  4657  rniun  4661  dminss  4665  imainss  4666  inimasn  4668  xpmlem  4671  dmxpss  4680  rnxpid  4682  ssrnres  4690  rninxp  4691  dminxp  4692  cnvcnv3  4697  dfrel2  4698  dmsnm  4713  dmsnopg  4719  cnvcnvsn  4724  dmsnsnsng  4725  cnvsng  4733  elxp4  4735  elxp5  4736  cnvresima  4737  dfco2  4747  dfco2a  4748  cores  4751  resco  4752  imaco  4753  rnco  4754  coiun  4757  co02  4761  coi1  4763  coass  4766  relssdmrn  4768  unielrel  4772  ressn  4785  cnviinm  4786  cnvpom  4787  cnvsom  4788  uniabio  4804  iotaval  4805  iotass  4811  sniota  4821  csbiotag  4822  dffun2  4839  dffun7  4854  dffun8  4855  dffun9  4856  funopg  4860  funssres  4868  funun  4870  funcnvsn  4871  funcnv2  4885  funcnv  4886  funcnv3  4887  funcnveq  4888  fun2cnv  4889  funcnvuni  4894  imadif  4905  funimaexglem  4908  isarep1  4911  2elresin  4936  fnres  4941  fcnvres  4998  fconstg  5008  fun11iun  5072  f1osng  5092  dffv3g  5099  fvssunirng  5115  sefvex  5121  fv3  5122  fvres  5123  nfunsn  5132  funimass4  5149  ssimaexg  5160  dmfco  5166  fvopab6  5189  fndmdif  5197  fvelrn  5223  dffo4  5240  f1ompt  5245  fmptco  5255  fsn  5260  fsng  5261  dfmpt  5265  dfmptg  5267  fnressn  5274  fressnfv  5275  fvsng  5284  resfunexg  5307  funfvima3  5317  idref  5321  abrexco  5323  imaiun  5324  dff13  5332  foeqcnvco  5355  f1eqcocnv  5356  fliftcnv  5360  isocnv2  5377  isoini  5382  isose  5385  riotav  5397  csbriotag  5404  acexmidlem2  5433  oprabid  5461  csbov123g  5466  0neqopab  5473  brabvv  5474  dfoprab2  5475  rnoprab  5510  eloprabga  5514  mpt2v  5517  f1opw  5630  opabex3d  5671  opabex3  5672  ofmres  5686  op1stg  5700  op2ndg  5701  1stval2  5705  2ndval2  5706  fo1st  5707  fo2nd  5708  f1stres  5709  f2ndres  5710  fo1stresm  5711  fo2ndresm  5712  xp1st  5715  xp2nd  5716  releldm2  5734  reldm  5735  sbcopeq1a  5736  csbopeq1a  5737  dfoprab3  5740  eloprabi  5745  mpt2mptsx  5746  dmmpt2ssx  5748  fmpt2x  5749  mpt2fvex  5752  mpt2exxg  5756  fmpt2co  5760  df1st2  5763  df2nd2  5764  1stconst  5765  2ndconst  5766  dfmpt2  5767  fo2ndf  5771  f1o2ndf1  5772  xporderlem  5774  brtpos2  5788  reldmtpos  5790  dmtpos  5793  rntpos  5794  ovtposg  5796  dftpos3  5799  dftpos4  5800  tpostpos  5801  tpossym  5813  tfrlem3  5848  tfrlem5  5852  tfrlem8  5856  tfrlemisucfn  5859  tfrlemisucaccv  5860  tfrlemibxssdm  5862  tfrlemibfn  5863  tfrlemibex  5864  tfrlemi14d  5868  tfrlemi14  5869  tfrexlem  5870  rdgruledefgg  5882  rdgivallem  5888  rdgon  5893  frecabex  5899  frectfr  5900  frec0g  5902  frecsuclem3  5906  oafnex  5939  sucinc  5940  fnoa  5942  oaexg  5943  omfnex  5944  fnom  5945  omexg  5946  fnoei  5947  oeiexg  5948  oeiv  5951  oa0  5952  oei0  5954  oacl  5955  omcl  5956  oeicl  5957  oav2  5958  nnsucelsuc  5985  ercnv  6038  iserd  6043  eqerlem  6048  eqer  6049  ecdmn0m  6059  erth  6061  qsss  6076  ecid  6080  ecidg  6081  qsid  6082  iinerm  6089  qsel  6094  erovlem  6109  ecopovsym  6113  ecopover  6115  th3qlem2  6120  dfplpq2  6213  enq0sym  6287  enq0ref  6288  enq0tr  6289  nqnq0pi  6293  nqnq0  6296  mulnnnq0  6305  nqprm  6397  nqprrnd  6398  nqprdisj  6399  nqprloc  6400  ltresr  6550  axcnre  6575  renfdisj  6680  bdcvv  7084  bdsnss  7100  bdop  7102  bj-vprc  7119  bdinex1g  7124  bdssexg  7127  bj-inex  7130  bj-zfpair2  7133  bj-uniexg  7141  bdunexb  7143  bj-unexg  7144  bj-indint  7154  bj-ssom  7158  bj-om  7159  bj-2inf  7160  bj-bdfindis  7169  bj-nn0suc0  7172  bj-nnelirr  7175  bj-inf2vnlem1  7188  bj-inf2vnlem2  7189  bj-omex2  7195  bj-nn0sucALT  7196  bj-findis  7197