Theorem vex 2692

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

Syntax hints:   ∈ wcel 1481  Vcvv 2689

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  elv  2693  elvd  2694  isset  2695  eqvisset  2699  ralv  2706  rexv  2707  reuv  2708  rmov  2709  rabab  2710  sbhypf  2738  ceqex  2816  ralab  2848  rexab  2850  mo2icl  2867  reu8  2884  csbvarg  3035  csbiebg  3047  sbcnestgf  3056  sbnfc2  3065  ddifnel  3212  ddifstab  3213  csbing  3288  unssdif  3316  unssin  3320  inssun  3321  invdif  3323  vn0  3378  vn0m  3379  eqv  3387  abvor0dc  3391  sbss  3476  velpw  3522  elpwg  3523  velsn  3549  vsnid  3564  exsnrex  3573  dftp2  3580  prmg  3652  prnzg  3655  snssg  3664  difprsnss  3666  sneqrg  3697  preq12bg  3708  pwprss  3740  pwtpss  3741  pwv  3743  unipr  3758  uniprg  3759  unisng  3761  elintg  3787  elintrabg  3792  intss1  3794  ssint  3795  intmin  3799  intss  3800  intssunim  3801  intmin4  3807  intab  3808  intun  3810  intpr  3811  intprg  3812  uniintsnr  3815  iinconstm  3830  iuniin  3831  iinss1  3833  dfiin2g  3854  dfiunv2  3857  ssiinf  3870  iinss  3872  iinss2  3873  0iin  3879  iinab  3882  iundif2ss  3886  iindif2m  3888  iinin2m  3889  iinuniss  3903  sspwuni  3905  pwpwab  3908  iinpw  3911  iunpwss  3912  brab1  3983  csbopabg  4014  mptv  4033  trint  4049  vnex  4067  inex1g  4072  ssexg  4075  inteximm  4082  inuni  4088  repizf2  4094  axpweq  4103  bnd2  4105  pwuni  4124  exmidundif  4137  exmidundifim  4138  zfpair2  4140  rext  4145  sspwb  4146  unipw  4147  ssextss  4150  euabex  4155  mss  4156  exss  4157  opth  4167  opthg  4168  copsexg  4174  copsex4g  4177  moop2  4181  euotd  4184  opabid  4187  elopab  4188  opelopabsbALT  4189  opelopabsb  4190  opabm  4210  pwin  4212  pwunss  4213  epelg  4220  epel  4222  pofun  4242  epse  4272  tron  4312  sucel  4340  suctr  4351  vuniex  4368  uniexg  4369  unexb  4371  snnex  4377  pwnex  4378  uniuni  4380  eusvnf  4382  eusvnfb  4383  iunpw  4409  unon  4435  ordunisuc2r  4438  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  ordsucunielexmid  4454  elirr  4464  en2lp  4477  dtruex  4482  onintexmid  4495  reg3exmidlemwe  4501  dcextest  4503  finds  4522  finds2  4523  elnn  4527  limom  4535  0nelxp  4575  opelxp  4577  opeliunxp  4602  elvv  4609  elvvv  4610  elvvuni  4611  xpsspw  4659  relopabi  4673  opabid2  4678  difopab  4680  xpiindim  4684  raliunxp  4688  rexiunxp  4689  ralxpf  4693  rexxpf  4694  relop  4697  cnvco  4732  dfrn2  4735  dfdm4  4739  dmss  4746  dmin  4755  dmiun  4756  dmuni  4757  dm0  4761  dmi  4762  reldm0  4765  elreldm  4773  elrnmpt1  4798  dmrnssfld  4810  dmcoss  4816  dmcosseq  4818  opelresg  4834  resieq  4837  dmres  4848  elres  4863  relssres  4865  resopab  4871  resiexg  4872  iss  4873  dfres2  4879  dfima2  4891  imadmrn  4899  imai  4903  csbima12g  4908  elimasng  4915  args  4916  epini  4918  iniseg  4919  dfse2  4920  exse2  4921  cotr  4928  issref  4929  cnvsym  4930  intasym  4931  asymref  4932  intirr  4933  brcodir  4934  codir  4935  qfto  4936  poirr2  4939  cnvopab  4948  cnv0  4950  cnvi  4951  cnvdif  4953  rniun  4957  dminss  4961  imainss  4962  inimasn  4964  xpmlem  4967  dmxpss  4977  rnxpid  4981  ssrnres  4989  rninxp  4990  dminxp  4991  cnvcnv3  4996  dfrel2  4997  dmsnm  5012  dmsnopg  5018  cnvcnvsn  5023  dmsnsnsng  5024  cnvsng  5032  elxp4  5034  elxp5  5035  cnvresima  5036  dfco2  5046  dfco2a  5047  cores  5050  resco  5051  imaco  5052  rnco  5053  coiun  5056  co02  5060  coi1  5062  coass  5065  relssdmrn  5067  unielrel  5074  ressn  5087  cnviinm  5088  cnvpom  5089  cnvsom  5090  uniabio  5106  iotaval  5107  iotass  5113  sniota  5123  csbiotag  5124  dffun2  5141  dffun7  5158  dffun8  5159  dffun9  5160  funopg  5165  funssres  5173  funun  5175  funcnvsn  5176  funinsn  5180  funcnv2  5191  funcnv  5192  funcnv3  5193  funcnveq  5194  fun2cnv  5195  funcnvuni  5200  imadif  5211  funimaexglem  5214  isarep1  5217  2elresin  5242  fnres  5247  fcnvres  5314  fconstg  5327  fun11iun  5396  f1osng  5416  dffv3g  5425  fvssunirng  5444  sefvex  5450  fv3  5452  fvres  5453  nfunsn  5463  funimass4  5480  ssimaexg  5491  dmfco  5497  fvopab6  5525  fndmdif  5533  fvelrn  5559  dffo4  5576  f1ompt  5579  fmptco  5594  fsn  5600  fsng  5601  dfmpt  5605  dfmptg  5607  fnressn  5614  fressnfv  5615  fvsng  5624  resfunexg  5649  funfvima3  5659  idref  5666  abrexco  5668  imaiun  5669  dff13  5677  foeqcnvco  5699  f1eqcocnv  5700  fliftcnv  5704  isocnv2  5721  isoini  5727  isose  5730  riotav  5743  csbriotag  5750  acexmidlem2  5779  oprabid  5811  csbov123g  5817  0neqopab  5824  brabvv  5825  dfoprab2  5826  rnoprab  5862  eloprabga  5866  mpov  5869  f1opw  5985  opabex3d  6027  opabex3  6028  ofmres  6042  op1stg  6056  op2ndg  6057  1stval2  6061  2ndval2  6062  fo1st  6063  fo2nd  6064  f1stres  6065  f2ndres  6066  fo1stresm  6067  fo2ndresm  6068  xp1st  6071  xp2nd  6072  releldm2  6091  reldm  6092  sbcopeq1a  6093  csbopeq1a  6094  dfoprab3  6097  eloprabi  6102  mpomptsx  6103  dmmpossx  6105  fmpox  6106  mpofvex  6109  mpoexxg  6116  fmpoco  6121  df1st2  6124  df2nd2  6125  1stconst  6126  2ndconst  6127  dfmpo  6128  fo2ndf  6132  f1o2ndf1  6133  xporderlem  6136  cnvoprab  6139  f1od2  6140  brtpos2  6156  reldmtpos  6158  dmtpos  6161  rntpos  6162  ovtposg  6164  dftpos3  6167  dftpos4  6168  tpostpos  6169  tpossym  6181  tfrlem3  6216  tfrlem5  6219  tfrlem8  6223  tfrlemisucfn  6229  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrlemibex  6234  tfrlemi14d  6238  tfrexlem  6239  tfr1onlem3  6243  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemres  6254  tfri1dALT  6256  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemres  6267  tfrcl  6269  rdgtfr  6279  rdgruledefgg  6280  rdgivallem  6286  rdgon  6291  rdg0g  6293  frec0g  6302  frecabex  6303  frecabcl  6304  frectfr  6305  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecrdg  6313  oafnex  6348  sucinc  6349  fnoa  6351  oaexg  6352  omfnex  6353  fnom  6354  omexg  6355  fnoei  6356  oeiexg  6357  oeiv  6360  oacl  6364  omcl  6365  oeicl  6366  oav2  6367  nnsucelsuc  6395  nnsucuniel  6399  ercnv  6458  iserd  6463  eqerlem  6468  eqer  6469  ecdmn0m  6479  erth  6481  qsss  6496  ecid  6500  ecidg  6501  qsid  6502  iinerm  6509  qsel  6514  erovlem  6529  ecopovsym  6533  ecopover  6535  th3qlem2  6540  mapprc  6554  fnmap  6557  fnpm  6558  mapdm0  6565  mapval2  6580  mapsn  6592  mapsncnv  6597  mapsnf1o2  6598  ixpconstg  6609  ixpprc  6621  ixpin  6625  ixpiinm  6626  ixpssmap2g  6629  ixpssmapg  6630  elixpsn  6637  ixpsnf1o  6638  bren  6649  brdomg  6650  domen  6653  domeng  6654  idssen  6679  ener  6681  domtr  6687  ensn1g  6699  en1  6701  en1bg  6702  fundmen  6708  fundmeng  6709  mapsnen  6713  fiprc  6717  unen  6718  xpsnen  6723  xpsneng  6724  xpcomco  6728  xpcomeng  6730  xpassen  6732  xpdom2  6733  xpdom2g  6734  xpf1o  6746  mapen  6748  mapxpen  6750  xpmapenlem  6751  ssenen  6753  phplem4  6757  phplem3g  6758  nneneq  6759  php5  6760  phpm  6767  findcard  6790  findcard2  6791  findcard2s  6792  isinfinf  6799  ac6sfi  6800  exmidpw  6810  unfidisj  6818  fiintim  6825  xpfi  6826  fisseneq  6828  ssfirab  6830  snexxph  6846  fidcenumlemr  6851  sbthlemi10  6862  isbth  6863  ssfii  6870  fi0  6871  fiss  6873  cnvinfex  6913  eqinfti  6915  infvalti  6917  infglbti  6920  infmoti  6923  ordiso2  6928  djuf1olem  6946  djuss  6963  ctm  7002  ctssdccl  7004  ctssdclemr  7005  finomni  7020  exmidomni  7022  fodjuomnilemdc  7024  pm54.43  7063  exmidfodomrlemim  7074  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  cc2lem  7098  cc3  7100  indpi  7174  dfplpq2  7186  enq0sym  7264  enq0ref  7265  enq0tr  7266  nqnq0pi  7270  nqnq0  7273  mulnnnq0  7282  nqprm  7374  nqprrnd  7375  nqprdisj  7376  nqprloc  7377  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemrl  7405  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  ltnqpr  7425  ltnqpri  7426  archpr  7475  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlem2  7492  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemopu  7531  suplocexprlemmu  7550  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  cnm  7664  ltresr  7671  peano1nnnn  7684  peano2nnnn  7685  axcnre  7713  axpre-apti  7717  renfdisj  7848  dfinfre  8738  1nn  8755  peano2nn  8756  indstr  9415  cnref1o  9469  ioof  9784  fzpr  9888  frec2uzrand  10209  frec2uzf1od  10210  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  frecfzennn  10230  ser3le  10322  hashinfom  10556  hashunlem  10582  hashun  10583  hashxp  10604  hashfacen  10611  zfz1isolem1  10615  zfz1iso  10616  shftfvalg  10622  ovshftex  10623  shftfibg  10624  shftfval  10625  shftfib  10627  shftfn  10628  2shfti  10635  shftvalg  10640  shftval4g  10641  maxabslemval  11012  fimaxre2  11030  xrmaxiflemval  11051  fclim  11095  climshft  11105  zsumdc  11185  fsum3  11188  fsum2dlemstep  11235  fsumcnv  11238  fisumcom2  11239  fisum0diag2  11248  fsumconst  11255  modfsummodlemstep  11258  fsumabs  11266  fsumrelem  11272  fsumiun  11278  ntrivcvgap  11349  algrf  11762  qredeu  11814  isprm2  11834  prmind2  11837  ennnfonelemex  11963  ennnfonelemrn  11968  exmidunben  11975  ctinfom  11977  ctinf  11979  qnnen  11980  enctlem  11981  ctiunctlemfo  11988  slotslfn  12024  restfn  12163  elrest  12166  bastg  12269  distop  12293  topnex  12294  epttop  12298  tgrest  12377  resttopon  12379  restco  12382  cnrest2  12444  cnptopresti  12446  cnptoprest  12447  cnptoprest2  12448  txuni2  12464  txbas  12466  eltx  12467  txcnp  12479  txcnmpt  12481  txrest  12484  txdis1cn  12486  txlm  12487  cnmpt1st  12496  cnmpt2nd  12497  txhmeo  12527  txswaphmeolem  12528  xmetec  12645  metrest  12714  reldvg  12856  dvfgg  12865  dvcj  12881  pilem3  12912  bdcvv  13226  bdsnss  13242  bdop  13244  bj-vprc  13265  bdinex1g  13270  bdssexg  13273  bj-inex  13276  bj-zfpair2  13279  bj-uniexg  13287  bdunexb  13289  bj-unexg  13290  bj-indint  13300  bj-ssom  13305  bj-om  13306  bj-2inf  13307  bj-bdfindis  13316  bj-nn0suc0  13319  bj-nnelirr  13322  bj-inf2vnlem1  13339  bj-inf2vnlem2  13340  bj-omex2  13346  bj-nn0sucALT  13347  bj-findis  13348  ss1oel2o  13360  pw1nct  13371  nninfsellemeq  13385  exmidsbthrlem  13392