Theorem vex 2752

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

Syntax hints:   ∈ wcel 2158  Vcvv 2749

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-v 2751

This theorem is referenced by:  elv  2753  elvd  2754  isset  2755  eqvisset  2759  ralv  2766  rexv  2767  reuv  2768  rmov  2769  rabab  2770  sbhypf  2798  ceqex  2876  ralab  2909  rexab  2911  mo2icl  2928  reu8  2945  csbvarg  3097  csbiebg  3111  sbcnestgf  3120  sbnfc2  3129  ddifnel  3278  ddifstab  3279  csbing  3354  unssdif  3382  unssin  3386  inssun  3387  invdif  3389  vn0  3445  vn0m  3446  eqv  3454  abvor0dc  3458  sbss  3543  velpw  3594  elpwg  3595  velsn  3621  vsnid  3636  exsnrex  3646  dftp2  3653  prmg  3725  prnzg  3728  snssgOLD  3740  difprsnss  3742  sneqrg  3774  preq12bg  3785  pwprss  3817  pwtpss  3818  pwv  3820  unipr  3835  uniprg  3836  unisng  3838  elintg  3864  elintrabg  3869  intss1  3871  ssint  3872  intmin  3876  intss  3877  intssunim  3878  intmin4  3884  intab  3885  intun  3887  intpr  3888  intprg  3889  uniintsnr  3892  iinconstm  3907  iuniin  3908  iinss1  3910  dfiin2g  3931  dfiunv2  3934  ssiinf  3948  iinss  3950  iinss2  3951  0iin  3957  iinab  3960  iundif2ss  3964  iindif2m  3966  iinin2m  3967  iinuniss  3981  sspwuni  3983  pwpwab  3986  iinpw  3989  iunpwss  3990  brab1  4062  csbopabg  4093  mptv  4112  trint  4128  vnex  4146  inex1g  4151  ssexg  4154  inteximm  4161  inuni  4167  repizf2  4174  axpweq  4183  bnd2  4185  pwuni  4204  exmidundif  4218  exmidundifim  4219  zfpair2  4222  rext  4227  sspwb  4228  unipw  4229  ssextss  4232  euabex  4237  mss  4238  exss  4239  opth  4249  opthg  4250  copsexg  4256  copsex4g  4259  moop2  4263  euotd  4266  opabid  4269  elopab  4270  opelopabsbALT  4271  opelopabsb  4272  opabm  4292  pwin  4294  pwunss  4295  epelg  4302  epel  4304  pofun  4324  epse  4354  tron  4394  sucel  4422  suctr  4433  vuniex  4450  uniexg  4451  unexb  4454  snnex  4460  pwnex  4461  uniuni  4463  eusvnf  4465  eusvnfb  4466  iunpw  4492  unon  4522  ordunisuc2r  4525  ordtri2or2exmidlem  4537  onsucelsucexmidlem  4540  ordsucunielexmid  4542  elirr  4552  en2lp  4565  dtruex  4570  onintexmid  4584  reg3exmidlemwe  4590  dcextest  4592  finds  4611  finds2  4612  elomssom  4616  limom  4625  0nelxp  4666  opelxp  4668  opeliunxp  4693  elvv  4700  elvvv  4701  elvvuni  4702  xpsspw  4750  relopabi  4764  opabid2  4770  difopab  4772  xpiindim  4776  raliunxp  4780  rexiunxp  4781  ralxpf  4785  rexxpf  4786  relop  4789  cnvco  4824  dfrn2  4827  dfdm4  4831  dmss  4838  dmin  4847  dmiun  4848  dmuni  4849  dm0  4853  dmi  4854  reldm0  4857  elreldm  4865  elrnmpt1  4890  dmrnssfld  4902  dmcoss  4908  dmcosseq  4910  opelresg  4926  resieq  4929  dmres  4940  elres  4955  relssres  4957  resopab  4963  resiexg  4964  iss  4965  dfres2  4971  restidsing  4975  dfima2  4984  imadmrn  4992  imai  4996  csbima12g  5001  elimasng  5008  args  5009  epini  5011  iniseg  5012  dfse2  5013  exse2  5014  cotr  5022  issref  5023  cnvsym  5024  intasym  5025  asymref  5026  intirr  5027  brcodir  5028  codir  5029  qfto  5030  poirr2  5033  cnvopab  5042  cnv0  5044  cnvi  5045  cnvdif  5047  rniun  5051  dminss  5055  imainss  5056  inimasn  5058  xpmlem  5061  dmxpss  5071  rnxpid  5075  ssrnres  5083  rninxp  5084  dminxp  5085  cnvcnv3  5090  dfrel2  5091  dmsnm  5106  dmsnopg  5112  cnvcnvsn  5117  dmsnsnsng  5118  cnvsng  5126  elxp4  5128  elxp5  5129  cnvresima  5130  dfco2  5140  dfco2a  5141  cores  5144  resco  5145  imaco  5146  rnco  5147  coiun  5150  co02  5154  coi1  5156  coass  5159  relssdmrn  5161  unielrel  5168  ressn  5181  cnviinm  5182  cnvpom  5183  cnvsom  5184  uniabio  5200  iotaval  5201  iotass  5207  sniota  5219  csbiotag  5221  dffun2  5238  dffun7  5255  dffun8  5256  dffun9  5257  funopg  5262  funssres  5270  funun  5272  funcnvsn  5273  funinsn  5277  funcnv2  5288  funcnv  5289  funcnv3  5290  funcnveq  5291  fun2cnv  5292  funcnvuni  5297  imadif  5308  funimaexglem  5311  isarep1  5314  2elresin  5339  fnres  5344  fcnvres  5411  fconstg  5424  fun11iun  5494  f1osng  5514  dffv3g  5523  fvssunirng  5542  sefvex  5548  fv3  5550  fvres  5551  nfunsn  5561  funimass4  5579  ssimaexg  5591  dmfco  5597  fvopab6  5625  fndmdif  5634  fvelrn  5660  dffo4  5677  f1ompt  5680  fmptco  5695  fsn  5701  fsng  5702  dfmpt  5706  dfmptg  5708  fnressn  5715  fressnfv  5716  fvsng  5725  resfunexg  5750  funfvima3  5763  idref  5770  abrexco  5773  imaiun  5774  dff13  5782  foeqcnvco  5804  f1eqcocnv  5805  fliftcnv  5809  isocnv2  5826  isoini  5832  isose  5835  riotav  5849  csbriotag  5856  acexmidlem2  5885  oprabid  5920  csbov123g  5926  0neqopab  5933  brabvv  5934  dfoprab2  5935  rnoprab  5971  eloprabga  5975  mpov  5978  f1opw  6092  opabex3d  6136  opabex3  6137  ofmres  6151  op1stg  6165  op2ndg  6166  1stval2  6170  2ndval2  6171  fo1st  6172  fo2nd  6173  f1stres  6174  f2ndres  6175  fo1stresm  6176  fo2ndresm  6177  xp1st  6180  xp2nd  6181  releldm2  6200  reldm  6201  sbcopeq1a  6202  csbopeq1a  6203  dfoprab3  6206  eloprabi  6211  mpomptsx  6212  dmmpossx  6214  fmpox  6215  mpofvex  6218  mpoexxg  6225  fmpoco  6231  df1st2  6234  df2nd2  6235  1stconst  6236  2ndconst  6237  dfmpo  6238  fo2ndf  6242  f1o2ndf1  6243  xporderlem  6246  cnvoprab  6249  f1od2  6250  brtpos2  6266  reldmtpos  6268  dmtpos  6271  rntpos  6272  ovtposg  6274  dftpos3  6277  dftpos4  6278  tpostpos  6279  tpossym  6291  tfrlem3  6326  tfrlem5  6329  tfrlem8  6333  tfrlemisucfn  6339  tfrlemisucaccv  6340  tfrlemibxssdm  6342  tfrlemibfn  6343  tfrlemibex  6344  tfrlemi14d  6348  tfrexlem  6349  tfr1onlem3  6353  tfr1onlemsucaccv  6356  tfr1onlembxssdm  6358  tfr1onlembfn  6359  tfr1onlemres  6364  tfri1dALT  6366  tfrcllemsucaccv  6369  tfrcllembxssdm  6371  tfrcllembfn  6372  tfrcllemres  6377  tfrcl  6379  rdgtfr  6389  rdgruledefgg  6390  rdgivallem  6396  rdgon  6401  rdg0g  6403  frec0g  6412  frecabex  6413  frecabcl  6414  frectfr  6415  freccllem  6417  frecfcllem  6419  frecsuclem  6421  frecrdg  6423  oafnex  6459  sucinc  6460  fnoa  6462  oaexg  6463  omfnex  6464  fnom  6465  omexg  6466  fnoei  6467  oeiexg  6468  oeiv  6471  oacl  6475  omcl  6476  oeicl  6477  oav2  6478  nnsucelsuc  6506  nnsucuniel  6510  ercnv  6570  iserd  6575  eqerlem  6580  eqer  6581  ecdmn0m  6591  erth  6593  qsss  6608  ecid  6612  ecidg  6613  qsid  6614  iinerm  6621  qsel  6626  erovlem  6641  ecopovsym  6645  ecopover  6647  th3qlem2  6652  mapprc  6666  fnmap  6669  fnpm  6670  mapdm0  6677  mapval2  6692  mapsn  6704  mapsncnv  6709  mapsnf1o2  6710  ixpconstg  6721  ixpprc  6733  ixpin  6737  ixpiinm  6738  ixpssmap2g  6741  ixpssmapg  6742  elixpsn  6749  ixpsnf1o  6750  bren  6761  brdomg  6762  domen  6765  domeng  6766  idssen  6791  ener  6793  domtr  6799  ensn1g  6811  en1  6813  en1bg  6814  fundmen  6820  fundmeng  6821  mapsnen  6825  fiprc  6829  unen  6830  xpsnen  6835  xpsneng  6836  xpcomco  6840  xpcomeng  6842  xpassen  6844  xpdom2  6845  xpdom2g  6846  xpf1o  6858  mapen  6860  mapxpen  6862  xpmapenlem  6863  ssenen  6865  phplem4  6869  phplem3g  6870  nneneq  6871  php5  6872  phpm  6879  findcard  6902  findcard2  6903  findcard2s  6904  isinfinf  6911  ac6sfi  6912  exmidpw  6922  exmidpweq  6923  unfidisj  6935  fiintim  6942  xpfi  6943  fisseneq  6945  ssfirab  6947  snexxph  6963  fidcenumlemr  6968  sbthlemi10  6979  isbth  6980  ssfii  6987  fi0  6988  fiss  6990  cnvinfex  7031  eqinfti  7033  infvalti  7035  infglbti  7038  infmoti  7041  ordiso2  7048  djuf1olem  7066  djuss  7083  ctm  7122  ctssdccl  7124  ctssdclemr  7125  finomni  7152  exmidomni  7154  fodjuomnilemdc  7156  nninfwlpoimlemginf  7188  pm54.43  7203  exmidfodomrlemim  7214  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  acfun  7220  ccfunen  7277  cc2lem  7279  cc3  7281  indpi  7355  dfplpq2  7367  enq0sym  7445  enq0ref  7446  enq0tr  7447  nqnq0pi  7451  nqnq0  7454  mulnnnq0  7463  nqprm  7555  nqprrnd  7556  nqprdisj  7557  nqprloc  7558  nqprl  7564  nqpru  7565  addnqprlemrl  7570  addnqprlemru  7571  addnqprlemfl  7572  addnqprlemfu  7573  mulnqprlemrl  7586  mulnqprlemru  7587  mulnqprlemfl  7588  mulnqprlemfu  7589  ltnqpr  7606  ltnqpri  7607  archpr  7656  cauappcvgprlemladdfu  7667  cauappcvgprlemladdfl  7668  cauappcvgprlem2  7673  caucvgprlemladdfu  7690  caucvgprlem2  7693  caucvgprprlemopu  7712  suplocexprlemmu  7731  suplocexprlemdisj  7733  suplocexprlemloc  7734  suplocexprlemub  7736  cnm  7845  ltresr  7852  peano1nnnn  7865  peano2nnnn  7866  axcnre  7894  axpre-apti  7898  renfdisj  8031  dfinfre  8927  1nn  8944  peano2nn  8945  indstr  9607  cnref1o  9664  ioof  9985  fzpr  10091  frec2uzrand  10419  frec2uzf1od  10420  frecuzrdgtcl  10426  frecuzrdgfunlem  10433  frecfzennn  10440  ser3le  10532  hashinfom  10772  hashunlem  10798  hashun  10799  hashxp  10820  hashfacen  10830  zfz1isolem1  10834  zfz1iso  10835  shftfvalg  10841  ovshftex  10842  shftfibg  10843  shftfval  10844  shftfib  10846  shftfn  10847  2shfti  10854  shftvalg  10859  shftval4g  10860  maxabslemval  11231  fimaxre2  11249  xrmaxiflemval  11272  fclim  11316  climshft  11326  zsumdc  11406  fsum3  11409  fsum2dlemstep  11456  fsumcnv  11459  fisumcom2  11460  fisum0diag2  11469  fsumconst  11476  modfsummodlemstep  11479  fsumabs  11487  fsumrelem  11493  fsumiun  11499  ntrivcvgap  11570  fprod2dlemstep  11644  fprodcnv  11647  fprodcom2fi  11648  fprodmodd  11663  algrf  12059  qredeu  12111  isprm2  12131  prmind2  12134  ennnfonelemex  12429  ennnfonelemrn  12434  exmidunben  12441  ctinfom  12443  ctinf  12445  qnnen  12446  enctlem  12447  ctiunctlemfo  12454  slotslfn  12502  setscomd  12517  restfn  12710  elrest  12713  ptex  12731  prdsex  12736  imasex  12744  imasival  12745  imasbas  12746  imasplusg  12747  imasmulr  12748  imasaddfnlemg  12753  fnpr2ob  12778  ismgm  12795  plusffng  12803  fn0g  12813  issgrp  12828  ismnddef  12841  subgintm  13090  releqgg  13112  eqgex  13113  eqgfval  13114  eqgval  13115  fnmgp  13174  isrng  13186  isring  13252  ringn0  13310  opprrngbg  13326  opprsubgg  13332  opprunitd  13358  opprsubrngg  13431  subrngintm  13432  subrngpropd  13436  subrgpropd  13468  scaffng  13498  rmodislmodlem  13539  rmodislmod  13540  lssex  13543  lsssn0  13559  lss1d  13572  lssintclm  13573  lspsnel  13606  rlmfn  13642  isridl  13692  bastg  13857  distop  13881  topnex  13882  epttop  13886  tgrest  13965  resttopon  13967  restco  13970  cnrest2  14032  cnptopresti  14034  cnptoprest  14035  cnptoprest2  14036  txuni2  14052  txbas  14054  eltx  14055  txcnp  14067  txcnmpt  14069  txrest  14072  txdis1cn  14074  txlm  14075  cnmpt1st  14084  cnmpt2nd  14085  txhmeo  14115  txswaphmeolem  14116  xmetec  14233  metrest  14302  reldvg  14444  dvfgg  14453  dvcj  14469  pilem3  14500  bdcvv  14905  bdsnss  14921  bdop  14923  bj-vprc  14944  bdinex1g  14949  bdssexg  14952  bj-inex  14955  bj-zfpair2  14958  bj-uniexg  14966  bdunexb  14968  bj-unexg  14969  bj-indint  14979  bj-ssom  14984  bj-om  14985  bj-2inf  14986  bj-bdfindis  14995  bj-nn0suc0  14998  bj-nnelirr  15001  bj-inf2vnlem1  15018  bj-inf2vnlem2  15019  bj-omex2  15025  bj-nn0sucALT  15026  bj-findis  15027  ss1oel2o  15040  pw1nct  15049  nninfsellemeq  15060  exmidsbthrlem  15067