Theorem vex 2618

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

Syntax hints:   ∈ wcel 1436  Vcvv 2615

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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-v 2617

This theorem is referenced by:  isset  2619  eqvisset  2623  ralv  2630  rexv  2631  reuv  2632  rmov  2633  rabab  2634  sbhypf  2662  ceqex  2735  ralab  2766  rexab  2768  mo2icl  2785  reu8  2802  csbvarg  2947  csbiebg  2959  sbcnestgf  2968  sbnfc2  2977  ddifnel  3120  ddifstab  3121  csbing  3196  unssdif  3223  unssin  3227  inssun  3228  invdif  3230  vn0  3282  vn0m  3283  eqv  3291  abvor0dc  3295  sbss  3377  selpw  3422  elpwg  3423  velsn  3448  vsnid  3459  exsnrex  3468  dftp2  3474  prmg  3544  prnzg  3547  snssg  3556  difprsnss  3558  sneqrg  3589  preq12bg  3600  pwprss  3632  pwtpss  3633  pwv  3635  unipr  3650  uniprg  3651  unisng  3653  elintg  3679  elintrabg  3684  intss1  3686  ssint  3687  intmin  3691  intss  3692  intssunim  3693  intmin4  3699  intab  3700  intun  3702  intpr  3703  intprg  3704  uniintsnr  3707  iinconstm  3722  iuniin  3723  iinss1  3725  dfiin2g  3746  dfiunv2  3749  ssiinf  3762  iinss  3764  iinss2  3765  0iin  3771  iinab  3774  iundif2ss  3778  iindif2m  3780  iinin2m  3781  iinuniss  3793  sspwuni  3795  iinpw  3798  iunpwss  3799  brab1  3865  csbopabg  3891  mptv  3910  trint  3926  trintssmOLD  3928  vnex  3945  inex1g  3950  ssexg  3953  inteximm  3960  inuni  3966  repizf2  3972  axpweq  3981  bnd2  3983  pwuni  4001  exmidundif  4009  zfpair2  4011  rext  4016  sspwb  4017  unipw  4018  ssextss  4021  euabex  4026  mss  4027  exss  4028  opth  4038  opthg  4039  copsexg  4045  copsex4g  4048  moop2  4052  euotd  4055  opabid  4058  elopab  4059  opelopabsbALT  4060  opelopabsb  4061  opabm  4081  pwin  4083  pwunss  4084  epelg  4091  epel  4093  pofun  4113  epse  4143  tron  4183  sucel  4211  suctr  4222  uniexg  4239  unexb  4241  snnex  4245  uniuni  4247  eusvnf  4249  eusvnfb  4250  iunpw  4275  unon  4301  ordunisuc2r  4304  ordtri2or2exmidlem  4315  onsucelsucexmidlem  4318  ordsucunielexmid  4320  elirr  4330  en2lp  4343  dtruex  4348  onintexmid  4361  reg3exmidlemwe  4367  dcextest  4369  finds  4388  finds2  4389  elnn  4393  limom  4401  0nelxp  4438  opelxp  4440  opeliunxp  4461  elvv  4468  elvvv  4469  elvvuni  4470  xpsspw  4518  relopabi  4531  opabid2  4535  difopab  4537  xpiindim  4541  raliunxp  4545  rexiunxp  4546  ralxpf  4550  rexxpf  4551  relop  4554  cnvco  4589  dfrn2  4592  dfdm4  4596  dmss  4603  dmin  4612  dmiun  4613  dmuni  4614  dm0  4618  dmi  4619  reldm0  4622  elreldm  4629  elrnmpt1  4654  dmrnssfld  4664  dmcoss  4670  dmcosseq  4672  opelresg  4688  resieq  4691  dmres  4701  elres  4715  relssres  4717  resopab  4723  resiexg  4724  iss  4725  dfres2  4731  dfima2  4743  imadmrn  4751  imai  4755  csbima12g  4760  elimasng  4767  args  4768  epini  4770  iniseg  4771  dfse2  4772  exse2  4773  cotr  4780  issref  4781  cnvsym  4782  intasym  4783  asymref  4784  intirr  4785  brcodir  4786  codir  4787  qfto  4788  poirr2  4791  cnvopab  4800  cnv0  4801  cnvi  4802  cnvdif  4804  rniun  4808  dminss  4812  imainss  4813  inimasn  4815  xpmlem  4818  dmxpss  4827  rnxpid  4831  ssrnres  4839  rninxp  4840  dminxp  4841  cnvcnv3  4846  dfrel2  4847  dmsnm  4862  dmsnopg  4868  cnvcnvsn  4873  dmsnsnsng  4874  cnvsng  4882  elxp4  4884  elxp5  4885  cnvresima  4886  dfco2  4896  dfco2a  4897  cores  4900  resco  4901  imaco  4902  rnco  4903  coiun  4906  co02  4910  coi1  4912  coass  4915  relssdmrn  4917  unielrel  4924  ressn  4937  cnviinm  4938  cnvpom  4939  cnvsom  4940  uniabio  4956  iotaval  4957  iotass  4963  sniota  4973  csbiotag  4974  dffun2  4991  dffun7  5007  dffun8  5008  dffun9  5009  funopg  5013  funssres  5021  funun  5023  funcnvsn  5024  funinsn  5028  funcnv2  5039  funcnv  5040  funcnv3  5041  funcnveq  5042  fun2cnv  5043  funcnvuni  5048  imadif  5059  funimaexglem  5062  isarep1  5065  2elresin  5090  fnres  5095  fcnvres  5157  fconstg  5170  fun11iun  5237  f1osng  5257  dffv3g  5264  fvssunirng  5283  sefvex  5289  fv3  5291  fvres  5292  nfunsn  5301  funimass4  5318  ssimaexg  5329  dmfco  5335  fvopab6  5359  fndmdif  5367  fvelrn  5393  dffo4  5410  f1ompt  5413  fmptco  5427  fsn  5432  fsng  5433  dfmpt  5437  dfmptg  5439  fnressn  5446  fressnfv  5447  fvsng  5456  resfunexg  5479  funfvima3  5489  idref  5497  abrexco  5499  imaiun  5500  dff13  5508  foeqcnvco  5530  f1eqcocnv  5531  fliftcnv  5535  isocnv2  5552  isoini  5558  isose  5561  riotav  5574  csbriotag  5581  acexmidlem2  5610  oprabid  5638  csbov123g  5644  0neqopab  5651  brabvv  5652  dfoprab2  5653  rnoprab  5688  eloprabga  5692  mpt2v  5695  f1opw  5808  opabex3d  5849  opabex3  5850  ofmres  5864  op1stg  5878  op2ndg  5879  1stval2  5883  2ndval2  5884  fo1st  5885  fo2nd  5886  f1stres  5887  f2ndres  5888  fo1stresm  5889  fo2ndresm  5890  xp1st  5893  xp2nd  5894  releldm2  5912  reldm  5913  sbcopeq1a  5914  csbopeq1a  5915  dfoprab3  5918  eloprabi  5923  mpt2mptsx  5924  dmmpt2ssx  5926  fmpt2x  5927  mpt2fvex  5930  mpt2exxg  5934  fmpt2co  5938  df1st2  5941  df2nd2  5942  1stconst  5943  2ndconst  5944  dfmpt2  5945  fo2ndf  5949  f1o2ndf1  5950  xporderlem  5953  cnvoprab  5956  f1od2  5957  brtpos2  5970  reldmtpos  5972  dmtpos  5975  rntpos  5976  ovtposg  5978  dftpos3  5981  dftpos4  5982  tpostpos  5983  tpossym  5995  tfrlem3  6030  tfrlem5  6033  tfrlem8  6037  tfrlemisucfn  6043  tfrlemisucaccv  6044  tfrlemibxssdm  6046  tfrlemibfn  6047  tfrlemibex  6048  tfrlemi14d  6052  tfrexlem  6053  tfr1onlem3  6057  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemres  6068  tfri1dALT  6070  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemres  6081  tfrcl  6083  rdgtfr  6093  rdgruledefgg  6094  rdgivallem  6100  rdgon  6105  rdg0g  6107  frec0g  6116  frecabex  6117  frecabcl  6118  frectfr  6119  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecrdg  6127  oafnex  6159  sucinc  6160  fnoa  6162  oaexg  6163  omfnex  6164  fnom  6165  omexg  6166  fnoei  6167  oeiexg  6168  oeiv  6171  oacl  6175  omcl  6176  oeicl  6177  oav2  6178  nnsucelsuc  6206  nnsucuniel  6210  ercnv  6265  iserd  6270  eqerlem  6275  eqer  6276  ecdmn0m  6286  erth  6288  qsss  6303  ecid  6307  ecidg  6308  qsid  6309  iinerm  6316  qsel  6321  erovlem  6336  ecopovsym  6340  ecopover  6342  th3qlem2  6347  mapprc  6361  fnmap  6364  fnpm  6365  mapdm0  6372  mapval2  6387  mapsn  6399  mapsncnv  6404  mapsnf1o2  6405  bren  6416  brdomg  6417  domen  6420  domeng  6421  ctex  6422  idssen  6446  ener  6448  domtr  6454  ensn1g  6466  en1  6468  en1bg  6469  fundmen  6475  fundmeng  6476  mapsnen  6480  fiprc  6484  unen  6485  xpsnen  6489  xpsneng  6490  xpcomco  6494  xpcomeng  6496  xpassen  6498  xpdom2  6499  xpdom2g  6500  xpf1o  6512  mapen  6514  mapxpen  6516  xpmapenlem  6517  ssenen  6519  phplem4  6523  phplem3g  6524  nneneq  6525  php5  6526  phpm  6533  findcard  6556  findcard2  6557  findcard2s  6558  isinfinf  6565  ac6sfi  6566  exmidpw  6576  unfidisj  6584  xpfi  6590  fisseneq  6592  ssfirab  6593  snexxph  6608  sbthlemi10  6619  isbth  6620  cnvinfex  6657  eqinfti  6659  infvalti  6661  infglbti  6664  infmoti  6667  ordiso2  6672  djuf1olem  6689  djuun  6704  djuss  6705  finomni  6740  exmidomniim  6741  exmidomni  6742  fodjuomnilemdc  6743  pm54.43  6762  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  indpi  6845  dfplpq2  6857  enq0sym  6935  enq0ref  6936  enq0tr  6937  nqnq0pi  6941  nqnq0  6944  mulnnnq0  6953  nqprm  7045  nqprrnd  7046  nqprdisj  7047  nqprloc  7048  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemrl  7076  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  ltnqpr  7096  ltnqpri  7097  archpr  7146  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlem2  7163  caucvgprlemladdfu  7180  caucvgprlem2  7183  caucvgprprlemopu  7202  ltresr  7320  peano1nnnn  7333  peano2nnnn  7334  axcnre  7360  axpre-apti  7364  renfdisj  7490  dfinfre  8352  1nn  8368  peano2nn  8369  indstr  9013  cnref1o  9065  ioof  9321  fzpr  9421  frec2uzrand  9740  frec2uzf1od  9741  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  frecfzennn  9761  serile  9851  ibcval5  10067  hashinfom  10082  hashunlem  10108  hashun  10109  hashxp  10130  hashfacen  10137  zfz1isolem1  10141  zfz1iso  10142  shftfvalg  10148  ovshftex  10149  shftfibg  10150  shftfval  10151  shftfib  10153  shftfn  10154  2shfti  10161  shftvalg  10166  shftval4g  10167  rexfiuz  10317  maxabslemval  10536  fimaxre2  10551  fclim  10575  climshft  10585  zisum  10663  fisum  10665  qredeu  10954  isprm2  10974  prmind2  10977  bdcvv  11186  bdsnss  11202  bdop  11204  bj-vprc  11225  bdinex1g  11230  bdssexg  11233  bj-inex  11236  bj-zfpair2  11239  bj-uniexg  11247  bdunexb  11249  bj-unexg  11250  bj-indint  11264  bj-ssom  11269  bj-om  11270  bj-2inf  11271  bj-bdfindis  11280  bj-nn0suc0  11283  bj-nnelirr  11286  bj-inf2vnlem1  11303  bj-inf2vnlem2  11304  bj-omex2  11310  bj-nn0sucALT  11311  bj-findis  11312  ss1oel2o  11326  nninfsellemeq  11344  exmidsbthrlem  11350