Theorem vex 2818

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

Syntax hints:   ∈ wcel 2205  Vcvv 2815

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  elv  2819  elvd  2820  el2v  2821  isset  2822  eqvisset  2826  ralv  2833  rexv  2834  reuv  2835  rmov  2836  rabab  2837  sbhypf  2866  ceqex  2946  ralab  2979  rexab  2981  mo2icl  2998  reu8  3015  csbvarg  3168  csbiebg  3183  sbcnestgf  3192  sbnfc2  3201  ddifnel  3352  ddifstab  3353  csbing  3430  unssdif  3458  unssin  3462  inssun  3463  invdif  3465  vn0  3521  vn0m  3522  eqv  3530  abvor0dc  3534  sbss  3619  velpw  3678  elpwg  3679  velsn  3708  vsnid  3723  exsnrex  3733  dftp2  3740  prmg  3816  prnzg  3819  snssgOLD  3832  difprsnss  3834  sneqrg  3868  preq12bg  3879  pwprss  3912  pwtpss  3913  pwv  3915  unipr  3930  uniprg  3931  unisng  3933  elintg  3959  elintrabg  3964  intss1  3966  ssint  3967  intmin  3971  intss  3972  intssunim  3973  intmin4  3979  intab  3980  intun  3982  intpr  3983  intprg  3984  uniintsnr  3987  iinconstm  4002  iuniin  4003  iinss1  4005  dfiin2g  4026  dfiunv2  4029  ssiinf  4043  iinss  4045  iinss2  4046  0iin  4052  iinab  4055  iundif2ss  4059  iindif2m  4061  iinin2m  4062  iinuniss  4076  sspwuni  4078  pwpwab  4081  iinpw  4084  iunpwss  4085  brab1  4159  csbopabg  4190  mptv  4209  trint  4225  vnex  4243  inex1g  4248  ssexg  4251  inteximm  4263  inuni  4269  repizf2  4277  axpweq  4286  bnd2  4288  pwuni  4307  exmidundif  4321  exmidundifim  4322  zfpair2  4325  rext  4333  sspwb  4334  unipw  4335  ssextss  4338  euabex  4343  mss  4344  exss  4345  opth  4355  opthg  4356  copsexg  4362  copsex4g  4365  moop2  4370  euotd  4373  opabid  4376  elopab  4378  opelopabsbALT  4379  opelopabsb  4380  opabm  4401  pwin  4405  pwunss  4406  epelg  4413  epel  4415  pofun  4435  epse  4465  tron  4505  sucel  4533  suctr  4544  vuniex  4561  uniexg  4562  unexb  4565  snnex  4571  pwnex  4572  uniuni  4574  eusvnf  4576  eusvnfb  4577  iunpw  4603  unon  4635  ordunisuc2r  4638  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  ordsucunielexmid  4655  elirr  4665  en2lp  4678  dtruex  4683  onintexmid  4697  reg3exmidlemwe  4703  dcextest  4705  finds  4724  finds2  4725  elomssom  4729  limom  4738  0nelxp  4779  opelxp  4781  opeliunxp  4807  elvv  4814  elvvv  4815  elvvuni  4816  xpsspw  4864  relopabiv  4880  relopabi  4882  opabid2  4888  difopab  4890  xpiindim  4894  raliunxp  4898  rexiunxp  4899  ralxpf  4903  rexxpf  4904  relop  4907  cnvco  4942  dfrn2  4945  dfdm4  4950  dmss  4957  dmin  4966  dmiun  4967  dmuni  4968  dm0  4972  dmi  4973  reldm0  4976  reldmm  4977  elreldm  4985  elrnmpt1  5010  dmrnssfld  5022  dmcoss  5029  dmcosseq  5031  opelresg  5047  resieq  5050  dmres  5061  elres  5076  relssres  5078  resopab  5084  resiexg  5085  iss  5086  dfres2  5092  restidsing  5096  dfima2  5105  imadmrn  5113  imai  5120  csbima12g  5125  elimasng  5132  args  5133  epini  5135  iniseg  5136  dfse2  5137  exse2  5138  cotr  5146  issref  5147  cnvsym  5148  intasym  5149  asymref  5150  intirr  5151  brcodir  5152  codir  5153  qfto  5154  poirr2  5157  cnvopab  5166  cnv0  5168  cnvi  5169  cnvdif  5171  rniun  5175  dminss  5179  imainss  5180  inimasn  5182  xpmlem  5185  dmxpss  5195  rnxpid  5199  ssrnres  5207  rninxp  5208  dminxp  5209  cnvcnv3  5214  dfrel2  5215  dmsnm  5230  dmsnopg  5236  cnvcnvsn  5241  dmsnsnsng  5242  cnvsng  5250  elxp4  5252  elxp5  5253  cnvresima  5254  dfco2  5264  dfco2a  5265  cores  5268  resco  5269  imaco  5270  rnco  5271  coiun  5274  co02  5278  coi1  5280  coass  5283  relssdmrn  5285  unielrel  5292  ressn  5305  cnviinm  5306  cnvpom  5307  cnvsom  5308  uniabio  5325  iotaval  5326  iotass  5332  sniota  5345  csbiotag  5347  dffun2  5364  dffun7  5381  dffun8  5382  dffun9  5383  funopg  5388  funssres  5397  funun  5399  funcnvsn  5403  funinsn  5407  funcnv2  5418  funcnv  5419  funcnv3  5420  funcnveq  5421  fun2cnv  5422  funcnvuni  5427  imadif  5438  funimaexglem  5441  isarep1  5444  2elresin  5471  fnres  5477  fcnvres  5552  fconstg  5566  fun11iun  5637  f1osng  5659  dffv3g  5668  fvssunirng  5687  sefvex  5693  fv3  5695  fvres  5696  nfunsn  5709  funimass4  5729  ssimaexg  5741  dmfco  5747  fvopab6  5776  fndmdif  5785  fvelrn  5810  dffo4  5827  f1ompt  5830  fmptco  5845  fsn  5851  fsng  5852  fsn2g  5854  dfmpt  5857  dfmptg  5859  funopsn  5862  funop  5863  funopdmsn  5866  fnressn  5872  fressnfv  5873  fvsng  5882  resfunexg  5907  funfvima3  5922  idref  5931  abrexco  5934  imaiun  5935  dff13  5943  foeqcnvco  5965  f1eqcocnv  5966  fliftcnv  5970  isocnv2  5987  isoini  5993  isose  5996  riotav  6011  csbriotag  6019  acexmidlem2  6049  oprabid  6084  csbov123g  6091  0neqopab  6100  brabvv  6101  dfoprab2  6102  rnoprab  6138  eloprabga  6142  mpov  6145  f1opw  6264  opabex3d  6316  opabex3  6317  ofmres  6331  uchoice  6333  op1stg  6346  op2ndg  6347  1stval2  6351  2ndval2  6352  fo1st  6353  fo2nd  6354  f1stres  6355  f2ndres  6356  fo1stresm  6357  fo2ndresm  6358  xp1st  6361  xp2nd  6362  releldm2  6381  reldm  6382  sbcopeq1a  6383  csbopeq1a  6384  dfoprab3  6387  opabn1stprc  6391  eloprabi  6394  mpomptsx  6395  dmmpossx  6397  fmpox  6398  mpofvex  6403  mpoexxg  6408  fmpoco  6414  df1st2  6417  df2nd2  6418  1stconst  6419  2ndconst  6420  dfmpo  6421  fo2ndf  6425  f1o2ndf1  6426  xporderlem  6429  cnvoprab  6432  f1od2  6433  suppval1  6441  cnvimadfsn  6447  suppimacnvfn  6448  brtpos2  6484  reldmtpos  6486  dmtpos  6489  rntpos  6490  ovtposg  6492  dftpos3  6495  dftpos4  6496  tpostpos  6497  tpossym  6509  tfrlem3  6544  tfrlem5  6547  tfrlem8  6551  tfrlemisucfn  6557  tfrlemisucaccv  6558  tfrlemibxssdm  6560  tfrlemibfn  6561  tfrlemibex  6562  tfrlemi14d  6566  tfrexlem  6567  tfr1onlem3  6571  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemres  6582  tfri1dALT  6584  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemres  6595  tfrcl  6597  rdgtfr  6607  rdgruledefgg  6608  rdgivallem  6614  rdgon  6619  rdg0g  6621  frec0g  6630  frecabex  6631  frecabcl  6632  frectfr  6633  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecrdg  6641  oafnex  6679  sucinc  6680  fnoa  6682  oaexg  6683  omfnex  6684  fnom  6685  omexg  6686  fnoei  6687  oeiexg  6688  oeiv  6691  oacl  6695  omcl  6696  oeicl  6697  oav2  6698  nnsucelsuc  6726  nnsucuniel  6730  ercnv  6790  iserd  6795  eqerlem  6800  eqer  6801  ecdmn0m  6813  erth  6815  qsss  6830  ecid  6834  ecidg  6835  qsid  6836  iinerm  6843  qsel  6848  erovlem  6863  ecopovsym  6867  ecopover  6869  th3qlem2  6874  mapprc  6888  fnmap  6891  fnpm  6892  mapdm0  6899  mapval2  6914  mapsnd  6925  mapsn  6927  mapsncnv  6932  mapsnf1o2  6933  ixpconstg  6944  ixpprc  6956  ixpin  6960  ixpiinm  6961  ixpssmap2g  6964  ixpssmapg  6965  elixpsn  6972  ixpsnf1o  6973  bren  6985  brdomg  6987  domen  6990  domeng  6991  idssen  7018  domssr  7019  ener  7021  domtr  7027  ensn1g  7039  en1  7041  en1bg  7042  fundmen  7049  fundmeng  7050  mapsnend  7054  mapsnen  7055  fiprc  7059  unen  7060  rex2dom  7065  en2m  7068  dom1o  7071  xpsnen  7074  xpsneng  7075  xpcomco  7079  xpcomeng  7081  xpassen  7083  xpdom2  7084  xpdom2g  7085  pw2f1odc  7090  xpf1o  7099  mapen  7101  mapxpen  7103  xpmapenlem  7104  mapunen  7106  ssenen  7107  phplem4  7111  phplem3g  7112  nneneq  7113  php5  7114  phpm  7122  findcard  7147  findcard2  7148  findcard2s  7149  isinfinf  7156  ac6sfi  7157  exmidpw  7170  exmidpweq  7171  exmidpw2en  7174  unfidisj  7184  fiintim  7193  xpfi  7194  fisseneq  7197  ssfirab  7199  mapfi  7216  snexxph  7222  fidcenumlemr  7227  sbthlemi10  7238  isbth  7239  ssfii  7263  fi0  7264  fiss  7266  cnvinfex  7311  eqinfti  7313  infvalti  7315  infglbti  7318  infmoti  7321  ordiso2  7328  djuf1olem  7346  djuss  7363  ctm  7402  ctssdccl  7404  ctssdclemr  7405  finomni  7433  exmidomni  7435  fodjuomnilemdc  7437  nninfwlpoimlemginf  7469  pm54.43  7489  pr2cv1  7494  exmidfodomrlemim  7506  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  finacn  7513  acfun  7516  ccfunen  7583  cc2lem  7585  cc3  7587  acnccim  7591  indpi  7662  dfplpq2  7674  enq0sym  7752  enq0ref  7753  enq0tr  7754  nqnq0pi  7758  nqnq0  7761  mulnnnq0  7770  nqprm  7862  nqprrnd  7863  nqprdisj  7864  nqprloc  7865  nqprl  7871  nqpru  7872  addnqprlemrl  7877  addnqprlemru  7878  addnqprlemfl  7879  addnqprlemfu  7880  mulnqprlemrl  7893  mulnqprlemru  7894  mulnqprlemfl  7895  mulnqprlemfu  7896  ltnqpr  7913  ltnqpri  7914  archpr  7963  cauappcvgprlemladdfu  7974  cauappcvgprlemladdfl  7975  cauappcvgprlem2  7980  caucvgprlemladdfu  7997  caucvgprlem2  8000  caucvgprprlemopu  8019  suplocexprlemmu  8038  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemub  8043  cnm  8152  ltresr  8159  peano1nnnn  8172  peano2nnnn  8173  axcnre  8201  axpre-apti  8205  renfdisj  8338  dfinfre  9235  1nn  9253  peano2nn  9254  indstr  9931  cnref1o  9989  ioof  10310  fzpr  10418  frec2uzrand  10774  frec2uzf1od  10775  frecuzrdgtcl  10781  frecuzrdgfunlem  10788  frecfzennn  10795  seqp1g  10835  seqclg  10841  seqf1og  10890  seqfeq4g  10900  ser3le  10906  hashinfom  11149  hashunlem  11176  hashun  11177  hashxp  11199  hashmap  11200  hashfibclem  11214  hashfacen  11216  zfz1isolem1  11220  zfz1iso  11221  fundm2domnop0  11228  wrdexb  11244  fnpfx  11377  cats1un  11421  wrdind  11422  wrd2ind  11423  shftfvalg  11511  ovshftex  11512  shftfibg  11513  shftfval  11514  shftfib  11516  shftfn  11517  2shfti  11524  shftvalg  11529  shftval4g  11530  maxabslemval  11901  fimaxre2  11920  xrmaxiflemval  11943  fclim  11987  climshft  11997  zsumdc  12078  fsum3  12081  fsum2dlemstep  12128  fsumcnv  12131  fisumcom2  12132  fisum0diag2  12141  fsumconst  12148  modfsummodlemstep  12151  fsumabs  12159  fsumrelem  12165  fsumiun  12171  ntrivcvgap  12242  fprod2dlemstep  12316  fprodcnv  12319  fprodcom2fi  12320  fprodmodd  12335  nninfct  12745  algrf  12750  qredeu  12802  isprm2  12822  prmind2  12825  4sqlemafi  13101  4sqlem12  13108  ballotfilemcdc  13150  ennnfonelemex  13186  ennnfonelemrn  13191  exmidunben  13198  ctinfom  13200  ctinf  13202  qnnen  13203  enctlem  13204  ctiunctlemfo  13211  slotslfn  13259  setscomd  13274  restfn  13477  elrest  13480  ptex  13498  prdsex  13503  prdsvallem  13506  prdsval  13507  prdsbaslemss  13508  prdsbas  13510  imasex  13539  imasival  13540  imasbas  13541  imasplusg  13542  imasmulr  13543  imasaddfnlemg  13548  fnpr2ob  13574  ismgm  13591  plusffng  13599  fn0g  13609  fngsum  13622  gsumsplit1r  13632  gsumprval  13633  issgrp  13637  ismnddef  13652  gsumfzz  13729  gsumfzcl  13733  mulgnngsum  13865  subgintm  13936  releqgg  13958  eqgex  13959  eqgfval  13960  eqgval  13961  isghm  13981  fnmgp  14087  isrng  14099  isring  14165  ringn0  14225  opprrngbg  14243  opprsubgg  14250  opprunitd  14277  dfrhm2  14321  rhmex  14324  opprsubrngg  14379  subrngintm  14380  subrngpropd  14384  subrgpropd  14421  isdomn  14438  opprdomnbg  14443  scaffng  14506  rmodislmodlem  14547  rmodislmod  14548  lssex  14551  lsssn0  14567  lss1d  14580  lssintclm  14581  ellspsn  14614  rlmfn  14650  isridl  14701  blfn  14748  mopnset  14749  metuex  14752  znval  14833  znleval  14850  psrval  14863  fnpsr  14864  mplvalcoe  14894  fnmpl  14897  bastg  14975  distop  14999  topnex  15000  epttop  15004  tgrest  15083  resttopon  15085  restco  15088  cnrest2  15150  cnptopresti  15152  cnptoprest  15153  cnptoprest2  15154  txuni2  15170  txbas  15172  eltx  15173  txcnp  15185  txcnmpt  15187  txrest  15190  txdis1cn  15192  txlm  15193  cnmpt1st  15202  cnmpt2nd  15203  txhmeo  15233  txswaphmeolem  15234  xmetec  15351  metrest  15420  reldvg  15593  dvfgg  15602  dvcj  15623  dvmptfsum  15639  elply2  15649  pilem3  15697  lgsquadlem1  15999  lgsquadlem2  16000  upgrex  16147  upgr1een  16168  umgredg  16189  umgredgnlp  16196  usgredgreu  16260  uspgredg2vtxeu  16262  ushgredgedg  16270  ushgredgedgloop  16272  griedg0ssusgr  16295  uhgrspansubgrlem  16320  upgrspanop  16327  umgrspanop  16328  usgrspanop  16329  wlkvtxiedg  16389  wlkvtxiedgg  16390  wlk1walkdom  16403  eulerpathum  16525  depindlem1  16550  bdcvv  16676  bdsnss  16692  bdop  16694  bj-vprc  16715  bdinex1g  16720  bdssexg  16723  bj-inex  16726  bj-zfpair2  16729  bj-uniexg  16737  bdunexb  16739  bj-unexg  16740  bj-indint  16750  bj-ssom  16755  bj-om  16756  bj-2inf  16757  bj-bdfindis  16766  bj-nn0suc0  16769  bj-nnelirr  16772  bj-inf2vnlem1  16789  bj-inf2vnlem2  16790  bj-omex2  16796  bj-nn0sucALT  16797  bj-findis  16798  ss1oel2o  16810  domomsubct  16824  pw1nct  16826  nninfsellemeq  16841  exmidsbthrlem  16851  gfsumval  16911