Theorem vex 2815

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

Syntax hints:   ∈ wcel 2203  Vcvv 2812

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2814

This theorem is referenced by:  elv  2816  elvd  2817  el2v  2818  isset  2819  eqvisset  2823  ralv  2830  rexv  2831  reuv  2832  rmov  2833  rabab  2834  sbhypf  2863  ceqex  2943  ralab  2976  rexab  2978  mo2icl  2995  reu8  3012  csbvarg  3165  csbiebg  3180  sbcnestgf  3189  sbnfc2  3198  ddifnel  3349  ddifstab  3350  csbing  3427  unssdif  3455  unssin  3459  inssun  3460  invdif  3462  vn0  3518  vn0m  3519  eqv  3527  abvor0dc  3531  sbss  3616  velpw  3675  elpwg  3676  velsn  3705  vsnid  3720  exsnrex  3730  dftp2  3737  prmg  3813  prnzg  3816  snssgOLD  3829  difprsnss  3831  sneqrg  3865  preq12bg  3876  pwprss  3909  pwtpss  3910  pwv  3912  unipr  3927  uniprg  3928  unisng  3930  elintg  3956  elintrabg  3961  intss1  3963  ssint  3964  intmin  3968  intss  3969  intssunim  3970  intmin4  3976  intab  3977  intun  3979  intpr  3980  intprg  3981  uniintsnr  3984  iinconstm  3999  iuniin  4000  iinss1  4002  dfiin2g  4023  dfiunv2  4026  ssiinf  4040  iinss  4042  iinss2  4043  0iin  4049  iinab  4052  iundif2ss  4056  iindif2m  4058  iinin2m  4059  iinuniss  4073  sspwuni  4075  pwpwab  4078  iinpw  4081  iunpwss  4082  brab1  4156  csbopabg  4187  mptv  4206  trint  4222  vnex  4240  inex1g  4245  ssexg  4248  inteximm  4260  inuni  4266  repizf2  4274  axpweq  4283  bnd2  4285  pwuni  4304  exmidundif  4318  exmidundifim  4319  zfpair2  4322  rext  4330  sspwb  4331  unipw  4332  ssextss  4335  euabex  4340  mss  4341  exss  4342  opth  4352  opthg  4353  copsexg  4359  copsex4g  4362  moop2  4367  euotd  4370  opabid  4373  elopab  4375  opelopabsbALT  4376  opelopabsb  4377  opabm  4398  pwin  4402  pwunss  4403  epelg  4410  epel  4412  pofun  4432  epse  4462  tron  4502  sucel  4530  suctr  4541  vuniex  4558  uniexg  4559  unexb  4562  snnex  4568  pwnex  4569  uniuni  4571  eusvnf  4573  eusvnfb  4574  iunpw  4600  unon  4632  ordunisuc2r  4635  ordtri2or2exmidlem  4647  onsucelsucexmidlem  4650  ordsucunielexmid  4652  elirr  4662  en2lp  4675  dtruex  4680  onintexmid  4694  reg3exmidlemwe  4700  dcextest  4702  finds  4721  finds2  4722  elomssom  4726  limom  4735  0nelxp  4776  opelxp  4778  opeliunxp  4804  elvv  4811  elvvv  4812  elvvuni  4813  xpsspw  4861  relopabiv  4877  relopabi  4879  opabid2  4885  difopab  4887  xpiindim  4891  raliunxp  4895  rexiunxp  4896  ralxpf  4900  rexxpf  4901  relop  4904  cnvco  4939  dfrn2  4942  dfdm4  4947  dmss  4954  dmin  4963  dmiun  4964  dmuni  4965  dm0  4969  dmi  4970  reldm0  4973  reldmm  4974  elreldm  4982  elrnmpt1  5007  dmrnssfld  5019  dmcoss  5026  dmcosseq  5028  opelresg  5044  resieq  5047  dmres  5058  elres  5073  relssres  5075  resopab  5081  resiexg  5082  iss  5083  dfres2  5089  restidsing  5093  dfima2  5102  imadmrn  5110  imai  5117  csbima12g  5122  elimasng  5129  args  5130  epini  5132  iniseg  5133  dfse2  5134  exse2  5135  cotr  5143  issref  5144  cnvsym  5145  intasym  5146  asymref  5147  intirr  5148  brcodir  5149  codir  5150  qfto  5151  poirr2  5154  cnvopab  5163  cnv0  5165  cnvi  5166  cnvdif  5168  rniun  5172  dminss  5176  imainss  5177  inimasn  5179  xpmlem  5182  dmxpss  5192  rnxpid  5196  ssrnres  5204  rninxp  5205  dminxp  5206  cnvcnv3  5211  dfrel2  5212  dmsnm  5227  dmsnopg  5233  cnvcnvsn  5238  dmsnsnsng  5239  cnvsng  5247  elxp4  5249  elxp5  5250  cnvresima  5251  dfco2  5261  dfco2a  5262  cores  5265  resco  5266  imaco  5267  rnco  5268  coiun  5271  co02  5275  coi1  5277  coass  5280  relssdmrn  5282  unielrel  5289  ressn  5302  cnviinm  5303  cnvpom  5304  cnvsom  5305  uniabio  5322  iotaval  5323  iotass  5329  sniota  5342  csbiotag  5344  dffun2  5361  dffun7  5378  dffun8  5379  dffun9  5380  funopg  5385  funssres  5394  funun  5396  funcnvsn  5400  funinsn  5404  funcnv2  5415  funcnv  5416  funcnv3  5417  funcnveq  5418  fun2cnv  5419  funcnvuni  5424  imadif  5435  funimaexglem  5438  isarep1  5441  2elresin  5468  fnres  5474  fcnvres  5549  fconstg  5563  fun11iun  5634  f1osng  5656  dffv3g  5665  fvssunirng  5684  sefvex  5690  fv3  5692  fvres  5693  nfunsn  5706  funimass4  5726  ssimaexg  5738  dmfco  5744  fvopab6  5773  fndmdif  5782  fvelrn  5807  dffo4  5824  f1ompt  5827  fmptco  5842  fsn  5848  fsng  5849  fsn2g  5851  dfmpt  5854  dfmptg  5856  funopsn  5859  funop  5860  funopdmsn  5863  fnressn  5869  fressnfv  5870  fvsng  5879  resfunexg  5904  funfvima3  5919  idref  5928  abrexco  5931  imaiun  5932  dff13  5940  foeqcnvco  5962  f1eqcocnv  5963  fliftcnv  5967  isocnv2  5984  isoini  5990  isose  5993  riotav  6008  csbriotag  6016  acexmidlem2  6046  oprabid  6081  csbov123g  6088  0neqopab  6097  brabvv  6098  dfoprab2  6099  rnoprab  6135  eloprabga  6139  mpov  6142  f1opw  6261  opabex3d  6313  opabex3  6314  ofmres  6328  uchoice  6330  op1stg  6343  op2ndg  6344  1stval2  6348  2ndval2  6349  fo1st  6350  fo2nd  6351  f1stres  6352  f2ndres  6353  fo1stresm  6354  fo2ndresm  6355  xp1st  6358  xp2nd  6359  releldm2  6378  reldm  6379  sbcopeq1a  6380  csbopeq1a  6381  dfoprab3  6384  opabn1stprc  6388  eloprabi  6391  mpomptsx  6392  dmmpossx  6394  fmpox  6395  mpofvex  6400  mpoexxg  6405  fmpoco  6411  df1st2  6414  df2nd2  6415  1stconst  6416  2ndconst  6417  dfmpo  6418  fo2ndf  6422  f1o2ndf1  6423  xporderlem  6426  cnvoprab  6429  f1od2  6430  suppval1  6438  cnvimadfsn  6444  suppimacnvfn  6445  brtpos2  6481  reldmtpos  6483  dmtpos  6486  rntpos  6487  ovtposg  6489  dftpos3  6492  dftpos4  6493  tpostpos  6494  tpossym  6506  tfrlem3  6541  tfrlem5  6544  tfrlem8  6548  tfrlemisucfn  6554  tfrlemisucaccv  6555  tfrlemibxssdm  6557  tfrlemibfn  6558  tfrlemibex  6559  tfrlemi14d  6563  tfrexlem  6564  tfr1onlem3  6568  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfr1onlemres  6579  tfri1dALT  6581  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemres  6592  tfrcl  6594  rdgtfr  6604  rdgruledefgg  6605  rdgivallem  6611  rdgon  6616  rdg0g  6618  frec0g  6627  frecabex  6628  frecabcl  6629  frectfr  6630  freccllem  6632  frecfcllem  6634  frecsuclem  6636  frecrdg  6638  oafnex  6676  sucinc  6677  fnoa  6679  oaexg  6680  omfnex  6681  fnom  6682  omexg  6683  fnoei  6684  oeiexg  6685  oeiv  6688  oacl  6692  omcl  6693  oeicl  6694  oav2  6695  nnsucelsuc  6723  nnsucuniel  6727  ercnv  6787  iserd  6792  eqerlem  6797  eqer  6798  ecdmn0m  6810  erth  6812  qsss  6827  ecid  6831  ecidg  6832  qsid  6833  iinerm  6840  qsel  6845  erovlem  6860  ecopovsym  6864  ecopover  6866  th3qlem2  6871  mapprc  6885  fnmap  6888  fnpm  6889  mapdm0  6896  mapval2  6911  mapsnd  6922  mapsn  6924  mapsncnv  6929  mapsnf1o2  6930  ixpconstg  6941  ixpprc  6953  ixpin  6957  ixpiinm  6958  ixpssmap2g  6961  ixpssmapg  6962  elixpsn  6969  ixpsnf1o  6970  bren  6982  brdomg  6984  domen  6987  domeng  6988  idssen  7015  domssr  7016  ener  7018  domtr  7024  ensn1g  7036  en1  7038  en1bg  7039  fundmen  7046  fundmeng  7047  mapsnend  7051  mapsnen  7052  fiprc  7056  unen  7057  rex2dom  7062  en2m  7065  dom1o  7068  xpsnen  7071  xpsneng  7072  xpcomco  7076  xpcomeng  7078  xpassen  7080  xpdom2  7081  xpdom2g  7082  pw2f1odc  7087  xpf1o  7096  mapen  7098  mapxpen  7100  xpmapenlem  7101  mapunen  7103  ssenen  7104  phplem4  7108  phplem3g  7109  nneneq  7110  php5  7111  phpm  7119  findcard  7144  findcard2  7145  findcard2s  7146  isinfinf  7153  ac6sfi  7154  exmidpw  7167  exmidpweq  7168  exmidpw2en  7171  unfidisj  7181  fiintim  7190  xpfi  7191  fisseneq  7194  ssfirab  7196  mapfi  7213  snexxph  7219  fidcenumlemr  7224  sbthlemi10  7235  isbth  7236  ssfii  7260  fi0  7261  fiss  7263  cnvinfex  7308  eqinfti  7310  infvalti  7312  infglbti  7315  infmoti  7318  ordiso2  7325  djuf1olem  7343  djuss  7360  ctm  7399  ctssdccl  7401  ctssdclemr  7402  finomni  7430  exmidomni  7432  fodjuomnilemdc  7434  nninfwlpoimlemginf  7466  pm54.43  7486  pr2cv1  7491  exmidfodomrlemim  7503  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  finacn  7510  acfun  7513  ccfunen  7574  cc2lem  7576  cc3  7578  acnccim  7582  indpi  7653  dfplpq2  7665  enq0sym  7743  enq0ref  7744  enq0tr  7745  nqnq0pi  7749  nqnq0  7752  mulnnnq0  7761  nqprm  7853  nqprrnd  7854  nqprdisj  7855  nqprloc  7856  nqprl  7862  nqpru  7863  addnqprlemrl  7868  addnqprlemru  7869  addnqprlemfl  7870  addnqprlemfu  7871  mulnqprlemrl  7884  mulnqprlemru  7885  mulnqprlemfl  7886  mulnqprlemfu  7887  ltnqpr  7904  ltnqpri  7905  archpr  7954  cauappcvgprlemladdfu  7965  cauappcvgprlemladdfl  7966  cauappcvgprlem2  7971  caucvgprlemladdfu  7988  caucvgprlem2  7991  caucvgprprlemopu  8010  suplocexprlemmu  8029  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemub  8034  cnm  8143  ltresr  8150  peano1nnnn  8163  peano2nnnn  8164  axcnre  8192  axpre-apti  8196  renfdisj  8329  dfinfre  9226  1nn  9244  peano2nn  9245  indstr  9921  cnref1o  9979  ioof  10300  fzpr  10407  frec2uzrand  10763  frec2uzf1od  10764  frecuzrdgtcl  10770  frecuzrdgfunlem  10777  frecfzennn  10784  seqp1g  10824  seqclg  10830  seqf1og  10879  seqfeq4g  10889  ser3le  10895  hashinfom  11136  hashunlem  11163  hashun  11164  hashxp  11186  hashfibclem  11199  hashfacen  11201  zfz1isolem1  11205  zfz1iso  11206  fundm2domnop0  11213  wrdexb  11229  fnpfx  11362  cats1un  11406  wrdind  11407  wrd2ind  11408  shftfvalg  11496  ovshftex  11497  shftfibg  11498  shftfval  11499  shftfib  11501  shftfn  11502  2shfti  11509  shftvalg  11514  shftval4g  11515  maxabslemval  11886  fimaxre2  11905  xrmaxiflemval  11928  fclim  11972  climshft  11982  zsumdc  12063  fsum3  12066  fsum2dlemstep  12113  fsumcnv  12116  fisumcom2  12117  fisum0diag2  12126  fsumconst  12133  modfsummodlemstep  12136  fsumabs  12144  fsumrelem  12150  fsumiun  12156  ntrivcvgap  12227  fprod2dlemstep  12301  fprodcnv  12304  fprodcom2fi  12305  fprodmodd  12320  nninfct  12730  algrf  12735  qredeu  12787  isprm2  12807  prmind2  12810  4sqlemafi  13086  4sqlem12  13093  ennnfonelemex  13154  ennnfonelemrn  13159  exmidunben  13166  ctinfom  13168  ctinf  13170  qnnen  13171  enctlem  13172  ctiunctlemfo  13179  slotslfn  13227  setscomd  13242  restfn  13445  elrest  13448  ptex  13466  prdsex  13471  prdsvallem  13474  prdsval  13475  prdsbaslemss  13476  prdsbas  13478  imasex  13507  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  imasaddfnlemg  13516  fnpr2ob  13542  ismgm  13559  plusffng  13567  fn0g  13577  fngsum  13590  gsumsplit1r  13600  gsumprval  13601  issgrp  13605  ismnddef  13620  gsumfzz  13697  gsumfzcl  13701  mulgnngsum  13833  subgintm  13904  releqgg  13926  eqgex  13927  eqgfval  13928  eqgval  13929  isghm  13949  fnmgp  14055  isrng  14067  isring  14133  ringn0  14193  opprrngbg  14211  opprsubgg  14217  opprunitd  14244  dfrhm2  14288  rhmex  14291  opprsubrngg  14345  subrngintm  14346  subrngpropd  14350  subrgpropd  14387  isdomn  14404  opprdomnbg  14409  scaffng  14444  rmodislmodlem  14485  rmodislmod  14486  lssex  14489  lsssn0  14505  lss1d  14518  lssintclm  14519  ellspsn  14552  rlmfn  14588  isridl  14639  blfn  14686  mopnset  14687  metuex  14690  znval  14771  znleval  14788  psrval  14801  fnpsr  14802  mplvalcoe  14832  fnmpl  14835  bastg  14913  distop  14937  topnex  14938  epttop  14942  tgrest  15021  resttopon  15023  restco  15026  cnrest2  15088  cnptopresti  15090  cnptoprest  15091  cnptoprest2  15092  txuni2  15108  txbas  15110  eltx  15111  txcnp  15123  txcnmpt  15125  txrest  15128  txdis1cn  15130  txlm  15131  cnmpt1st  15140  cnmpt2nd  15141  txhmeo  15171  txswaphmeolem  15172  xmetec  15289  metrest  15358  reldvg  15531  dvfgg  15540  dvcj  15561  dvmptfsum  15577  elply2  15587  pilem3  15635  lgsquadlem1  15937  lgsquadlem2  15938  upgrex  16085  upgr1een  16106  umgredg  16127  umgredgnlp  16134  usgredgreu  16198  uspgredg2vtxeu  16200  ushgredgedg  16208  ushgredgedgloop  16210  griedg0ssusgr  16233  uhgrspansubgrlem  16258  upgrspanop  16265  umgrspanop  16266  usgrspanop  16267  wlkvtxiedg  16327  wlkvtxiedgg  16328  wlk1walkdom  16341  eulerpathum  16463  depindlem1  16488  bdcvv  16614  bdsnss  16630  bdop  16632  bj-vprc  16653  bdinex1g  16658  bdssexg  16661  bj-inex  16664  bj-zfpair2  16667  bj-uniexg  16675  bdunexb  16677  bj-unexg  16678  bj-indint  16688  bj-ssom  16693  bj-om  16694  bj-2inf  16695  bj-bdfindis  16704  bj-nn0suc0  16707  bj-nnelirr  16710  bj-inf2vnlem1  16727  bj-inf2vnlem2  16728  bj-omex2  16734  bj-nn0sucALT  16735  bj-findis  16736  ss1oel2o  16748  domomsubct  16762  pw1nct  16764  nninfsellemeq  16779  exmidsbthrlem  16789  gfsumval  16848