Theorem vex 2741

Description: All setvar variables are sets (see isset 2744). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	|- x e. _V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		equid 1701	. 2 |- x = x
2		df-v 2740	. . 3 |- _V = { x | x = x }
3	2	abeq2i 2288	. 2 |- ( x e. _V <-> x = x )
4	1, 3	mpbir 146	1 |- x e. _V

Syntax hints:   e. wcel 2148   _Vcvv 2738

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  elv  2742  elvd  2743  isset  2744  eqvisset  2748  ralv  2755  rexv  2756  reuv  2757  rmov  2758  rabab  2759  sbhypf  2787  ceqex  2865  ralab  2898  rexab  2900  mo2icl  2917  reu8  2934  csbvarg  3086  csbiebg  3100  sbcnestgf  3109  sbnfc2  3118  ddifnel  3267  ddifstab  3268  csbing  3343  unssdif  3371  unssin  3375  inssun  3376  invdif  3378  vn0  3434  vn0m  3435  eqv  3443  abvor0dc  3447  sbss  3532  velpw  3583  elpwg  3584  velsn  3610  vsnid  3625  exsnrex  3635  dftp2  3642  prmg  3714  prnzg  3717  snssgOLD  3729  difprsnss  3731  sneqrg  3763  preq12bg  3774  pwprss  3806  pwtpss  3807  pwv  3809  unipr  3824  uniprg  3825  unisng  3827  elintg  3853  elintrabg  3858  intss1  3860  ssint  3861  intmin  3865  intss  3866  intssunim  3867  intmin4  3873  intab  3874  intun  3876  intpr  3877  intprg  3878  uniintsnr  3881  iinconstm  3896  iuniin  3897  iinss1  3899  dfiin2g  3920  dfiunv2  3923  ssiinf  3937  iinss  3939  iinss2  3940  0iin  3946  iinab  3949  iundif2ss  3953  iindif2m  3955  iinin2m  3956  iinuniss  3970  sspwuni  3972  pwpwab  3975  iinpw  3978  iunpwss  3979  brab1  4051  csbopabg  4082  mptv  4101  trint  4117  vnex  4135  inex1g  4140  ssexg  4143  inteximm  4150  inuni  4156  repizf2  4163  axpweq  4172  bnd2  4174  pwuni  4193  exmidundif  4207  exmidundifim  4208  zfpair2  4211  rext  4216  sspwb  4217  unipw  4218  ssextss  4221  euabex  4226  mss  4227  exss  4228  opth  4238  opthg  4239  copsexg  4245  copsex4g  4248  moop2  4252  euotd  4255  opabid  4258  elopab  4259  opelopabsbALT  4260  opelopabsb  4261  opabm  4281  pwin  4283  pwunss  4284  epelg  4291  epel  4293  pofun  4313  epse  4343  tron  4383  sucel  4411  suctr  4422  vuniex  4439  uniexg  4440  unexb  4443  snnex  4449  pwnex  4450  uniuni  4452  eusvnf  4454  eusvnfb  4455  iunpw  4481  unon  4511  ordunisuc2r  4514  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  ordsucunielexmid  4531  elirr  4541  en2lp  4554  dtruex  4559  onintexmid  4573  reg3exmidlemwe  4579  dcextest  4581  finds  4600  finds2  4601  elomssom  4605  limom  4614  0nelxp  4655  opelxp  4657  opeliunxp  4682  elvv  4689  elvvv  4690  elvvuni  4691  xpsspw  4739  relopabi  4753  opabid2  4759  difopab  4761  xpiindim  4765  raliunxp  4769  rexiunxp  4770  ralxpf  4774  rexxpf  4775  relop  4778  cnvco  4813  dfrn2  4816  dfdm4  4820  dmss  4827  dmin  4836  dmiun  4837  dmuni  4838  dm0  4842  dmi  4843  reldm0  4846  elreldm  4854  elrnmpt1  4879  dmrnssfld  4891  dmcoss  4897  dmcosseq  4899  opelresg  4915  resieq  4918  dmres  4929  elres  4944  relssres  4946  resopab  4952  resiexg  4953  iss  4954  dfres2  4960  restidsing  4964  dfima2  4973  imadmrn  4981  imai  4985  csbima12g  4990  elimasng  4997  args  4998  epini  5000  iniseg  5001  dfse2  5002  exse2  5003  cotr  5011  issref  5012  cnvsym  5013  intasym  5014  asymref  5015  intirr  5016  brcodir  5017  codir  5018  qfto  5019  poirr2  5022  cnvopab  5031  cnv0  5033  cnvi  5034  cnvdif  5036  rniun  5040  dminss  5044  imainss  5045  inimasn  5047  xpmlem  5050  dmxpss  5060  rnxpid  5064  ssrnres  5072  rninxp  5073  dminxp  5074  cnvcnv3  5079  dfrel2  5080  dmsnm  5095  dmsnopg  5101  cnvcnvsn  5106  dmsnsnsng  5107  cnvsng  5115  elxp4  5117  elxp5  5118  cnvresima  5119  dfco2  5129  dfco2a  5130  cores  5133  resco  5134  imaco  5135  rnco  5136  coiun  5139  co02  5143  coi1  5145  coass  5148  relssdmrn  5150  unielrel  5157  ressn  5170  cnviinm  5171  cnvpom  5172  cnvsom  5173  uniabio  5189  iotaval  5190  iotass  5196  sniota  5208  csbiotag  5210  dffun2  5227  dffun7  5244  dffun8  5245  dffun9  5246  funopg  5251  funssres  5259  funun  5261  funcnvsn  5262  funinsn  5266  funcnv2  5277  funcnv  5278  funcnv3  5279  funcnveq  5280  fun2cnv  5281  funcnvuni  5286  imadif  5297  funimaexglem  5300  isarep1  5303  2elresin  5328  fnres  5333  fcnvres  5400  fconstg  5413  fun11iun  5483  f1osng  5503  dffv3g  5512  fvssunirng  5531  sefvex  5537  fv3  5539  fvres  5540  nfunsn  5550  funimass4  5567  ssimaexg  5579  dmfco  5585  fvopab6  5613  fndmdif  5622  fvelrn  5648  dffo4  5665  f1ompt  5668  fmptco  5683  fsn  5689  fsng  5690  dfmpt  5694  dfmptg  5696  fnressn  5703  fressnfv  5704  fvsng  5713  resfunexg  5738  funfvima3  5751  idref  5758  abrexco  5760  imaiun  5761  dff13  5769  foeqcnvco  5791  f1eqcocnv  5792  fliftcnv  5796  isocnv2  5813  isoini  5819  isose  5822  riotav  5836  csbriotag  5843  acexmidlem2  5872  oprabid  5907  csbov123g  5913  0neqopab  5920  brabvv  5921  dfoprab2  5922  rnoprab  5958  eloprabga  5962  mpov  5965  f1opw  6078  opabex3d  6122  opabex3  6123  ofmres  6137  op1stg  6151  op2ndg  6152  1stval2  6156  2ndval2  6157  fo1st  6158  fo2nd  6159  f1stres  6160  f2ndres  6161  fo1stresm  6162  fo2ndresm  6163  xp1st  6166  xp2nd  6167  releldm2  6186  reldm  6187  sbcopeq1a  6188  csbopeq1a  6189  dfoprab3  6192  eloprabi  6197  mpomptsx  6198  dmmpossx  6200  fmpox  6201  mpofvex  6204  mpoexxg  6211  fmpoco  6217  df1st2  6220  df2nd2  6221  1stconst  6222  2ndconst  6223  dfmpo  6224  fo2ndf  6228  f1o2ndf1  6229  xporderlem  6232  cnvoprab  6235  f1od2  6236  brtpos2  6252  reldmtpos  6254  dmtpos  6257  rntpos  6258  ovtposg  6260  dftpos3  6263  dftpos4  6264  tpostpos  6265  tpossym  6277  tfrlem3  6312  tfrlem5  6315  tfrlem8  6319  tfrlemisucfn  6325  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemibex  6330  tfrlemi14d  6334  tfrexlem  6335  tfr1onlem3  6339  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemres  6363  tfrcl  6365  rdgtfr  6375  rdgruledefgg  6376  rdgivallem  6382  rdgon  6387  rdg0g  6389  frec0g  6398  frecabex  6399  frecabcl  6400  frectfr  6401  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecrdg  6409  oafnex  6445  sucinc  6446  fnoa  6448  oaexg  6449  omfnex  6450  fnom  6451  omexg  6452  fnoei  6453  oeiexg  6454  oeiv  6457  oacl  6461  omcl  6462  oeicl  6463  oav2  6464  nnsucelsuc  6492  nnsucuniel  6496  ercnv  6556  iserd  6561  eqerlem  6566  eqer  6567  ecdmn0m  6577  erth  6579  qsss  6594  ecid  6598  ecidg  6599  qsid  6600  iinerm  6607  qsel  6612  erovlem  6627  ecopovsym  6631  ecopover  6633  th3qlem2  6638  mapprc  6652  fnmap  6655  fnpm  6656  mapdm0  6663  mapval2  6678  mapsn  6690  mapsncnv  6695  mapsnf1o2  6696  ixpconstg  6707  ixpprc  6719  ixpin  6723  ixpiinm  6724  ixpssmap2g  6727  ixpssmapg  6728  elixpsn  6735  ixpsnf1o  6736  bren  6747  brdomg  6748  domen  6751  domeng  6752  idssen  6777  ener  6779  domtr  6785  ensn1g  6797  en1  6799  en1bg  6800  fundmen  6806  fundmeng  6807  mapsnen  6811  fiprc  6815  unen  6816  xpsnen  6821  xpsneng  6822  xpcomco  6826  xpcomeng  6828  xpassen  6830  xpdom2  6831  xpdom2g  6832  xpf1o  6844  mapen  6846  mapxpen  6848  xpmapenlem  6849  ssenen  6851  phplem4  6855  phplem3g  6856  nneneq  6857  php5  6858  phpm  6865  findcard  6888  findcard2  6889  findcard2s  6890  isinfinf  6897  ac6sfi  6898  exmidpw  6908  exmidpweq  6909  unfidisj  6921  fiintim  6928  xpfi  6929  fisseneq  6931  ssfirab  6933  snexxph  6949  fidcenumlemr  6954  sbthlemi10  6965  isbth  6966  ssfii  6973  fi0  6974  fiss  6976  cnvinfex  7017  eqinfti  7019  infvalti  7021  infglbti  7024  infmoti  7027  ordiso2  7034  djuf1olem  7052  djuss  7069  ctm  7108  ctssdccl  7110  ctssdclemr  7111  finomni  7138  exmidomni  7140  fodjuomnilemdc  7142  nninfwlpoimlemginf  7174  pm54.43  7189  exmidfodomrlemim  7200  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  acfun  7206  ccfunen  7263  cc2lem  7265  cc3  7267  indpi  7341  dfplpq2  7353  enq0sym  7431  enq0ref  7432  enq0tr  7433  nqnq0pi  7437  nqnq0  7440  mulnnnq0  7449  nqprm  7541  nqprrnd  7542  nqprdisj  7543  nqprloc  7544  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  ltnqpr  7592  ltnqpri  7593  archpr  7642  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlem2  7659  caucvgprlemladdfu  7676  caucvgprlem2  7679  caucvgprprlemopu  7698  suplocexprlemmu  7717  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  cnm  7831  ltresr  7838  peano1nnnn  7851  peano2nnnn  7852  axcnre  7880  axpre-apti  7884  renfdisj  8017  dfinfre  8913  1nn  8930  peano2nn  8931  indstr  9593  cnref1o  9650  ioof  9971  fzpr  10077  frec2uzrand  10405  frec2uzf1od  10406  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  frecfzennn  10426  ser3le  10518  hashinfom  10758  hashunlem  10784  hashun  10785  hashxp  10806  hashfacen  10816  zfz1isolem1  10820  zfz1iso  10821  shftfvalg  10827  ovshftex  10828  shftfibg  10829  shftfval  10830  shftfib  10832  shftfn  10833  2shfti  10840  shftvalg  10845  shftval4g  10846  maxabslemval  11217  fimaxre2  11235  xrmaxiflemval  11258  fclim  11302  climshft  11312  zsumdc  11392  fsum3  11395  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  fisum0diag2  11455  fsumconst  11462  modfsummodlemstep  11465  fsumabs  11473  fsumrelem  11479  fsumiun  11485  ntrivcvgap  11556  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodmodd  11649  algrf  12045  qredeu  12097  isprm2  12117  prmind2  12120  ennnfonelemex  12415  ennnfonelemrn  12420  exmidunben  12427  ctinfom  12429  ctinf  12431  qnnen  12432  enctlem  12433  ctiunctlemfo  12440  slotslfn  12488  setscomd  12503  restfn  12692  elrest  12695  ptex  12713  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfnlemg  12735  fnpr2ob  12759  ismgm  12776  plusffng  12784  fn0g  12794  issgrp  12809  ismnddef  12819  subgintm  13058  releqgg  13080  eqgfval  13081  eqgval  13082  fnmgp  13132  isring  13183  ringn0  13237  opprunitd  13279  subrgpropd  13369  scaffng  13399  rmodislmodlem  13440  rmodislmod  13441  bastg  13564  distop  13588  topnex  13589  epttop  13593  tgrest  13672  resttopon  13674  restco  13677  cnrest2  13739  cnptopresti  13741  cnptoprest  13742  cnptoprest2  13743  txuni2  13759  txbas  13761  eltx  13762  txcnp  13774  txcnmpt  13776  txrest  13779  txdis1cn  13781  txlm  13782  cnmpt1st  13791  cnmpt2nd  13792  txhmeo  13822  txswaphmeolem  13823  xmetec  13940  metrest  14009  reldvg  14151  dvfgg  14160  dvcj  14176  pilem3  14207  bdcvv  14612  bdsnss  14628  bdop  14630  bj-vprc  14651  bdinex1g  14656  bdssexg  14659  bj-inex  14662  bj-zfpair2  14665  bj-uniexg  14673  bdunexb  14675  bj-unexg  14676  bj-indint  14686  bj-ssom  14691  bj-om  14692  bj-2inf  14693  bj-bdfindis  14702  bj-nn0suc0  14705  bj-nnelirr  14708  bj-inf2vnlem1  14725  bj-inf2vnlem2  14726  bj-omex2  14732  bj-nn0sucALT  14733  bj-findis  14734  ss1oel2o  14746  pw1nct  14755  nninfsellemeq  14766  exmidsbthrlem  14773