Theorem vex 2755

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

Syntax hints:   ∈ wcel 2160  Vcvv 2752

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  elv  2756  elvd  2757  isset  2758  eqvisset  2762  ralv  2769  rexv  2770  reuv  2771  rmov  2772  rabab  2773  sbhypf  2801  ceqex  2879  ralab  2912  rexab  2914  mo2icl  2931  reu8  2948  csbvarg  3100  csbiebg  3114  sbcnestgf  3123  sbnfc2  3132  ddifnel  3281  ddifstab  3282  csbing  3357  unssdif  3385  unssin  3389  inssun  3390  invdif  3392  vn0  3448  vn0m  3449  eqv  3457  abvor0dc  3461  sbss  3546  velpw  3597  elpwg  3598  velsn  3624  vsnid  3639  exsnrex  3649  dftp2  3656  prmg  3728  prnzg  3731  snssgOLD  3743  difprsnss  3745  sneqrg  3777  preq12bg  3788  pwprss  3820  pwtpss  3821  pwv  3823  unipr  3838  uniprg  3839  unisng  3841  elintg  3867  elintrabg  3872  intss1  3874  ssint  3875  intmin  3879  intss  3880  intssunim  3881  intmin4  3887  intab  3888  intun  3890  intpr  3891  intprg  3892  uniintsnr  3895  iinconstm  3910  iuniin  3911  iinss1  3913  dfiin2g  3934  dfiunv2  3937  ssiinf  3951  iinss  3953  iinss2  3954  0iin  3960  iinab  3963  iundif2ss  3967  iindif2m  3969  iinin2m  3970  iinuniss  3984  sspwuni  3986  pwpwab  3989  iinpw  3992  iunpwss  3993  brab1  4065  csbopabg  4096  mptv  4115  trint  4131  vnex  4149  inex1g  4154  ssexg  4157  inteximm  4164  inuni  4170  repizf2  4177  axpweq  4186  bnd2  4188  pwuni  4207  exmidundif  4221  exmidundifim  4222  zfpair2  4225  rext  4230  sspwb  4231  unipw  4232  ssextss  4235  euabex  4240  mss  4241  exss  4242  opth  4252  opthg  4253  copsexg  4259  copsex4g  4262  moop2  4266  euotd  4269  opabid  4272  elopab  4273  opelopabsbALT  4274  opelopabsb  4275  opabm  4295  pwin  4297  pwunss  4298  epelg  4305  epel  4307  pofun  4327  epse  4357  tron  4397  sucel  4425  suctr  4436  vuniex  4453  uniexg  4454  unexb  4457  snnex  4463  pwnex  4464  uniuni  4466  eusvnf  4468  eusvnfb  4469  iunpw  4495  unon  4525  ordunisuc2r  4528  ordtri2or2exmidlem  4540  onsucelsucexmidlem  4543  ordsucunielexmid  4545  elirr  4555  en2lp  4568  dtruex  4573  onintexmid  4587  reg3exmidlemwe  4593  dcextest  4595  finds  4614  finds2  4615  elomssom  4619  limom  4628  0nelxp  4669  opelxp  4671  opeliunxp  4696  elvv  4703  elvvv  4704  elvvuni  4705  xpsspw  4753  relopabi  4767  opabid2  4773  difopab  4775  xpiindim  4779  raliunxp  4783  rexiunxp  4784  ralxpf  4788  rexxpf  4789  relop  4792  cnvco  4827  dfrn2  4830  dfdm4  4834  dmss  4841  dmin  4850  dmiun  4851  dmuni  4852  dm0  4856  dmi  4857  reldm0  4860  elreldm  4868  elrnmpt1  4893  dmrnssfld  4905  dmcoss  4911  dmcosseq  4913  opelresg  4929  resieq  4932  dmres  4943  elres  4958  relssres  4960  resopab  4966  resiexg  4967  iss  4968  dfres2  4974  restidsing  4978  dfima2  4987  imadmrn  4995  imai  4999  csbima12g  5004  elimasng  5011  args  5012  epini  5014  iniseg  5015  dfse2  5016  exse2  5017  cotr  5025  issref  5026  cnvsym  5027  intasym  5028  asymref  5029  intirr  5030  brcodir  5031  codir  5032  qfto  5033  poirr2  5036  cnvopab  5045  cnv0  5047  cnvi  5048  cnvdif  5050  rniun  5054  dminss  5058  imainss  5059  inimasn  5061  xpmlem  5064  dmxpss  5074  rnxpid  5078  ssrnres  5086  rninxp  5087  dminxp  5088  cnvcnv3  5093  dfrel2  5094  dmsnm  5109  dmsnopg  5115  cnvcnvsn  5120  dmsnsnsng  5121  cnvsng  5129  elxp4  5131  elxp5  5132  cnvresima  5133  dfco2  5143  dfco2a  5144  cores  5147  resco  5148  imaco  5149  rnco  5150  coiun  5153  co02  5157  coi1  5159  coass  5162  relssdmrn  5164  unielrel  5171  ressn  5184  cnviinm  5185  cnvpom  5186  cnvsom  5187  uniabio  5203  iotaval  5204  iotass  5210  sniota  5223  csbiotag  5225  dffun2  5242  dffun7  5259  dffun8  5260  dffun9  5261  funopg  5266  funssres  5274  funun  5276  funcnvsn  5277  funinsn  5281  funcnv2  5292  funcnv  5293  funcnv3  5294  funcnveq  5295  fun2cnv  5296  funcnvuni  5301  imadif  5312  funimaexglem  5315  isarep1  5318  2elresin  5343  fnres  5348  fcnvres  5415  fconstg  5428  fun11iun  5498  f1osng  5518  dffv3g  5527  fvssunirng  5546  sefvex  5552  fv3  5554  fvres  5555  nfunsn  5565  funimass4  5583  ssimaexg  5595  dmfco  5601  fvopab6  5629  fndmdif  5638  fvelrn  5664  dffo4  5681  f1ompt  5684  fmptco  5699  fsn  5705  fsng  5706  dfmpt  5710  dfmptg  5712  fnressn  5719  fressnfv  5720  fvsng  5729  resfunexg  5754  funfvima3  5767  idref  5774  abrexco  5777  imaiun  5778  dff13  5786  foeqcnvco  5808  f1eqcocnv  5809  fliftcnv  5813  isocnv2  5830  isoini  5836  isose  5839  riotav  5853  csbriotag  5860  acexmidlem2  5889  oprabid  5924  csbov123g  5930  0neqopab  5937  brabvv  5938  dfoprab2  5939  rnoprab  5975  eloprabga  5979  mpov  5982  f1opw  6097  opabex3d  6141  opabex3  6142  ofmres  6156  op1stg  6170  op2ndg  6171  1stval2  6175  2ndval2  6176  fo1st  6177  fo2nd  6178  f1stres  6179  f2ndres  6180  fo1stresm  6181  fo2ndresm  6182  xp1st  6185  xp2nd  6186  releldm2  6205  reldm  6206  sbcopeq1a  6207  csbopeq1a  6208  dfoprab3  6211  eloprabi  6216  mpomptsx  6217  dmmpossx  6219  fmpox  6220  mpofvex  6223  mpoexxg  6230  fmpoco  6236  df1st2  6239  df2nd2  6240  1stconst  6241  2ndconst  6242  dfmpo  6243  fo2ndf  6247  f1o2ndf1  6248  xporderlem  6251  cnvoprab  6254  f1od2  6255  brtpos2  6271  reldmtpos  6273  dmtpos  6276  rntpos  6277  ovtposg  6279  dftpos3  6282  dftpos4  6283  tpostpos  6284  tpossym  6296  tfrlem3  6331  tfrlem5  6334  tfrlem8  6338  tfrlemisucfn  6344  tfrlemisucaccv  6345  tfrlemibxssdm  6347  tfrlemibfn  6348  tfrlemibex  6349  tfrlemi14d  6353  tfrexlem  6354  tfr1onlem3  6358  tfr1onlemsucaccv  6361  tfr1onlembxssdm  6363  tfr1onlembfn  6364  tfr1onlemres  6369  tfri1dALT  6371  tfrcllemsucaccv  6374  tfrcllembxssdm  6376  tfrcllembfn  6377  tfrcllemres  6382  tfrcl  6384  rdgtfr  6394  rdgruledefgg  6395  rdgivallem  6401  rdgon  6406  rdg0g  6408  frec0g  6417  frecabex  6418  frecabcl  6419  frectfr  6420  freccllem  6422  frecfcllem  6424  frecsuclem  6426  frecrdg  6428  oafnex  6464  sucinc  6465  fnoa  6467  oaexg  6468  omfnex  6469  fnom  6470  omexg  6471  fnoei  6472  oeiexg  6473  oeiv  6476  oacl  6480  omcl  6481  oeicl  6482  oav2  6483  nnsucelsuc  6511  nnsucuniel  6515  ercnv  6575  iserd  6580  eqerlem  6585  eqer  6586  ecdmn0m  6596  erth  6598  qsss  6613  ecid  6617  ecidg  6618  qsid  6619  iinerm  6626  qsel  6631  erovlem  6646  ecopovsym  6650  ecopover  6652  th3qlem2  6657  mapprc  6671  fnmap  6674  fnpm  6675  mapdm0  6682  mapval2  6697  mapsn  6709  mapsncnv  6714  mapsnf1o2  6715  ixpconstg  6726  ixpprc  6738  ixpin  6742  ixpiinm  6743  ixpssmap2g  6746  ixpssmapg  6747  elixpsn  6754  ixpsnf1o  6755  bren  6766  brdomg  6767  domen  6770  domeng  6771  idssen  6796  ener  6798  domtr  6804  ensn1g  6816  en1  6818  en1bg  6819  fundmen  6825  fundmeng  6826  mapsnen  6830  fiprc  6834  unen  6835  xpsnen  6840  xpsneng  6841  xpcomco  6845  xpcomeng  6847  xpassen  6849  xpdom2  6850  xpdom2g  6851  xpf1o  6863  mapen  6865  mapxpen  6867  xpmapenlem  6868  ssenen  6870  phplem4  6874  phplem3g  6875  nneneq  6876  php5  6877  phpm  6884  findcard  6907  findcard2  6908  findcard2s  6909  isinfinf  6916  ac6sfi  6917  exmidpw  6927  exmidpweq  6928  unfidisj  6940  fiintim  6947  xpfi  6948  fisseneq  6950  ssfirab  6952  snexxph  6969  fidcenumlemr  6974  sbthlemi10  6985  isbth  6986  ssfii  6993  fi0  6994  fiss  6996  cnvinfex  7037  eqinfti  7039  infvalti  7041  infglbti  7044  infmoti  7047  ordiso2  7054  djuf1olem  7072  djuss  7089  ctm  7128  ctssdccl  7130  ctssdclemr  7131  finomni  7158  exmidomni  7160  fodjuomnilemdc  7162  nninfwlpoimlemginf  7194  pm54.43  7209  exmidfodomrlemim  7220  exmidfodomrlemr  7221  exmidfodomrlemrALT  7222  acfun  7226  ccfunen  7283  cc2lem  7285  cc3  7287  indpi  7361  dfplpq2  7373  enq0sym  7451  enq0ref  7452  enq0tr  7453  nqnq0pi  7457  nqnq0  7460  mulnnnq0  7469  nqprm  7561  nqprrnd  7562  nqprdisj  7563  nqprloc  7564  nqprl  7570  nqpru  7571  addnqprlemrl  7576  addnqprlemru  7577  addnqprlemfl  7578  addnqprlemfu  7579  mulnqprlemrl  7592  mulnqprlemru  7593  mulnqprlemfl  7594  mulnqprlemfu  7595  ltnqpr  7612  ltnqpri  7613  archpr  7662  cauappcvgprlemladdfu  7673  cauappcvgprlemladdfl  7674  cauappcvgprlem2  7679  caucvgprlemladdfu  7696  caucvgprlem2  7699  caucvgprprlemopu  7718  suplocexprlemmu  7737  suplocexprlemdisj  7739  suplocexprlemloc  7740  suplocexprlemub  7742  cnm  7851  ltresr  7858  peano1nnnn  7871  peano2nnnn  7872  axcnre  7900  axpre-apti  7904  renfdisj  8037  dfinfre  8933  1nn  8950  peano2nn  8951  indstr  9613  cnref1o  9670  ioof  9991  fzpr  10097  frec2uzrand  10425  frec2uzf1od  10426  frecuzrdgtcl  10432  frecuzrdgfunlem  10439  frecfzennn  10446  ser3le  10538  hashinfom  10778  hashunlem  10804  hashun  10805  hashxp  10826  hashfacen  10836  zfz1isolem1  10840  zfz1iso  10841  shftfvalg  10847  ovshftex  10848  shftfibg  10849  shftfval  10850  shftfib  10852  shftfn  10853  2shfti  10860  shftvalg  10865  shftval4g  10866  maxabslemval  11237  fimaxre2  11255  xrmaxiflemval  11278  fclim  11322  climshft  11332  zsumdc  11412  fsum3  11415  fsum2dlemstep  11462  fsumcnv  11465  fisumcom2  11466  fisum0diag2  11475  fsumconst  11482  modfsummodlemstep  11485  fsumabs  11493  fsumrelem  11499  fsumiun  11505  ntrivcvgap  11576  fprod2dlemstep  11650  fprodcnv  11653  fprodcom2fi  11654  fprodmodd  11669  algrf  12065  qredeu  12117  isprm2  12137  prmind2  12140  4sqlemafi  12413  4sqlem12  12417  ennnfonelemex  12440  ennnfonelemrn  12445  exmidunben  12452  ctinfom  12454  ctinf  12456  qnnen  12457  enctlem  12458  ctiunctlemfo  12465  slotslfn  12513  setscomd  12528  restfn  12721  elrest  12724  ptex  12742  prdsex  12747  imasex  12755  imasival  12756  imasbas  12757  imasplusg  12758  imasmulr  12759  imasaddfnlemg  12764  fnpr2ob  12789  ismgm  12806  plusffng  12814  fn0g  12824  issgrp  12839  ismnddef  12852  subgintm  13110  releqgg  13132  eqgex  13133  eqgfval  13134  eqgval  13135  isghm  13150  fnmgp  13244  isrng  13256  isring  13322  ringn0  13380  opprrngbg  13396  opprsubgg  13402  opprunitd  13428  dfrhm2  13472  rhmex  13475  opprsubrngg  13526  subrngintm  13527  subrngpropd  13531  subrgpropd  13563  scaffng  13593  rmodislmodlem  13634  rmodislmod  13635  lssex  13638  lsssn0  13654  lss1d  13667  lssintclm  13668  lspsnel  13701  rlmfn  13737  isridl  13787  znval  13900  bastg  13965  distop  13989  topnex  13990  epttop  13994  tgrest  14073  resttopon  14075  restco  14078  cnrest2  14140  cnptopresti  14142  cnptoprest  14143  cnptoprest2  14144  txuni2  14160  txbas  14162  eltx  14163  txcnp  14175  txcnmpt  14177  txrest  14180  txdis1cn  14182  txlm  14183  cnmpt1st  14192  cnmpt2nd  14193  txhmeo  14223  txswaphmeolem  14224  xmetec  14341  metrest  14410  reldvg  14552  dvfgg  14561  dvcj  14577  pilem3  14608  bdcvv  15013  bdsnss  15029  bdop  15031  bj-vprc  15052  bdinex1g  15057  bdssexg  15060  bj-inex  15063  bj-zfpair2  15066  bj-uniexg  15074  bdunexb  15076  bj-unexg  15077  bj-indint  15087  bj-ssom  15092  bj-om  15093  bj-2inf  15094  bj-bdfindis  15103  bj-nn0suc0  15106  bj-nnelirr  15109  bj-inf2vnlem1  15126  bj-inf2vnlem2  15127  bj-omex2  15133  bj-nn0sucALT  15134  bj-findis  15135  ss1oel2o  15148  pw1nct  15157  nninfsellemeq  15168  exmidsbthrlem  15175