Theorem vex 2776

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

Syntax hints:   ∈ wcel 2177  Vcvv 2773

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  elv  2777  elvd  2778  isset  2779  eqvisset  2783  ralv  2790  rexv  2791  reuv  2792  rmov  2793  rabab  2794  sbhypf  2823  ceqex  2901  ralab  2934  rexab  2936  mo2icl  2953  reu8  2970  csbvarg  3122  csbiebg  3137  sbcnestgf  3146  sbnfc2  3155  ddifnel  3305  ddifstab  3306  csbing  3381  unssdif  3409  unssin  3413  inssun  3414  invdif  3416  vn0  3472  vn0m  3473  eqv  3481  abvor0dc  3485  sbss  3569  velpw  3624  elpwg  3625  velsn  3651  vsnid  3666  exsnrex  3676  dftp2  3683  prmg  3756  prnzg  3759  snssgOLD  3771  difprsnss  3773  sneqrg  3805  preq12bg  3816  pwprss  3848  pwtpss  3849  pwv  3851  unipr  3866  uniprg  3867  unisng  3869  elintg  3895  elintrabg  3900  intss1  3902  ssint  3903  intmin  3907  intss  3908  intssunim  3909  intmin4  3915  intab  3916  intun  3918  intpr  3919  intprg  3920  uniintsnr  3923  iinconstm  3938  iuniin  3939  iinss1  3941  dfiin2g  3962  dfiunv2  3965  ssiinf  3979  iinss  3981  iinss2  3982  0iin  3988  iinab  3991  iundif2ss  3995  iindif2m  3997  iinin2m  3998  iinuniss  4012  sspwuni  4014  pwpwab  4017  iinpw  4020  iunpwss  4021  brab1  4095  csbopabg  4126  mptv  4145  trint  4161  vnex  4179  inex1g  4184  ssexg  4187  inteximm  4197  inuni  4203  repizf2  4210  axpweq  4219  bnd2  4221  pwuni  4240  exmidundif  4254  exmidundifim  4255  zfpair2  4258  rext  4263  sspwb  4264  unipw  4265  ssextss  4268  euabex  4273  mss  4274  exss  4275  opth  4285  opthg  4286  copsexg  4292  copsex4g  4295  moop2  4300  euotd  4303  opabid  4306  elopab  4308  opelopabsbALT  4309  opelopabsb  4310  opabm  4331  pwin  4333  pwunss  4334  epelg  4341  epel  4343  pofun  4363  epse  4393  tron  4433  sucel  4461  suctr  4472  vuniex  4489  uniexg  4490  unexb  4493  snnex  4499  pwnex  4500  uniuni  4502  eusvnf  4504  eusvnfb  4505  iunpw  4531  unon  4563  ordunisuc2r  4566  ordtri2or2exmidlem  4578  onsucelsucexmidlem  4581  ordsucunielexmid  4583  elirr  4593  en2lp  4606  dtruex  4611  onintexmid  4625  reg3exmidlemwe  4631  dcextest  4633  finds  4652  finds2  4653  elomssom  4657  limom  4666  0nelxp  4707  opelxp  4709  opeliunxp  4734  elvv  4741  elvvv  4742  elvvuni  4743  xpsspw  4791  relopabiv  4805  relopabi  4807  opabid2  4813  difopab  4815  xpiindim  4819  raliunxp  4823  rexiunxp  4824  ralxpf  4828  rexxpf  4829  relop  4832  cnvco  4867  dfrn2  4870  dfdm4  4875  dmss  4882  dmin  4891  dmiun  4892  dmuni  4893  dm0  4897  dmi  4898  reldm0  4901  elreldm  4909  elrnmpt1  4934  dmrnssfld  4946  dmcoss  4953  dmcosseq  4955  opelresg  4971  resieq  4974  dmres  4985  elres  5000  relssres  5002  resopab  5008  resiexg  5009  iss  5010  dfres2  5016  restidsing  5020  dfima2  5029  imadmrn  5037  imai  5043  csbima12g  5048  elimasng  5055  args  5056  epini  5058  iniseg  5059  dfse2  5060  exse2  5061  cotr  5069  issref  5070  cnvsym  5071  intasym  5072  asymref  5073  intirr  5074  brcodir  5075  codir  5076  qfto  5077  poirr2  5080  cnvopab  5089  cnv0  5091  cnvi  5092  cnvdif  5094  rniun  5098  dminss  5102  imainss  5103  inimasn  5105  xpmlem  5108  dmxpss  5118  rnxpid  5122  ssrnres  5130  rninxp  5131  dminxp  5132  cnvcnv3  5137  dfrel2  5138  dmsnm  5153  dmsnopg  5159  cnvcnvsn  5164  dmsnsnsng  5165  cnvsng  5173  elxp4  5175  elxp5  5176  cnvresima  5177  dfco2  5187  dfco2a  5188  cores  5191  resco  5192  imaco  5193  rnco  5194  coiun  5197  co02  5201  coi1  5203  coass  5206  relssdmrn  5208  unielrel  5215  ressn  5228  cnviinm  5229  cnvpom  5230  cnvsom  5231  uniabio  5247  iotaval  5248  iotass  5254  sniota  5267  csbiotag  5269  dffun2  5286  dffun7  5303  dffun8  5304  dffun9  5305  funopg  5310  funssres  5318  funun  5320  funcnvsn  5324  funinsn  5328  funcnv2  5339  funcnv  5340  funcnv3  5341  funcnveq  5342  fun2cnv  5343  funcnvuni  5348  imadif  5359  funimaexglem  5362  isarep1  5365  2elresin  5392  fnres  5398  fcnvres  5466  fconstg  5479  fun11iun  5550  f1osng  5570  dffv3g  5579  fvssunirng  5598  sefvex  5604  fv3  5606  fvres  5607  nfunsn  5618  funimass4  5636  ssimaexg  5648  dmfco  5654  fvopab6  5683  fndmdif  5692  fvelrn  5718  dffo4  5735  f1ompt  5738  fmptco  5753  fsn  5759  fsng  5760  dfmpt  5764  dfmptg  5766  funopsn  5769  funop  5770  funopdmsn  5771  fnressn  5777  fressnfv  5778  fvsng  5787  resfunexg  5812  funfvima3  5825  idref  5832  abrexco  5835  imaiun  5836  dff13  5844  foeqcnvco  5866  f1eqcocnv  5867  fliftcnv  5871  isocnv2  5888  isoini  5894  isose  5897  riotav  5912  csbriotag  5919  acexmidlem2  5948  oprabid  5983  csbov123g  5990  0neqopab  5997  brabvv  5998  dfoprab2  5999  rnoprab  6035  eloprabga  6039  mpov  6042  f1opw  6160  opabex3d  6213  opabex3  6214  ofmres  6228  uchoice  6230  op1stg  6243  op2ndg  6244  1stval2  6248  2ndval2  6249  fo1st  6250  fo2nd  6251  f1stres  6252  f2ndres  6253  fo1stresm  6254  fo2ndresm  6255  xp1st  6258  xp2nd  6259  releldm2  6278  reldm  6279  sbcopeq1a  6280  csbopeq1a  6281  dfoprab3  6284  eloprabi  6289  mpomptsx  6290  dmmpossx  6292  fmpox  6293  mpofvex  6298  mpoexxg  6303  fmpoco  6309  df1st2  6312  df2nd2  6313  1stconst  6314  2ndconst  6315  dfmpo  6316  fo2ndf  6320  f1o2ndf1  6321  xporderlem  6324  cnvoprab  6327  f1od2  6328  brtpos2  6344  reldmtpos  6346  dmtpos  6349  rntpos  6350  ovtposg  6352  dftpos3  6355  dftpos4  6356  tpostpos  6357  tpossym  6369  tfrlem3  6404  tfrlem5  6407  tfrlem8  6411  tfrlemisucfn  6417  tfrlemisucaccv  6418  tfrlemibxssdm  6420  tfrlemibfn  6421  tfrlemibex  6422  tfrlemi14d  6426  tfrexlem  6427  tfr1onlem3  6431  tfr1onlemsucaccv  6434  tfr1onlembxssdm  6436  tfr1onlembfn  6437  tfr1onlemres  6442  tfri1dALT  6444  tfrcllemsucaccv  6447  tfrcllembxssdm  6449  tfrcllembfn  6450  tfrcllemres  6455  tfrcl  6457  rdgtfr  6467  rdgruledefgg  6468  rdgivallem  6474  rdgon  6479  rdg0g  6481  frec0g  6490  frecabex  6491  frecabcl  6492  frectfr  6493  freccllem  6495  frecfcllem  6497  frecsuclem  6499  frecrdg  6501  oafnex  6537  sucinc  6538  fnoa  6540  oaexg  6541  omfnex  6542  fnom  6543  omexg  6544  fnoei  6545  oeiexg  6546  oeiv  6549  oacl  6553  omcl  6554  oeicl  6555  oav2  6556  nnsucelsuc  6584  nnsucuniel  6588  ercnv  6648  iserd  6653  eqerlem  6658  eqer  6659  ecdmn0m  6671  erth  6673  qsss  6688  ecid  6692  ecidg  6693  qsid  6694  iinerm  6701  qsel  6706  erovlem  6721  ecopovsym  6725  ecopover  6727  th3qlem2  6732  mapprc  6746  fnmap  6749  fnpm  6750  mapdm0  6757  mapval2  6772  mapsn  6784  mapsncnv  6789  mapsnf1o2  6790  ixpconstg  6801  ixpprc  6813  ixpin  6817  ixpiinm  6818  ixpssmap2g  6821  ixpssmapg  6822  elixpsn  6829  ixpsnf1o  6830  bren  6842  brdomg  6844  domen  6847  domeng  6848  idssen  6875  domssr  6876  ener  6878  domtr  6884  ensn1g  6896  en1  6898  en1bg  6899  fundmen  6905  fundmeng  6906  mapsnen  6910  fiprc  6914  unen  6915  rex2dom  6917  xpsnen  6923  xpsneng  6924  xpcomco  6928  xpcomeng  6930  xpassen  6932  xpdom2  6933  xpdom2g  6934  pw2f1odc  6939  xpf1o  6948  mapen  6950  mapxpen  6952  xpmapenlem  6953  ssenen  6955  phplem4  6959  phplem3g  6960  nneneq  6961  php5  6962  phpm  6969  findcard  6992  findcard2  6993  findcard2s  6994  isinfinf  7001  ac6sfi  7002  exmidpw  7012  exmidpweq  7013  exmidpw2en  7016  unfidisj  7026  fiintim  7035  xpfi  7036  fisseneq  7038  ssfirab  7040  snexxph  7059  fidcenumlemr  7064  sbthlemi10  7075  isbth  7076  ssfii  7083  fi0  7084  fiss  7086  cnvinfex  7127  eqinfti  7129  infvalti  7131  infglbti  7134  infmoti  7137  ordiso2  7144  djuf1olem  7162  djuss  7179  ctm  7218  ctssdccl  7220  ctssdclemr  7221  finomni  7249  exmidomni  7251  fodjuomnilemdc  7253  nninfwlpoimlemginf  7285  pm54.43  7305  exmidfodomrlemim  7316  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  finacn  7323  acfun  7326  ccfunen  7383  cc2lem  7385  cc3  7387  acnccim  7391  indpi  7462  dfplpq2  7474  enq0sym  7552  enq0ref  7553  enq0tr  7554  nqnq0pi  7558  nqnq0  7561  mulnnnq0  7570  nqprm  7662  nqprrnd  7663  nqprdisj  7664  nqprloc  7665  nqprl  7671  nqpru  7672  addnqprlemrl  7677  addnqprlemru  7678  addnqprlemfl  7679  addnqprlemfu  7680  mulnqprlemrl  7693  mulnqprlemru  7694  mulnqprlemfl  7695  mulnqprlemfu  7696  ltnqpr  7713  ltnqpri  7714  archpr  7763  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  cauappcvgprlem2  7780  caucvgprlemladdfu  7797  caucvgprlem2  7800  caucvgprprlemopu  7819  suplocexprlemmu  7838  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  cnm  7952  ltresr  7959  peano1nnnn  7972  peano2nnnn  7973  axcnre  8001  axpre-apti  8005  renfdisj  8139  dfinfre  9036  1nn  9054  peano2nn  9055  indstr  9721  cnref1o  9779  ioof  10100  fzpr  10206  frec2uzrand  10557  frec2uzf1od  10558  frecuzrdgtcl  10564  frecuzrdgfunlem  10571  frecfzennn  10578  seqp1g  10618  seqclg  10624  seqf1og  10673  seqfeq4g  10683  ser3le  10689  hashinfom  10930  hashunlem  10956  hashun  10957  hashxp  10978  hashfacen  10988  zfz1isolem1  10992  zfz1iso  10993  fundm2domnop0  10997  wrdexb  11013  shftfvalg  11173  ovshftex  11174  shftfibg  11175  shftfval  11176  shftfib  11178  shftfn  11179  2shfti  11186  shftvalg  11191  shftval4g  11192  maxabslemval  11563  fimaxre2  11582  xrmaxiflemval  11605  fclim  11649  climshft  11659  zsumdc  11739  fsum3  11742  fsum2dlemstep  11789  fsumcnv  11792  fisumcom2  11793  fisum0diag2  11802  fsumconst  11809  modfsummodlemstep  11812  fsumabs  11820  fsumrelem  11826  fsumiun  11832  ntrivcvgap  11903  fprod2dlemstep  11977  fprodcnv  11980  fprodcom2fi  11981  fprodmodd  11996  nninfct  12406  algrf  12411  qredeu  12463  isprm2  12483  prmind2  12486  4sqlemafi  12762  4sqlem12  12769  ennnfonelemex  12829  ennnfonelemrn  12834  exmidunben  12841  ctinfom  12843  ctinf  12845  qnnen  12846  enctlem  12847  ctiunctlemfo  12854  slotslfn  12902  setscomd  12917  restfn  13119  elrest  13122  ptex  13140  prdsex  13145  prdsvallem  13148  prdsval  13149  prdsbaslemss  13150  prdsbas  13152  imasex  13181  imasival  13182  imasbas  13183  imasplusg  13184  imasmulr  13185  imasaddfnlemg  13190  fnpr2ob  13216  ismgm  13233  plusffng  13241  fn0g  13251  fngsum  13264  gsumsplit1r  13274  gsumprval  13275  issgrp  13279  ismnddef  13294  gsumfzz  13371  gsumfzcl  13375  mulgnngsum  13507  subgintm  13578  releqgg  13600  eqgex  13601  eqgfval  13602  eqgval  13603  isghm  13623  fnmgp  13728  isrng  13740  isring  13806  ringn0  13866  opprrngbg  13884  opprsubgg  13890  opprunitd  13916  dfrhm2  13960  rhmex  13963  opprsubrngg  14017  subrngintm  14018  subrngpropd  14022  subrgpropd  14059  isdomn  14075  opprdomnbg  14080  scaffng  14115  rmodislmodlem  14156  rmodislmod  14157  lssex  14160  lsssn0  14176  lss1d  14189  lssintclm  14190  ellspsn  14223  rlmfn  14259  isridl  14310  blfn  14357  mopnset  14358  metuex  14361  znval  14442  znleval  14459  psrval  14472  fnpsr  14473  mplvalcoe  14496  fnmpl  14499  bastg  14577  distop  14601  topnex  14602  epttop  14606  tgrest  14685  resttopon  14687  restco  14690  cnrest2  14752  cnptopresti  14754  cnptoprest  14755  cnptoprest2  14756  txuni2  14772  txbas  14774  eltx  14775  txcnp  14787  txcnmpt  14789  txrest  14792  txdis1cn  14794  txlm  14795  cnmpt1st  14804  cnmpt2nd  14805  txhmeo  14835  txswaphmeolem  14836  xmetec  14953  metrest  15022  reldvg  15195  dvfgg  15204  dvcj  15225  dvmptfsum  15241  elply2  15251  pilem3  15299  lgsquadlem1  15598  lgsquadlem2  15599  bdcvv  15867  bdsnss  15883  bdop  15885  bj-vprc  15906  bdinex1g  15911  bdssexg  15914  bj-inex  15917  bj-zfpair2  15920  bj-uniexg  15928  bdunexb  15930  bj-unexg  15931  bj-indint  15941  bj-ssom  15946  bj-om  15947  bj-2inf  15948  bj-bdfindis  15957  bj-nn0suc0  15960  bj-nnelirr  15963  bj-inf2vnlem1  15980  bj-inf2vnlem2  15981  bj-omex2  15987  bj-nn0sucALT  15988  bj-findis  15989  ss1oel2o  16002  domomsubct  16012  pw1nct  16014  nninfsellemeq  16025  exmidsbthrlem  16035