Theorem vex 2766

Description: All setvar variables are sets (see isset 2769). 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 1715	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2765	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2307	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 146	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2167  Vcvv 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elv  2767  elvd  2768  isset  2769  eqvisset  2773  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rabab  2784  sbhypf  2813  ceqex  2891  ralab  2924  rexab  2926  mo2icl  2943  reu8  2960  csbvarg  3112  csbiebg  3127  sbcnestgf  3136  sbnfc2  3145  ddifnel  3295  ddifstab  3296  csbing  3371  unssdif  3399  unssin  3403  inssun  3404  invdif  3406  vn0  3462  vn0m  3463  eqv  3471  abvor0dc  3475  sbss  3559  velpw  3613  elpwg  3614  velsn  3640  vsnid  3655  exsnrex  3665  dftp2  3672  prmg  3744  prnzg  3747  snssgOLD  3759  difprsnss  3761  sneqrg  3793  preq12bg  3804  pwprss  3836  pwtpss  3837  pwv  3839  unipr  3854  uniprg  3855  unisng  3857  elintg  3883  elintrabg  3888  intss1  3890  ssint  3891  intmin  3895  intss  3896  intssunim  3897  intmin4  3903  intab  3904  intun  3906  intpr  3907  intprg  3908  uniintsnr  3911  iinconstm  3926  iuniin  3927  iinss1  3929  dfiin2g  3950  dfiunv2  3953  ssiinf  3967  iinss  3969  iinss2  3970  0iin  3976  iinab  3979  iundif2ss  3983  iindif2m  3985  iinin2m  3986  iinuniss  4000  sspwuni  4002  pwpwab  4005  iinpw  4008  iunpwss  4009  brab1  4081  csbopabg  4112  mptv  4131  trint  4147  vnex  4165  inex1g  4170  ssexg  4173  inteximm  4183  inuni  4189  repizf2  4196  axpweq  4205  bnd2  4207  pwuni  4226  exmidundif  4240  exmidundifim  4241  zfpair2  4244  rext  4249  sspwb  4250  unipw  4251  ssextss  4254  euabex  4259  mss  4260  exss  4261  opth  4271  opthg  4272  copsexg  4278  copsex4g  4281  moop2  4285  euotd  4288  opabid  4291  elopab  4293  opelopabsbALT  4294  opelopabsb  4295  opabm  4316  pwin  4318  pwunss  4319  epelg  4326  epel  4328  pofun  4348  epse  4378  tron  4418  sucel  4446  suctr  4457  vuniex  4474  uniexg  4475  unexb  4478  snnex  4484  pwnex  4485  uniuni  4487  eusvnf  4489  eusvnfb  4490  iunpw  4516  unon  4548  ordunisuc2r  4551  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsucunielexmid  4568  elirr  4578  en2lp  4591  dtruex  4596  onintexmid  4610  reg3exmidlemwe  4616  dcextest  4618  finds  4637  finds2  4638  elomssom  4642  limom  4651  0nelxp  4692  opelxp  4694  opeliunxp  4719  elvv  4726  elvvv  4727  elvvuni  4728  xpsspw  4776  relopabiv  4790  relopabi  4792  opabid2  4798  difopab  4800  xpiindim  4804  raliunxp  4808  rexiunxp  4809  ralxpf  4813  rexxpf  4814  relop  4817  cnvco  4852  dfrn2  4855  dfdm4  4859  dmss  4866  dmin  4875  dmiun  4876  dmuni  4877  dm0  4881  dmi  4882  reldm0  4885  elreldm  4893  elrnmpt1  4918  dmrnssfld  4930  dmcoss  4936  dmcosseq  4938  opelresg  4954  resieq  4957  dmres  4968  elres  4983  relssres  4985  resopab  4991  resiexg  4992  iss  4993  dfres2  4999  restidsing  5003  dfima2  5012  imadmrn  5020  imai  5026  csbima12g  5031  elimasng  5038  args  5039  epini  5041  iniseg  5042  dfse2  5043  exse2  5044  cotr  5052  issref  5053  cnvsym  5054  intasym  5055  asymref  5056  intirr  5057  brcodir  5058  codir  5059  qfto  5060  poirr2  5063  cnvopab  5072  cnv0  5074  cnvi  5075  cnvdif  5077  rniun  5081  dminss  5085  imainss  5086  inimasn  5088  xpmlem  5091  dmxpss  5101  rnxpid  5105  ssrnres  5113  rninxp  5114  dminxp  5115  cnvcnv3  5120  dfrel2  5121  dmsnm  5136  dmsnopg  5142  cnvcnvsn  5147  dmsnsnsng  5148  cnvsng  5156  elxp4  5158  elxp5  5159  cnvresima  5160  dfco2  5170  dfco2a  5171  cores  5174  resco  5175  imaco  5176  rnco  5177  coiun  5180  co02  5184  coi1  5186  coass  5189  relssdmrn  5191  unielrel  5198  ressn  5211  cnviinm  5212  cnvpom  5213  cnvsom  5214  uniabio  5230  iotaval  5231  iotass  5237  sniota  5250  csbiotag  5252  dffun2  5269  dffun7  5286  dffun8  5287  dffun9  5288  funopg  5293  funssres  5301  funun  5303  funcnvsn  5304  funinsn  5308  funcnv2  5319  funcnv  5320  funcnv3  5321  funcnveq  5322  fun2cnv  5323  funcnvuni  5328  imadif  5339  funimaexglem  5342  isarep1  5345  2elresin  5370  fnres  5375  fcnvres  5442  fconstg  5455  fun11iun  5526  f1osng  5546  dffv3g  5555  fvssunirng  5574  sefvex  5580  fv3  5582  fvres  5583  nfunsn  5594  funimass4  5612  ssimaexg  5624  dmfco  5630  fvopab6  5659  fndmdif  5668  fvelrn  5694  dffo4  5711  f1ompt  5714  fmptco  5729  fsn  5735  fsng  5736  dfmpt  5740  dfmptg  5742  fnressn  5749  fressnfv  5750  fvsng  5759  resfunexg  5784  funfvima3  5797  idref  5804  abrexco  5807  imaiun  5808  dff13  5816  foeqcnvco  5838  f1eqcocnv  5839  fliftcnv  5843  isocnv2  5860  isoini  5866  isose  5869  riotav  5884  csbriotag  5891  acexmidlem2  5920  oprabid  5955  csbov123g  5961  0neqopab  5968  brabvv  5969  dfoprab2  5970  rnoprab  6006  eloprabga  6010  mpov  6013  f1opw  6131  opabex3d  6179  opabex3  6180  ofmres  6194  uchoice  6196  op1stg  6209  op2ndg  6210  1stval2  6214  2ndval2  6215  fo1st  6216  fo2nd  6217  f1stres  6218  f2ndres  6219  fo1stresm  6220  fo2ndresm  6221  xp1st  6224  xp2nd  6225  releldm2  6244  reldm  6245  sbcopeq1a  6246  csbopeq1a  6247  dfoprab3  6250  eloprabi  6255  mpomptsx  6256  dmmpossx  6258  fmpox  6259  mpofvex  6264  mpoexxg  6269  fmpoco  6275  df1st2  6278  df2nd2  6279  1stconst  6280  2ndconst  6281  dfmpo  6282  fo2ndf  6286  f1o2ndf1  6287  xporderlem  6290  cnvoprab  6293  f1od2  6294  brtpos2  6310  reldmtpos  6312  dmtpos  6315  rntpos  6316  ovtposg  6318  dftpos3  6321  dftpos4  6322  tpostpos  6323  tpossym  6335  tfrlem3  6370  tfrlem5  6373  tfrlem8  6377  tfrlemisucfn  6383  tfrlemisucaccv  6384  tfrlemibxssdm  6386  tfrlemibfn  6387  tfrlemibex  6388  tfrlemi14d  6392  tfrexlem  6393  tfr1onlem3  6397  tfr1onlemsucaccv  6400  tfr1onlembxssdm  6402  tfr1onlembfn  6403  tfr1onlemres  6408  tfri1dALT  6410  tfrcllemsucaccv  6413  tfrcllembxssdm  6415  tfrcllembfn  6416  tfrcllemres  6421  tfrcl  6423  rdgtfr  6433  rdgruledefgg  6434  rdgivallem  6440  rdgon  6445  rdg0g  6447  frec0g  6456  frecabex  6457  frecabcl  6458  frectfr  6459  freccllem  6461  frecfcllem  6463  frecsuclem  6465  frecrdg  6467  oafnex  6503  sucinc  6504  fnoa  6506  oaexg  6507  omfnex  6508  fnom  6509  omexg  6510  fnoei  6511  oeiexg  6512  oeiv  6515  oacl  6519  omcl  6520  oeicl  6521  oav2  6522  nnsucelsuc  6550  nnsucuniel  6554  ercnv  6614  iserd  6619  eqerlem  6624  eqer  6625  ecdmn0m  6637  erth  6639  qsss  6654  ecid  6658  ecidg  6659  qsid  6660  iinerm  6667  qsel  6672  erovlem  6687  ecopovsym  6691  ecopover  6693  th3qlem2  6698  mapprc  6712  fnmap  6715  fnpm  6716  mapdm0  6723  mapval2  6738  mapsn  6750  mapsncnv  6755  mapsnf1o2  6756  ixpconstg  6767  ixpprc  6779  ixpin  6783  ixpiinm  6784  ixpssmap2g  6787  ixpssmapg  6788  elixpsn  6795  ixpsnf1o  6796  bren  6807  brdomg  6808  domen  6811  domeng  6812  idssen  6837  ener  6839  domtr  6845  ensn1g  6857  en1  6859  en1bg  6860  fundmen  6866  fundmeng  6867  mapsnen  6871  fiprc  6875  unen  6876  xpsnen  6881  xpsneng  6882  xpcomco  6886  xpcomeng  6888  xpassen  6890  xpdom2  6891  xpdom2g  6892  pw2f1odc  6897  xpf1o  6906  mapen  6908  mapxpen  6910  xpmapenlem  6911  ssenen  6913  phplem4  6917  phplem3g  6918  nneneq  6919  php5  6920  phpm  6927  findcard  6950  findcard2  6951  findcard2s  6952  isinfinf  6959  ac6sfi  6960  exmidpw  6970  exmidpweq  6971  exmidpw2en  6974  unfidisj  6984  fiintim  6993  xpfi  6994  fisseneq  6996  ssfirab  6998  snexxph  7017  fidcenumlemr  7022  sbthlemi10  7033  isbth  7034  ssfii  7041  fi0  7042  fiss  7044  cnvinfex  7085  eqinfti  7087  infvalti  7089  infglbti  7092  infmoti  7095  ordiso2  7102  djuf1olem  7120  djuss  7137  ctm  7176  ctssdccl  7178  ctssdclemr  7179  finomni  7207  exmidomni  7209  fodjuomnilemdc  7211  nninfwlpoimlemginf  7243  pm54.43  7259  exmidfodomrlemim  7270  exmidfodomrlemr  7271  exmidfodomrlemrALT  7272  acfun  7276  ccfunen  7333  cc2lem  7335  cc3  7337  indpi  7411  dfplpq2  7423  enq0sym  7501  enq0ref  7502  enq0tr  7503  nqnq0pi  7507  nqnq0  7510  mulnnnq0  7519  nqprm  7611  nqprrnd  7612  nqprdisj  7613  nqprloc  7614  nqprl  7620  nqpru  7621  addnqprlemrl  7626  addnqprlemru  7627  addnqprlemfl  7628  addnqprlemfu  7629  mulnqprlemrl  7642  mulnqprlemru  7643  mulnqprlemfl  7644  mulnqprlemfu  7645  ltnqpr  7662  ltnqpri  7663  archpr  7712  cauappcvgprlemladdfu  7723  cauappcvgprlemladdfl  7724  cauappcvgprlem2  7729  caucvgprlemladdfu  7746  caucvgprlem2  7749  caucvgprprlemopu  7768  suplocexprlemmu  7787  suplocexprlemdisj  7789  suplocexprlemloc  7790  suplocexprlemub  7792  cnm  7901  ltresr  7908  peano1nnnn  7921  peano2nnnn  7922  axcnre  7950  axpre-apti  7954  renfdisj  8088  dfinfre  8985  1nn  9003  peano2nn  9004  indstr  9669  cnref1o  9727  ioof  10048  fzpr  10154  frec2uzrand  10499  frec2uzf1od  10500  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  frecfzennn  10520  seqp1g  10560  seqclg  10566  seqf1og  10615  seqfeq4g  10625  ser3le  10631  hashinfom  10872  hashunlem  10898  hashun  10899  hashxp  10920  hashfacen  10930  zfz1isolem1  10934  zfz1iso  10935  wrdexb  10949  shftfvalg  10985  ovshftex  10986  shftfibg  10987  shftfval  10988  shftfib  10990  shftfn  10991  2shfti  10998  shftvalg  11003  shftval4g  11004  maxabslemval  11375  fimaxre2  11394  xrmaxiflemval  11417  fclim  11461  climshft  11471  zsumdc  11551  fsum3  11554  fsum2dlemstep  11601  fsumcnv  11604  fisumcom2  11605  fisum0diag2  11614  fsumconst  11621  modfsummodlemstep  11624  fsumabs  11632  fsumrelem  11638  fsumiun  11644  ntrivcvgap  11715  fprod2dlemstep  11789  fprodcnv  11792  fprodcom2fi  11793  fprodmodd  11808  nninfct  12218  algrf  12223  qredeu  12275  isprm2  12295  prmind2  12298  4sqlemafi  12574  4sqlem12  12581  ennnfonelemex  12641  ennnfonelemrn  12646  exmidunben  12653  ctinfom  12655  ctinf  12657  qnnen  12658  enctlem  12659  ctiunctlemfo  12666  slotslfn  12714  setscomd  12729  restfn  12924  elrest  12927  ptex  12945  prdsex  12950  imasex  12958  imasival  12959  imasbas  12960  imasplusg  12961  imasmulr  12962  imasaddfnlemg  12967  fnpr2ob  12993  ismgm  13010  plusffng  13018  fn0g  13028  fngsum  13041  gsumsplit1r  13051  gsumprval  13052  issgrp  13056  ismnddef  13069  gsumfzz  13137  gsumfzcl  13141  mulgnngsum  13267  subgintm  13338  releqgg  13360  eqgex  13361  eqgfval  13362  eqgval  13363  isghm  13383  fnmgp  13488  isrng  13500  isring  13566  ringn0  13626  opprrngbg  13644  opprsubgg  13650  opprunitd  13676  dfrhm2  13720  rhmex  13723  opprsubrngg  13777  subrngintm  13778  subrngpropd  13782  subrgpropd  13819  isdomn  13835  opprdomnbg  13840  scaffng  13875  rmodislmodlem  13916  rmodislmod  13917  lssex  13920  lsssn0  13936  lss1d  13949  lssintclm  13950  ellspsn  13983  rlmfn  14019  isridl  14070  blfn  14117  mopnset  14118  metuex  14121  znval  14202  znleval  14219  psrval  14230  fnpsr  14231  bastg  14307  distop  14331  topnex  14332  epttop  14336  tgrest  14415  resttopon  14417  restco  14420  cnrest2  14482  cnptopresti  14484  cnptoprest  14485  cnptoprest2  14486  txuni2  14502  txbas  14504  eltx  14505  txcnp  14517  txcnmpt  14519  txrest  14522  txdis1cn  14524  txlm  14525  cnmpt1st  14534  cnmpt2nd  14535  txhmeo  14565  txswaphmeolem  14566  xmetec  14683  metrest  14752  reldvg  14925  dvfgg  14934  dvcj  14955  dvmptfsum  14971  elply2  14981  pilem3  15029  lgsquadlem1  15328  lgsquadlem2  15329  bdcvv  15513  bdsnss  15529  bdop  15531  bj-vprc  15552  bdinex1g  15557  bdssexg  15560  bj-inex  15563  bj-zfpair2  15566  bj-uniexg  15574  bdunexb  15576  bj-unexg  15577  bj-indint  15587  bj-ssom  15592  bj-om  15593  bj-2inf  15594  bj-bdfindis  15603  bj-nn0suc0  15606  bj-nnelirr  15609  bj-inf2vnlem1  15626  bj-inf2vnlem2  15627  bj-omex2  15633  bj-nn0sucALT  15634  bj-findis  15635  ss1oel2o  15648  pw1nct  15657  nninfsellemeq  15668  exmidsbthrlem  15676