Theorem vex 2804

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

Syntax hints:   ∈ wcel 2201  Vcvv 2801

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-v 2803

This theorem is referenced by:  elv  2805  elvd  2806  el2v  2807  isset  2808  eqvisset  2812  ralv  2819  rexv  2820  reuv  2821  rmov  2822  rabab  2823  sbhypf  2852  ceqex  2932  ralab  2965  rexab  2967  mo2icl  2984  reu8  3001  csbvarg  3154  csbiebg  3169  sbcnestgf  3178  sbnfc2  3187  ddifnel  3337  ddifstab  3338  csbing  3413  unssdif  3441  unssin  3445  inssun  3446  invdif  3448  vn0  3504  vn0m  3505  eqv  3513  abvor0dc  3517  sbss  3601  velpw  3660  elpwg  3661  velsn  3687  vsnid  3702  exsnrex  3712  dftp2  3719  prmg  3795  prnzg  3798  snssgOLD  3810  difprsnss  3812  sneqrg  3846  preq12bg  3857  pwprss  3890  pwtpss  3891  pwv  3893  unipr  3908  uniprg  3909  unisng  3911  elintg  3937  elintrabg  3942  intss1  3944  ssint  3945  intmin  3949  intss  3950  intssunim  3951  intmin4  3957  intab  3958  intun  3960  intpr  3961  intprg  3962  uniintsnr  3965  iinconstm  3980  iuniin  3981  iinss1  3983  dfiin2g  4004  dfiunv2  4007  ssiinf  4021  iinss  4023  iinss2  4024  0iin  4030  iinab  4033  iundif2ss  4037  iindif2m  4039  iinin2m  4040  iinuniss  4054  sspwuni  4056  pwpwab  4059  iinpw  4062  iunpwss  4063  brab1  4137  csbopabg  4168  mptv  4187  trint  4203  vnex  4221  inex1g  4226  ssexg  4229  inteximm  4240  inuni  4246  repizf2  4254  axpweq  4263  bnd2  4265  pwuni  4284  exmidundif  4298  exmidundifim  4299  zfpair2  4302  rext  4309  sspwb  4310  unipw  4311  ssextss  4314  euabex  4319  mss  4320  exss  4321  opth  4331  opthg  4332  copsexg  4338  copsex4g  4341  moop2  4346  euotd  4349  opabid  4352  elopab  4354  opelopabsbALT  4355  opelopabsb  4356  opabm  4377  pwin  4381  pwunss  4382  epelg  4389  epel  4391  pofun  4411  epse  4441  tron  4481  sucel  4509  suctr  4520  vuniex  4537  uniexg  4538  unexb  4541  snnex  4547  pwnex  4548  uniuni  4550  eusvnf  4552  eusvnfb  4553  iunpw  4579  unon  4611  ordunisuc2r  4614  ordtri2or2exmidlem  4626  onsucelsucexmidlem  4629  ordsucunielexmid  4631  elirr  4641  en2lp  4654  dtruex  4659  onintexmid  4673  reg3exmidlemwe  4679  dcextest  4681  finds  4700  finds2  4701  elomssom  4705  limom  4714  0nelxp  4755  opelxp  4757  opeliunxp  4783  elvv  4790  elvvv  4791  elvvuni  4792  xpsspw  4840  relopabiv  4855  relopabi  4857  opabid2  4863  difopab  4865  xpiindim  4869  raliunxp  4873  rexiunxp  4874  ralxpf  4878  rexxpf  4879  relop  4882  cnvco  4917  dfrn2  4920  dfdm4  4925  dmss  4932  dmin  4941  dmiun  4942  dmuni  4943  dm0  4947  dmi  4948  reldm0  4951  reldmm  4952  elreldm  4960  elrnmpt1  4985  dmrnssfld  4997  dmcoss  5004  dmcosseq  5006  opelresg  5022  resieq  5025  dmres  5036  elres  5051  relssres  5053  resopab  5059  resiexg  5060  iss  5061  dfres2  5067  restidsing  5071  dfima2  5080  imadmrn  5088  imai  5094  csbima12g  5099  elimasng  5106  args  5107  epini  5109  iniseg  5110  dfse2  5111  exse2  5112  cotr  5120  issref  5121  cnvsym  5122  intasym  5123  asymref  5124  intirr  5125  brcodir  5126  codir  5127  qfto  5128  poirr2  5131  cnvopab  5140  cnv0  5142  cnvi  5143  cnvdif  5145  rniun  5149  dminss  5153  imainss  5154  inimasn  5156  xpmlem  5159  dmxpss  5169  rnxpid  5173  ssrnres  5181  rninxp  5182  dminxp  5183  cnvcnv3  5188  dfrel2  5189  dmsnm  5204  dmsnopg  5210  cnvcnvsn  5215  dmsnsnsng  5216  cnvsng  5224  elxp4  5226  elxp5  5227  cnvresima  5228  dfco2  5238  dfco2a  5239  cores  5242  resco  5243  imaco  5244  rnco  5245  coiun  5248  co02  5252  coi1  5254  coass  5257  relssdmrn  5259  unielrel  5266  ressn  5279  cnviinm  5280  cnvpom  5281  cnvsom  5282  uniabio  5299  iotaval  5300  iotass  5306  sniota  5319  csbiotag  5321  dffun2  5338  dffun7  5355  dffun8  5356  dffun9  5357  funopg  5362  funssres  5371  funun  5373  funcnvsn  5377  funinsn  5381  funcnv2  5392  funcnv  5393  funcnv3  5394  funcnveq  5395  fun2cnv  5396  funcnvuni  5401  imadif  5412  funimaexglem  5415  isarep1  5418  2elresin  5445  fnres  5451  fcnvres  5522  fconstg  5536  fun11iun  5607  f1osng  5629  dffv3g  5638  fvssunirng  5657  sefvex  5663  fv3  5665  fvres  5666  nfunsn  5679  funimass4  5699  ssimaexg  5711  dmfco  5717  fvopab6  5746  fndmdif  5755  fvelrn  5781  dffo4  5798  f1ompt  5801  fmptco  5816  fsn  5822  fsng  5823  fsn2g  5825  dfmpt  5828  dfmptg  5830  funopsn  5833  funop  5834  funopdmsn  5837  fnressn  5843  fressnfv  5844  fvsng  5853  resfunexg  5878  funfvima3  5893  idref  5902  abrexco  5905  imaiun  5906  dff13  5914  foeqcnvco  5936  f1eqcocnv  5937  fliftcnv  5941  isocnv2  5958  isoini  5964  isose  5967  riotav  5982  csbriotag  5990  acexmidlem2  6020  oprabid  6055  csbov123g  6062  0neqopab  6071  brabvv  6072  dfoprab2  6073  rnoprab  6109  eloprabga  6113  mpov  6116  f1opw  6235  opabex3d  6288  opabex3  6289  ofmres  6303  uchoice  6305  op1stg  6318  op2ndg  6319  1stval2  6323  2ndval2  6324  fo1st  6325  fo2nd  6326  f1stres  6327  f2ndres  6328  fo1stresm  6329  fo2ndresm  6330  xp1st  6333  xp2nd  6334  releldm2  6353  reldm  6354  sbcopeq1a  6355  csbopeq1a  6356  dfoprab3  6359  opabn1stprc  6363  eloprabi  6366  mpomptsx  6367  dmmpossx  6369  fmpox  6370  mpofvex  6375  mpoexxg  6380  fmpoco  6386  df1st2  6389  df2nd2  6390  1stconst  6391  2ndconst  6392  dfmpo  6393  fo2ndf  6397  f1o2ndf1  6398  xporderlem  6401  cnvoprab  6404  f1od2  6405  brtpos2  6422  reldmtpos  6424  dmtpos  6427  rntpos  6428  ovtposg  6430  dftpos3  6433  dftpos4  6434  tpostpos  6435  tpossym  6447  tfrlem3  6482  tfrlem5  6485  tfrlem8  6489  tfrlemisucfn  6495  tfrlemisucaccv  6496  tfrlemibxssdm  6498  tfrlemibfn  6499  tfrlemibex  6500  tfrlemi14d  6504  tfrexlem  6505  tfr1onlem3  6509  tfr1onlemsucaccv  6512  tfr1onlembxssdm  6514  tfr1onlembfn  6515  tfr1onlemres  6520  tfri1dALT  6522  tfrcllemsucaccv  6525  tfrcllembxssdm  6527  tfrcllembfn  6528  tfrcllemres  6533  tfrcl  6535  rdgtfr  6545  rdgruledefgg  6546  rdgivallem  6552  rdgon  6557  rdg0g  6559  frec0g  6568  frecabex  6569  frecabcl  6570  frectfr  6571  freccllem  6573  frecfcllem  6575  frecsuclem  6577  frecrdg  6579  oafnex  6617  sucinc  6618  fnoa  6620  oaexg  6621  omfnex  6622  fnom  6623  omexg  6624  fnoei  6625  oeiexg  6626  oeiv  6629  oacl  6633  omcl  6634  oeicl  6635  oav2  6636  nnsucelsuc  6664  nnsucuniel  6668  ercnv  6728  iserd  6733  eqerlem  6738  eqer  6739  ecdmn0m  6751  erth  6753  qsss  6768  ecid  6772  ecidg  6773  qsid  6774  iinerm  6781  qsel  6786  erovlem  6801  ecopovsym  6805  ecopover  6807  th3qlem2  6812  mapprc  6826  fnmap  6829  fnpm  6830  mapdm0  6837  mapval2  6852  mapsn  6864  mapsncnv  6869  mapsnf1o2  6870  ixpconstg  6881  ixpprc  6893  ixpin  6897  ixpiinm  6898  ixpssmap2g  6901  ixpssmapg  6902  elixpsn  6909  ixpsnf1o  6910  bren  6922  brdomg  6924  domen  6927  domeng  6928  idssen  6955  domssr  6956  ener  6958  domtr  6964  ensn1g  6976  en1  6978  en1bg  6979  fundmen  6986  fundmeng  6987  mapsnen  6991  fiprc  6995  unen  6996  rex2dom  7001  en2m  7004  dom1o  7007  xpsnen  7010  xpsneng  7011  xpcomco  7015  xpcomeng  7017  xpassen  7019  xpdom2  7020  xpdom2g  7021  pw2f1odc  7026  xpf1o  7035  mapen  7037  mapxpen  7039  xpmapenlem  7040  ssenen  7042  phplem4  7046  phplem3g  7047  nneneq  7048  php5  7049  phpm  7057  findcard  7082  findcard2  7083  findcard2s  7084  isinfinf  7091  ac6sfi  7092  exmidpw  7105  exmidpweq  7106  exmidpw2en  7109  unfidisj  7119  fiintim  7128  xpfi  7129  fisseneq  7132  ssfirab  7134  snexxph  7154  fidcenumlemr  7159  sbthlemi10  7170  isbth  7171  ssfii  7178  fi0  7179  fiss  7181  cnvinfex  7222  eqinfti  7224  infvalti  7226  infglbti  7229  infmoti  7232  ordiso2  7239  djuf1olem  7257  djuss  7274  ctm  7313  ctssdccl  7315  ctssdclemr  7316  finomni  7344  exmidomni  7346  fodjuomnilemdc  7348  nninfwlpoimlemginf  7380  pm54.43  7400  pr2cv1  7405  exmidfodomrlemim  7417  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  finacn  7424  acfun  7427  ccfunen  7488  cc2lem  7490  cc3  7492  acnccim  7496  indpi  7567  dfplpq2  7579  enq0sym  7657  enq0ref  7658  enq0tr  7659  nqnq0pi  7663  nqnq0  7666  mulnnnq0  7675  nqprm  7767  nqprrnd  7768  nqprdisj  7769  nqprloc  7770  nqprl  7776  nqpru  7777  addnqprlemrl  7782  addnqprlemru  7783  addnqprlemfl  7784  addnqprlemfu  7785  mulnqprlemrl  7798  mulnqprlemru  7799  mulnqprlemfl  7800  mulnqprlemfu  7801  ltnqpr  7818  ltnqpri  7819  archpr  7868  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  cauappcvgprlem2  7885  caucvgprlemladdfu  7902  caucvgprlem2  7905  caucvgprprlemopu  7924  suplocexprlemmu  7943  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemub  7948  cnm  8057  ltresr  8064  peano1nnnn  8077  peano2nnnn  8078  axcnre  8106  axpre-apti  8110  renfdisj  8244  dfinfre  9141  1nn  9159  peano2nn  9160  indstr  9832  cnref1o  9890  ioof  10211  fzpr  10317  frec2uzrand  10673  frec2uzf1od  10674  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  frecfzennn  10694  seqp1g  10734  seqclg  10740  seqf1og  10789  seqfeq4g  10799  ser3le  10805  hashinfom  11046  hashunlem  11073  hashun  11074  hashxp  11096  hashfacen  11106  zfz1isolem1  11110  zfz1iso  11111  fundm2domnop0  11118  wrdexb  11134  fnpfx  11267  cats1un  11311  wrdind  11312  wrd2ind  11313  shftfvalg  11401  ovshftex  11402  shftfibg  11403  shftfval  11404  shftfib  11406  shftfn  11407  2shfti  11414  shftvalg  11419  shftval4g  11420  maxabslemval  11791  fimaxre2  11810  xrmaxiflemval  11833  fclim  11877  climshft  11887  zsumdc  11968  fsum3  11971  fsum2dlemstep  12018  fsumcnv  12021  fisumcom2  12022  fisum0diag2  12031  fsumconst  12038  modfsummodlemstep  12041  fsumabs  12049  fsumrelem  12055  fsumiun  12061  ntrivcvgap  12132  fprod2dlemstep  12206  fprodcnv  12209  fprodcom2fi  12210  fprodmodd  12225  nninfct  12635  algrf  12640  qredeu  12692  isprm2  12712  prmind2  12715  4sqlemafi  12991  4sqlem12  12998  ennnfonelemex  13058  ennnfonelemrn  13063  exmidunben  13070  ctinfom  13072  ctinf  13074  qnnen  13075  enctlem  13076  ctiunctlemfo  13083  slotslfn  13131  setscomd  13146  restfn  13349  elrest  13352  ptex  13370  prdsex  13375  prdsvallem  13378  prdsval  13379  prdsbaslemss  13380  prdsbas  13382  imasex  13411  imasival  13412  imasbas  13413  imasplusg  13414  imasmulr  13415  imasaddfnlemg  13420  fnpr2ob  13446  ismgm  13463  plusffng  13471  fn0g  13481  fngsum  13494  gsumsplit1r  13504  gsumprval  13505  issgrp  13509  ismnddef  13524  gsumfzz  13601  gsumfzcl  13605  mulgnngsum  13737  subgintm  13808  releqgg  13830  eqgex  13831  eqgfval  13832  eqgval  13833  isghm  13853  fnmgp  13959  isrng  13971  isring  14037  ringn0  14097  opprrngbg  14115  opprsubgg  14121  opprunitd  14148  dfrhm2  14192  rhmex  14195  opprsubrngg  14249  subrngintm  14250  subrngpropd  14254  subrgpropd  14291  isdomn  14307  opprdomnbg  14312  scaffng  14347  rmodislmodlem  14388  rmodislmod  14389  lssex  14392  lsssn0  14408  lss1d  14421  lssintclm  14422  ellspsn  14455  rlmfn  14491  isridl  14542  blfn  14589  mopnset  14590  metuex  14593  znval  14674  znleval  14691  psrval  14704  fnpsr  14705  mplvalcoe  14733  fnmpl  14736  bastg  14814  distop  14838  topnex  14839  epttop  14843  tgrest  14922  resttopon  14924  restco  14927  cnrest2  14989  cnptopresti  14991  cnptoprest  14992  cnptoprest2  14993  txuni2  15009  txbas  15011  eltx  15012  txcnp  15024  txcnmpt  15026  txrest  15029  txdis1cn  15031  txlm  15032  cnmpt1st  15041  cnmpt2nd  15042  txhmeo  15072  txswaphmeolem  15073  xmetec  15190  metrest  15259  reldvg  15432  dvfgg  15441  dvcj  15462  dvmptfsum  15478  elply2  15488  pilem3  15536  lgsquadlem1  15835  lgsquadlem2  15836  upgrex  15983  upgr1een  16004  umgredg  16025  umgredgnlp  16032  usgredgreu  16096  uspgredg2vtxeu  16098  ushgredgedg  16106  ushgredgedgloop  16108  griedg0ssusgr  16131  uhgrspansubgrlem  16156  upgrspanop  16163  umgrspanop  16164  usgrspanop  16165  wlkvtxiedg  16225  wlkvtxiedgg  16226  wlk1walkdom  16239  eulerpathum  16361  depindlem1  16386  bdcvv  16512  bdsnss  16528  bdop  16530  bj-vprc  16551  bdinex1g  16556  bdssexg  16559  bj-inex  16562  bj-zfpair2  16565  bj-uniexg  16573  bdunexb  16575  bj-unexg  16576  bj-indint  16586  bj-ssom  16591  bj-om  16592  bj-2inf  16593  bj-bdfindis  16602  bj-nn0suc0  16605  bj-nnelirr  16608  bj-inf2vnlem1  16625  bj-inf2vnlem2  16626  bj-omex2  16632  bj-nn0sucALT  16633  bj-findis  16634  ss1oel2o  16646  domomsubct  16662  pw1nct  16664  nninfsellemeq  16679  exmidsbthrlem  16689  gfsumval  16748