Theorem vex 2733

Description: All setvar variables are sets (see isset 2736). 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 1694	. 2 ⊢ 𝑥 = 𝑥
2		df-v 2732	. . 3 ⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
3	2	abeq2i 2281	. 2 ⊢ (𝑥 ∈ V ↔ 𝑥 = 𝑥)
4	1, 3	mpbir 145	1 ⊢ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  elv  2734  elvd  2735  isset  2736  eqvisset  2740  ralv  2747  rexv  2748  reuv  2749  rmov  2750  rabab  2751  sbhypf  2779  ceqex  2857  ralab  2890  rexab  2892  mo2icl  2909  reu8  2926  csbvarg  3077  csbiebg  3091  sbcnestgf  3100  sbnfc2  3109  ddifnel  3258  ddifstab  3259  csbing  3334  unssdif  3362  unssin  3366  inssun  3367  invdif  3369  vn0  3424  vn0m  3425  eqv  3433  abvor0dc  3437  sbss  3522  velpw  3571  elpwg  3572  velsn  3598  vsnid  3613  exsnrex  3623  dftp2  3630  prmg  3702  prnzg  3705  snssg  3714  difprsnss  3716  sneqrg  3747  preq12bg  3758  pwprss  3790  pwtpss  3791  pwv  3793  unipr  3808  uniprg  3809  unisng  3811  elintg  3837  elintrabg  3842  intss1  3844  ssint  3845  intmin  3849  intss  3850  intssunim  3851  intmin4  3857  intab  3858  intun  3860  intpr  3861  intprg  3862  uniintsnr  3865  iinconstm  3880  iuniin  3881  iinss1  3883  dfiin2g  3904  dfiunv2  3907  ssiinf  3920  iinss  3922  iinss2  3923  0iin  3929  iinab  3932  iundif2ss  3936  iindif2m  3938  iinin2m  3939  iinuniss  3953  sspwuni  3955  pwpwab  3958  iinpw  3961  iunpwss  3962  brab1  4034  csbopabg  4065  mptv  4084  trint  4100  vnex  4118  inex1g  4123  ssexg  4126  inteximm  4133  inuni  4139  repizf2  4146  axpweq  4155  bnd2  4157  pwuni  4176  exmidundif  4190  exmidundifim  4191  zfpair2  4193  rext  4198  sspwb  4199  unipw  4200  ssextss  4203  euabex  4208  mss  4209  exss  4210  opth  4220  opthg  4221  copsexg  4227  copsex4g  4230  moop2  4234  euotd  4237  opabid  4240  elopab  4241  opelopabsbALT  4242  opelopabsb  4243  opabm  4263  pwin  4265  pwunss  4266  epelg  4273  epel  4275  pofun  4295  epse  4325  tron  4365  sucel  4393  suctr  4404  vuniex  4421  uniexg  4422  unexb  4425  snnex  4431  pwnex  4432  uniuni  4434  eusvnf  4436  eusvnfb  4437  iunpw  4463  unon  4493  ordunisuc2r  4496  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  ordsucunielexmid  4513  elirr  4523  en2lp  4536  dtruex  4541  onintexmid  4555  reg3exmidlemwe  4561  dcextest  4563  finds  4582  finds2  4583  elomssom  4587  limom  4596  0nelxp  4637  opelxp  4639  opeliunxp  4664  elvv  4671  elvvv  4672  elvvuni  4673  xpsspw  4721  relopabi  4735  opabid2  4740  difopab  4742  xpiindim  4746  raliunxp  4750  rexiunxp  4751  ralxpf  4755  rexxpf  4756  relop  4759  cnvco  4794  dfrn2  4797  dfdm4  4801  dmss  4808  dmin  4817  dmiun  4818  dmuni  4819  dm0  4823  dmi  4824  reldm0  4827  elreldm  4835  elrnmpt1  4860  dmrnssfld  4872  dmcoss  4878  dmcosseq  4880  opelresg  4896  resieq  4899  dmres  4910  elres  4925  relssres  4927  resopab  4933  resiexg  4934  iss  4935  dfres2  4941  dfima2  4953  imadmrn  4961  imai  4965  csbima12g  4970  elimasng  4977  args  4978  epini  4980  iniseg  4981  dfse2  4982  exse2  4983  cotr  4990  issref  4991  cnvsym  4992  intasym  4993  asymref  4994  intirr  4995  brcodir  4996  codir  4997  qfto  4998  poirr2  5001  cnvopab  5010  cnv0  5012  cnvi  5013  cnvdif  5015  rniun  5019  dminss  5023  imainss  5024  inimasn  5026  xpmlem  5029  dmxpss  5039  rnxpid  5043  ssrnres  5051  rninxp  5052  dminxp  5053  cnvcnv3  5058  dfrel2  5059  dmsnm  5074  dmsnopg  5080  cnvcnvsn  5085  dmsnsnsng  5086  cnvsng  5094  elxp4  5096  elxp5  5097  cnvresima  5098  dfco2  5108  dfco2a  5109  cores  5112  resco  5113  imaco  5114  rnco  5115  coiun  5118  co02  5122  coi1  5124  coass  5127  relssdmrn  5129  unielrel  5136  ressn  5149  cnviinm  5150  cnvpom  5151  cnvsom  5152  uniabio  5168  iotaval  5169  iotass  5175  sniota  5187  csbiotag  5189  dffun2  5206  dffun7  5223  dffun8  5224  dffun9  5225  funopg  5230  funssres  5238  funun  5240  funcnvsn  5241  funinsn  5245  funcnv2  5256  funcnv  5257  funcnv3  5258  funcnveq  5259  fun2cnv  5260  funcnvuni  5265  imadif  5276  funimaexglem  5279  isarep1  5282  2elresin  5307  fnres  5312  fcnvres  5379  fconstg  5392  fun11iun  5461  f1osng  5481  dffv3g  5490  fvssunirng  5509  sefvex  5515  fv3  5517  fvres  5518  nfunsn  5528  funimass4  5545  ssimaexg  5556  dmfco  5562  fvopab6  5590  fndmdif  5599  fvelrn  5625  dffo4  5642  f1ompt  5645  fmptco  5660  fsn  5666  fsng  5667  dfmpt  5671  dfmptg  5673  fnressn  5680  fressnfv  5681  fvsng  5690  resfunexg  5715  funfvima3  5727  idref  5734  abrexco  5736  imaiun  5737  dff13  5745  foeqcnvco  5767  f1eqcocnv  5768  fliftcnv  5772  isocnv2  5789  isoini  5795  isose  5798  riotav  5812  csbriotag  5819  acexmidlem2  5848  oprabid  5883  csbov123g  5889  0neqopab  5896  brabvv  5897  dfoprab2  5898  rnoprab  5934  eloprabga  5938  mpov  5941  f1opw  6054  opabex3d  6098  opabex3  6099  ofmres  6113  op1stg  6127  op2ndg  6128  1stval2  6132  2ndval2  6133  fo1st  6134  fo2nd  6135  f1stres  6136  f2ndres  6137  fo1stresm  6138  fo2ndresm  6139  xp1st  6142  xp2nd  6143  releldm2  6162  reldm  6163  sbcopeq1a  6164  csbopeq1a  6165  dfoprab3  6168  eloprabi  6173  mpomptsx  6174  dmmpossx  6176  fmpox  6177  mpofvex  6180  mpoexxg  6187  fmpoco  6193  df1st2  6196  df2nd2  6197  1stconst  6198  2ndconst  6199  dfmpo  6200  fo2ndf  6204  f1o2ndf1  6205  xporderlem  6208  cnvoprab  6211  f1od2  6212  brtpos2  6228  reldmtpos  6230  dmtpos  6233  rntpos  6234  ovtposg  6236  dftpos3  6239  dftpos4  6240  tpostpos  6241  tpossym  6253  tfrlem3  6288  tfrlem5  6291  tfrlem8  6295  tfrlemisucfn  6301  tfrlemisucaccv  6302  tfrlemibxssdm  6304  tfrlemibfn  6305  tfrlemibex  6306  tfrlemi14d  6310  tfrexlem  6311  tfr1onlem3  6315  tfr1onlemsucaccv  6318  tfr1onlembxssdm  6320  tfr1onlembfn  6321  tfr1onlemres  6326  tfri1dALT  6328  tfrcllemsucaccv  6331  tfrcllembxssdm  6333  tfrcllembfn  6334  tfrcllemres  6339  tfrcl  6341  rdgtfr  6351  rdgruledefgg  6352  rdgivallem  6358  rdgon  6363  rdg0g  6365  frec0g  6374  frecabex  6375  frecabcl  6376  frectfr  6377  freccllem  6379  frecfcllem  6381  frecsuclem  6383  frecrdg  6385  oafnex  6421  sucinc  6422  fnoa  6424  oaexg  6425  omfnex  6426  fnom  6427  omexg  6428  fnoei  6429  oeiexg  6430  oeiv  6433  oacl  6437  omcl  6438  oeicl  6439  oav2  6440  nnsucelsuc  6468  nnsucuniel  6472  ercnv  6531  iserd  6536  eqerlem  6541  eqer  6542  ecdmn0m  6552  erth  6554  qsss  6569  ecid  6573  ecidg  6574  qsid  6575  iinerm  6582  qsel  6587  erovlem  6602  ecopovsym  6606  ecopover  6608  th3qlem2  6613  mapprc  6627  fnmap  6630  fnpm  6631  mapdm0  6638  mapval2  6653  mapsn  6665  mapsncnv  6670  mapsnf1o2  6671  ixpconstg  6682  ixpprc  6694  ixpin  6698  ixpiinm  6699  ixpssmap2g  6702  ixpssmapg  6703  elixpsn  6710  ixpsnf1o  6711  bren  6722  brdomg  6723  domen  6726  domeng  6727  idssen  6752  ener  6754  domtr  6760  ensn1g  6772  en1  6774  en1bg  6775  fundmen  6781  fundmeng  6782  mapsnen  6786  fiprc  6790  unen  6791  xpsnen  6796  xpsneng  6797  xpcomco  6801  xpcomeng  6803  xpassen  6805  xpdom2  6806  xpdom2g  6807  xpf1o  6819  mapen  6821  mapxpen  6823  xpmapenlem  6824  ssenen  6826  phplem4  6830  phplem3g  6831  nneneq  6832  php5  6833  phpm  6840  findcard  6863  findcard2  6864  findcard2s  6865  isinfinf  6872  ac6sfi  6873  exmidpw  6883  exmidpweq  6884  unfidisj  6896  fiintim  6903  xpfi  6904  fisseneq  6906  ssfirab  6908  snexxph  6924  fidcenumlemr  6929  sbthlemi10  6940  isbth  6941  ssfii  6948  fi0  6949  fiss  6951  cnvinfex  6992  eqinfti  6994  infvalti  6996  infglbti  6999  infmoti  7002  ordiso2  7009  djuf1olem  7027  djuss  7044  ctm  7083  ctssdccl  7085  ctssdclemr  7086  finomni  7113  exmidomni  7115  fodjuomnilemdc  7117  pm54.43  7156  exmidfodomrlemim  7167  exmidfodomrlemr  7168  exmidfodomrlemrALT  7169  acfun  7173  ccfunen  7215  cc2lem  7217  cc3  7219  indpi  7293  dfplpq2  7305  enq0sym  7383  enq0ref  7384  enq0tr  7385  nqnq0pi  7389  nqnq0  7392  mulnnnq0  7401  nqprm  7493  nqprrnd  7494  nqprdisj  7495  nqprloc  7496  nqprl  7502  nqpru  7503  addnqprlemrl  7508  addnqprlemru  7509  addnqprlemfl  7510  addnqprlemfu  7511  mulnqprlemrl  7524  mulnqprlemru  7525  mulnqprlemfl  7526  mulnqprlemfu  7527  ltnqpr  7544  ltnqpri  7545  archpr  7594  cauappcvgprlemladdfu  7605  cauappcvgprlemladdfl  7606  cauappcvgprlem2  7611  caucvgprlemladdfu  7628  caucvgprlem2  7631  caucvgprprlemopu  7650  suplocexprlemmu  7669  suplocexprlemdisj  7671  suplocexprlemloc  7672  suplocexprlemub  7674  cnm  7783  ltresr  7790  peano1nnnn  7803  peano2nnnn  7804  axcnre  7832  axpre-apti  7836  renfdisj  7968  dfinfre  8861  1nn  8878  peano2nn  8879  indstr  9541  cnref1o  9598  ioof  9917  fzpr  10022  frec2uzrand  10350  frec2uzf1od  10351  frecuzrdgtcl  10357  frecuzrdgfunlem  10364  frecfzennn  10371  ser3le  10463  hashinfom  10701  hashunlem  10728  hashun  10729  hashxp  10750  hashfacen  10760  zfz1isolem1  10764  zfz1iso  10765  shftfvalg  10771  ovshftex  10772  shftfibg  10773  shftfval  10774  shftfib  10776  shftfn  10777  2shfti  10784  shftvalg  10789  shftval4g  10790  maxabslemval  11161  fimaxre2  11179  xrmaxiflemval  11202  fclim  11246  climshft  11256  zsumdc  11336  fsum3  11339  fsum2dlemstep  11386  fsumcnv  11389  fisumcom2  11390  fisum0diag2  11399  fsumconst  11406  modfsummodlemstep  11409  fsumabs  11417  fsumrelem  11423  fsumiun  11429  ntrivcvgap  11500  fprod2dlemstep  11574  fprodcnv  11577  fprodcom2fi  11578  fprodmodd  11593  algrf  11988  qredeu  12040  isprm2  12060  prmind2  12063  ennnfonelemex  12358  ennnfonelemrn  12363  exmidunben  12370  ctinfom  12372  ctinf  12374  qnnen  12375  enctlem  12376  ctiunctlemfo  12383  slotslfn  12431  restfn  12572  elrest  12575  ismgm  12600  plusffng  12608  fn0g  12618  issgrp  12633  ismnddef  12643  bastg  12816  distop  12840  topnex  12841  epttop  12845  tgrest  12924  resttopon  12926  restco  12929  cnrest2  12991  cnptopresti  12993  cnptoprest  12994  cnptoprest2  12995  txuni2  13011  txbas  13013  eltx  13014  txcnp  13026  txcnmpt  13028  txrest  13031  txdis1cn  13033  txlm  13034  cnmpt1st  13043  cnmpt2nd  13044  txhmeo  13074  txswaphmeolem  13075  xmetec  13192  metrest  13261  reldvg  13403  dvfgg  13412  dvcj  13428  pilem3  13459  bdcvv  13854  bdsnss  13870  bdop  13872  bj-vprc  13893  bdinex1g  13898  bdssexg  13901  bj-inex  13904  bj-zfpair2  13907  bj-uniexg  13915  bdunexb  13917  bj-unexg  13918  bj-indint  13928  bj-ssom  13933  bj-om  13934  bj-2inf  13935  bj-bdfindis  13944  bj-nn0suc0  13947  bj-nnelirr  13950  bj-inf2vnlem1  13967  bj-inf2vnlem2  13968  bj-omex2  13974  bj-nn0sucALT  13975  bj-findis  13976  ss1oel2o  13988  pw1nct  13998  nninfsellemeq  14009  exmidsbthrlem  14016