Theorem vex 2763

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

Syntax hints:   ∈ wcel 2164  Vcvv 2760

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 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elv  2764  elvd  2765  isset  2766  eqvisset  2770  ralv  2777  rexv  2778  reuv  2779  rmov  2780  rabab  2781  sbhypf  2809  ceqex  2887  ralab  2920  rexab  2922  mo2icl  2939  reu8  2956  csbvarg  3108  csbiebg  3123  sbcnestgf  3132  sbnfc2  3141  ddifnel  3290  ddifstab  3291  csbing  3366  unssdif  3394  unssin  3398  inssun  3399  invdif  3401  vn0  3457  vn0m  3458  eqv  3466  abvor0dc  3470  sbss  3554  velpw  3608  elpwg  3609  velsn  3635  vsnid  3650  exsnrex  3660  dftp2  3667  prmg  3739  prnzg  3742  snssgOLD  3754  difprsnss  3756  sneqrg  3788  preq12bg  3799  pwprss  3831  pwtpss  3832  pwv  3834  unipr  3849  uniprg  3850  unisng  3852  elintg  3878  elintrabg  3883  intss1  3885  ssint  3886  intmin  3890  intss  3891  intssunim  3892  intmin4  3898  intab  3899  intun  3901  intpr  3902  intprg  3903  uniintsnr  3906  iinconstm  3921  iuniin  3922  iinss1  3924  dfiin2g  3945  dfiunv2  3948  ssiinf  3962  iinss  3964  iinss2  3965  0iin  3971  iinab  3974  iundif2ss  3978  iindif2m  3980  iinin2m  3981  iinuniss  3995  sspwuni  3997  pwpwab  4000  iinpw  4003  iunpwss  4004  brab1  4076  csbopabg  4107  mptv  4126  trint  4142  vnex  4160  inex1g  4165  ssexg  4168  inteximm  4178  inuni  4184  repizf2  4191  axpweq  4200  bnd2  4202  pwuni  4221  exmidundif  4235  exmidundifim  4236  zfpair2  4239  rext  4244  sspwb  4245  unipw  4246  ssextss  4249  euabex  4254  mss  4255  exss  4256  opth  4266  opthg  4267  copsexg  4273  copsex4g  4276  moop2  4280  euotd  4283  opabid  4286  elopab  4288  opelopabsbALT  4289  opelopabsb  4290  opabm  4311  pwin  4313  pwunss  4314  epelg  4321  epel  4323  pofun  4343  epse  4373  tron  4413  sucel  4441  suctr  4452  vuniex  4469  uniexg  4470  unexb  4473  snnex  4479  pwnex  4480  uniuni  4482  eusvnf  4484  eusvnfb  4485  iunpw  4511  unon  4543  ordunisuc2r  4546  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  ordsucunielexmid  4563  elirr  4573  en2lp  4586  dtruex  4591  onintexmid  4605  reg3exmidlemwe  4611  dcextest  4613  finds  4632  finds2  4633  elomssom  4637  limom  4646  0nelxp  4687  opelxp  4689  opeliunxp  4714  elvv  4721  elvvv  4722  elvvuni  4723  xpsspw  4771  relopabiv  4785  relopabi  4787  opabid2  4793  difopab  4795  xpiindim  4799  raliunxp  4803  rexiunxp  4804  ralxpf  4808  rexxpf  4809  relop  4812  cnvco  4847  dfrn2  4850  dfdm4  4854  dmss  4861  dmin  4870  dmiun  4871  dmuni  4872  dm0  4876  dmi  4877  reldm0  4880  elreldm  4888  elrnmpt1  4913  dmrnssfld  4925  dmcoss  4931  dmcosseq  4933  opelresg  4949  resieq  4952  dmres  4963  elres  4978  relssres  4980  resopab  4986  resiexg  4987  iss  4988  dfres2  4994  restidsing  4998  dfima2  5007  imadmrn  5015  imai  5021  csbima12g  5026  elimasng  5033  args  5034  epini  5036  iniseg  5037  dfse2  5038  exse2  5039  cotr  5047  issref  5048  cnvsym  5049  intasym  5050  asymref  5051  intirr  5052  brcodir  5053  codir  5054  qfto  5055  poirr2  5058  cnvopab  5067  cnv0  5069  cnvi  5070  cnvdif  5072  rniun  5076  dminss  5080  imainss  5081  inimasn  5083  xpmlem  5086  dmxpss  5096  rnxpid  5100  ssrnres  5108  rninxp  5109  dminxp  5110  cnvcnv3  5115  dfrel2  5116  dmsnm  5131  dmsnopg  5137  cnvcnvsn  5142  dmsnsnsng  5143  cnvsng  5151  elxp4  5153  elxp5  5154  cnvresima  5155  dfco2  5165  dfco2a  5166  cores  5169  resco  5170  imaco  5171  rnco  5172  coiun  5175  co02  5179  coi1  5181  coass  5184  relssdmrn  5186  unielrel  5193  ressn  5206  cnviinm  5207  cnvpom  5208  cnvsom  5209  uniabio  5225  iotaval  5226  iotass  5232  sniota  5245  csbiotag  5247  dffun2  5264  dffun7  5281  dffun8  5282  dffun9  5283  funopg  5288  funssres  5296  funun  5298  funcnvsn  5299  funinsn  5303  funcnv2  5314  funcnv  5315  funcnv3  5316  funcnveq  5317  fun2cnv  5318  funcnvuni  5323  imadif  5334  funimaexglem  5337  isarep1  5340  2elresin  5365  fnres  5370  fcnvres  5437  fconstg  5450  fun11iun  5521  f1osng  5541  dffv3g  5550  fvssunirng  5569  sefvex  5575  fv3  5577  fvres  5578  nfunsn  5589  funimass4  5607  ssimaexg  5619  dmfco  5625  fvopab6  5654  fndmdif  5663  fvelrn  5689  dffo4  5706  f1ompt  5709  fmptco  5724  fsn  5730  fsng  5731  dfmpt  5735  dfmptg  5737  fnressn  5744  fressnfv  5745  fvsng  5754  resfunexg  5779  funfvima3  5792  idref  5799  abrexco  5802  imaiun  5803  dff13  5811  foeqcnvco  5833  f1eqcocnv  5834  fliftcnv  5838  isocnv2  5855  isoini  5861  isose  5864  riotav  5879  csbriotag  5886  acexmidlem2  5915  oprabid  5950  csbov123g  5956  0neqopab  5963  brabvv  5964  dfoprab2  5965  rnoprab  6001  eloprabga  6005  mpov  6008  f1opw  6125  opabex3d  6173  opabex3  6174  ofmres  6188  uchoice  6190  op1stg  6203  op2ndg  6204  1stval2  6208  2ndval2  6209  fo1st  6210  fo2nd  6211  f1stres  6212  f2ndres  6213  fo1stresm  6214  fo2ndresm  6215  xp1st  6218  xp2nd  6219  releldm2  6238  reldm  6239  sbcopeq1a  6240  csbopeq1a  6241  dfoprab3  6244  eloprabi  6249  mpomptsx  6250  dmmpossx  6252  fmpox  6253  mpofvex  6256  mpoexxg  6263  fmpoco  6269  df1st2  6272  df2nd2  6273  1stconst  6274  2ndconst  6275  dfmpo  6276  fo2ndf  6280  f1o2ndf1  6281  xporderlem  6284  cnvoprab  6287  f1od2  6288  brtpos2  6304  reldmtpos  6306  dmtpos  6309  rntpos  6310  ovtposg  6312  dftpos3  6315  dftpos4  6316  tpostpos  6317  tpossym  6329  tfrlem3  6364  tfrlem5  6367  tfrlem8  6371  tfrlemisucfn  6377  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemibex  6382  tfrlemi14d  6386  tfrexlem  6387  tfr1onlem3  6391  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemres  6415  tfrcl  6417  rdgtfr  6427  rdgruledefgg  6428  rdgivallem  6434  rdgon  6439  rdg0g  6441  frec0g  6450  frecabex  6451  frecabcl  6452  frectfr  6453  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecrdg  6461  oafnex  6497  sucinc  6498  fnoa  6500  oaexg  6501  omfnex  6502  fnom  6503  omexg  6504  fnoei  6505  oeiexg  6506  oeiv  6509  oacl  6513  omcl  6514  oeicl  6515  oav2  6516  nnsucelsuc  6544  nnsucuniel  6548  ercnv  6608  iserd  6613  eqerlem  6618  eqer  6619  ecdmn0m  6631  erth  6633  qsss  6648  ecid  6652  ecidg  6653  qsid  6654  iinerm  6661  qsel  6666  erovlem  6681  ecopovsym  6685  ecopover  6687  th3qlem2  6692  mapprc  6706  fnmap  6709  fnpm  6710  mapdm0  6717  mapval2  6732  mapsn  6744  mapsncnv  6749  mapsnf1o2  6750  ixpconstg  6761  ixpprc  6773  ixpin  6777  ixpiinm  6778  ixpssmap2g  6781  ixpssmapg  6782  elixpsn  6789  ixpsnf1o  6790  bren  6801  brdomg  6802  domen  6805  domeng  6806  idssen  6831  ener  6833  domtr  6839  ensn1g  6851  en1  6853  en1bg  6854  fundmen  6860  fundmeng  6861  mapsnen  6865  fiprc  6869  unen  6870  xpsnen  6875  xpsneng  6876  xpcomco  6880  xpcomeng  6882  xpassen  6884  xpdom2  6885  xpdom2g  6886  pw2f1odc  6891  xpf1o  6900  mapen  6902  mapxpen  6904  xpmapenlem  6905  ssenen  6907  phplem4  6911  phplem3g  6912  nneneq  6913  php5  6914  phpm  6921  findcard  6944  findcard2  6945  findcard2s  6946  isinfinf  6953  ac6sfi  6954  exmidpw  6964  exmidpweq  6965  exmidpw2en  6968  unfidisj  6978  fiintim  6985  xpfi  6986  fisseneq  6988  ssfirab  6990  snexxph  7009  fidcenumlemr  7014  sbthlemi10  7025  isbth  7026  ssfii  7033  fi0  7034  fiss  7036  cnvinfex  7077  eqinfti  7079  infvalti  7081  infglbti  7084  infmoti  7087  ordiso2  7094  djuf1olem  7112  djuss  7129  ctm  7168  ctssdccl  7170  ctssdclemr  7171  finomni  7199  exmidomni  7201  fodjuomnilemdc  7203  nninfwlpoimlemginf  7235  pm54.43  7250  exmidfodomrlemim  7261  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  acfun  7267  ccfunen  7324  cc2lem  7326  cc3  7328  indpi  7402  dfplpq2  7414  enq0sym  7492  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nqnq0  7501  mulnnnq0  7510  nqprm  7602  nqprrnd  7603  nqprdisj  7604  nqprloc  7605  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  ltnqpr  7653  ltnqpri  7654  archpr  7703  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlem2  7720  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemopu  7759  suplocexprlemmu  7778  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  cnm  7892  ltresr  7899  peano1nnnn  7912  peano2nnnn  7913  axcnre  7941  axpre-apti  7945  renfdisj  8079  dfinfre  8975  1nn  8993  peano2nn  8994  indstr  9658  cnref1o  9716  ioof  10037  fzpr  10143  frec2uzrand  10476  frec2uzf1od  10477  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  frecfzennn  10497  seqp1g  10537  seqclg  10543  seqf1og  10592  seqfeq4g  10602  ser3le  10608  hashinfom  10849  hashunlem  10875  hashun  10876  hashxp  10897  hashfacen  10907  zfz1isolem1  10911  zfz1iso  10912  wrdexb  10926  shftfvalg  10962  ovshftex  10963  shftfibg  10964  shftfval  10965  shftfib  10967  shftfn  10968  2shfti  10975  shftvalg  10980  shftval4g  10981  maxabslemval  11352  fimaxre2  11370  xrmaxiflemval  11393  fclim  11437  climshft  11447  zsumdc  11527  fsum3  11530  fsum2dlemstep  11577  fsumcnv  11580  fisumcom2  11581  fisum0diag2  11590  fsumconst  11597  modfsummodlemstep  11600  fsumabs  11608  fsumrelem  11614  fsumiun  11620  ntrivcvgap  11691  fprod2dlemstep  11765  fprodcnv  11768  fprodcom2fi  11769  fprodmodd  11784  nninfct  12178  algrf  12183  qredeu  12235  isprm2  12255  prmind2  12258  4sqlemafi  12533  4sqlem12  12540  ennnfonelemex  12571  ennnfonelemrn  12576  exmidunben  12583  ctinfom  12585  ctinf  12587  qnnen  12588  enctlem  12589  ctiunctlemfo  12596  slotslfn  12644  setscomd  12659  restfn  12854  elrest  12857  ptex  12875  prdsex  12880  imasex  12888  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfnlemg  12897  fnpr2ob  12923  ismgm  12940  plusffng  12948  fn0g  12958  fngsum  12971  gsumsplit1r  12981  gsumprval  12982  issgrp  12986  ismnddef  12999  gsumfzz  13067  gsumfzcl  13071  mulgnngsum  13197  subgintm  13268  releqgg  13290  eqgex  13291  eqgfval  13292  eqgval  13293  isghm  13313  fnmgp  13418  isrng  13430  isring  13496  ringn0  13556  opprrngbg  13574  opprsubgg  13580  opprunitd  13606  dfrhm2  13650  rhmex  13653  opprsubrngg  13707  subrngintm  13708  subrngpropd  13712  subrgpropd  13749  isdomn  13765  opprdomnbg  13770  scaffng  13805  rmodislmodlem  13846  rmodislmod  13847  lssex  13850  lsssn0  13866  lss1d  13879  lssintclm  13880  ellspsn  13913  rlmfn  13949  isridl  14000  znval  14124  znleval  14141  psrval  14152  fnpsr  14153  bastg  14229  distop  14253  topnex  14254  epttop  14258  tgrest  14337  resttopon  14339  restco  14342  cnrest2  14404  cnptopresti  14406  cnptoprest  14407  cnptoprest2  14408  txuni2  14424  txbas  14426  eltx  14427  txcnp  14439  txcnmpt  14441  txrest  14444  txdis1cn  14446  txlm  14447  cnmpt1st  14456  cnmpt2nd  14457  txhmeo  14487  txswaphmeolem  14488  xmetec  14605  metrest  14674  reldvg  14833  dvfgg  14842  dvcj  14858  elply2  14881  pilem3  14918  lgsquadlem1  15191  bdcvv  15349  bdsnss  15365  bdop  15367  bj-vprc  15388  bdinex1g  15393  bdssexg  15396  bj-inex  15399  bj-zfpair2  15402  bj-uniexg  15410  bdunexb  15412  bj-unexg  15413  bj-indint  15423  bj-ssom  15428  bj-om  15429  bj-2inf  15430  bj-bdfindis  15439  bj-nn0suc0  15442  bj-nnelirr  15445  bj-inf2vnlem1  15462  bj-inf2vnlem2  15463  bj-omex2  15469  bj-nn0sucALT  15470  bj-findis  15471  ss1oel2o  15484  pw1nct  15493  nninfsellemeq  15504  exmidsbthrlem  15512