Theorem vex 2803

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

Syntax hints:   ∈ wcel 2200  Vcvv 2800

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  elv  2804  elvd  2805  el2v  2806  isset  2807  eqvisset  2811  ralv  2818  rexv  2819  reuv  2820  rmov  2821  rabab  2822  sbhypf  2851  ceqex  2931  ralab  2964  rexab  2966  mo2icl  2983  reu8  3000  csbvarg  3153  csbiebg  3168  sbcnestgf  3177  sbnfc2  3186  ddifnel  3336  ddifstab  3337  csbing  3412  unssdif  3440  unssin  3444  inssun  3445  invdif  3447  vn0  3503  vn0m  3504  eqv  3512  abvor0dc  3516  sbss  3600  velpw  3657  elpwg  3658  velsn  3684  vsnid  3699  exsnrex  3709  dftp2  3716  prmg  3792  prnzg  3795  snssgOLD  3807  difprsnss  3809  sneqrg  3843  preq12bg  3854  pwprss  3887  pwtpss  3888  pwv  3890  unipr  3905  uniprg  3906  unisng  3908  elintg  3934  elintrabg  3939  intss1  3941  ssint  3942  intmin  3946  intss  3947  intssunim  3948  intmin4  3954  intab  3955  intun  3957  intpr  3958  intprg  3959  uniintsnr  3962  iinconstm  3977  iuniin  3978  iinss1  3980  dfiin2g  4001  dfiunv2  4004  ssiinf  4018  iinss  4020  iinss2  4021  0iin  4027  iinab  4030  iundif2ss  4034  iindif2m  4036  iinin2m  4037  iinuniss  4051  sspwuni  4053  pwpwab  4056  iinpw  4059  iunpwss  4060  brab1  4134  csbopabg  4165  mptv  4184  trint  4200  vnex  4218  inex1g  4223  ssexg  4226  inteximm  4237  inuni  4243  repizf2  4250  axpweq  4259  bnd2  4261  pwuni  4280  exmidundif  4294  exmidundifim  4295  zfpair2  4298  rext  4305  sspwb  4306  unipw  4307  ssextss  4310  euabex  4315  mss  4316  exss  4317  opth  4327  opthg  4328  copsexg  4334  copsex4g  4337  moop2  4342  euotd  4345  opabid  4348  elopab  4350  opelopabsbALT  4351  opelopabsb  4352  opabm  4373  pwin  4377  pwunss  4378  epelg  4385  epel  4387  pofun  4407  epse  4437  tron  4477  sucel  4505  suctr  4516  vuniex  4533  uniexg  4534  unexb  4537  snnex  4543  pwnex  4544  uniuni  4546  eusvnf  4548  eusvnfb  4549  iunpw  4575  unon  4607  ordunisuc2r  4610  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  ordsucunielexmid  4627  elirr  4637  en2lp  4650  dtruex  4655  onintexmid  4669  reg3exmidlemwe  4675  dcextest  4677  finds  4696  finds2  4697  elomssom  4701  limom  4710  0nelxp  4751  opelxp  4753  opeliunxp  4779  elvv  4786  elvvv  4787  elvvuni  4788  xpsspw  4836  relopabiv  4851  relopabi  4853  opabid2  4859  difopab  4861  xpiindim  4865  raliunxp  4869  rexiunxp  4870  ralxpf  4874  rexxpf  4875  relop  4878  cnvco  4913  dfrn2  4916  dfdm4  4921  dmss  4928  dmin  4937  dmiun  4938  dmuni  4939  dm0  4943  dmi  4944  reldm0  4947  reldmm  4948  elreldm  4956  elrnmpt1  4981  dmrnssfld  4993  dmcoss  5000  dmcosseq  5002  opelresg  5018  resieq  5021  dmres  5032  elres  5047  relssres  5049  resopab  5055  resiexg  5056  iss  5057  dfres2  5063  restidsing  5067  dfima2  5076  imadmrn  5084  imai  5090  csbima12g  5095  elimasng  5102  args  5103  epini  5105  iniseg  5106  dfse2  5107  exse2  5108  cotr  5116  issref  5117  cnvsym  5118  intasym  5119  asymref  5120  intirr  5121  brcodir  5122  codir  5123  qfto  5124  poirr2  5127  cnvopab  5136  cnv0  5138  cnvi  5139  cnvdif  5141  rniun  5145  dminss  5149  imainss  5150  inimasn  5152  xpmlem  5155  dmxpss  5165  rnxpid  5169  ssrnres  5177  rninxp  5178  dminxp  5179  cnvcnv3  5184  dfrel2  5185  dmsnm  5200  dmsnopg  5206  cnvcnvsn  5211  dmsnsnsng  5212  cnvsng  5220  elxp4  5222  elxp5  5223  cnvresima  5224  dfco2  5234  dfco2a  5235  cores  5238  resco  5239  imaco  5240  rnco  5241  coiun  5244  co02  5248  coi1  5250  coass  5253  relssdmrn  5255  unielrel  5262  ressn  5275  cnviinm  5276  cnvpom  5277  cnvsom  5278  uniabio  5295  iotaval  5296  iotass  5302  sniota  5315  csbiotag  5317  dffun2  5334  dffun7  5351  dffun8  5352  dffun9  5353  funopg  5358  funssres  5366  funun  5368  funcnvsn  5372  funinsn  5376  funcnv2  5387  funcnv  5388  funcnv3  5389  funcnveq  5390  fun2cnv  5391  funcnvuni  5396  imadif  5407  funimaexglem  5410  isarep1  5413  2elresin  5440  fnres  5446  fcnvres  5517  fconstg  5530  fun11iun  5601  f1osng  5622  dffv3g  5631  fvssunirng  5650  sefvex  5656  fv3  5658  fvres  5659  nfunsn  5672  funimass4  5692  ssimaexg  5704  dmfco  5710  fvopab6  5739  fndmdif  5748  fvelrn  5774  dffo4  5791  f1ompt  5794  fmptco  5809  fsn  5815  fsng  5816  dfmpt  5820  dfmptg  5822  funopsn  5825  funop  5826  funopdmsn  5829  fnressn  5835  fressnfv  5836  fvsng  5845  resfunexg  5870  funfvima3  5883  idref  5892  abrexco  5895  imaiun  5896  dff13  5904  foeqcnvco  5926  f1eqcocnv  5927  fliftcnv  5931  isocnv2  5948  isoini  5954  isose  5957  riotav  5972  csbriotag  5980  acexmidlem2  6010  oprabid  6045  csbov123g  6052  0neqopab  6061  brabvv  6062  dfoprab2  6063  rnoprab  6099  eloprabga  6103  mpov  6106  f1opw  6225  opabex3d  6278  opabex3  6279  ofmres  6293  uchoice  6295  op1stg  6308  op2ndg  6309  1stval2  6313  2ndval2  6314  fo1st  6315  fo2nd  6316  f1stres  6317  f2ndres  6318  fo1stresm  6319  fo2ndresm  6320  xp1st  6323  xp2nd  6324  releldm2  6343  reldm  6344  sbcopeq1a  6345  csbopeq1a  6346  dfoprab3  6349  opabn1stprc  6353  eloprabi  6356  mpomptsx  6357  dmmpossx  6359  fmpox  6360  mpofvex  6365  mpoexxg  6370  fmpoco  6376  df1st2  6379  df2nd2  6380  1stconst  6381  2ndconst  6382  dfmpo  6383  fo2ndf  6387  f1o2ndf1  6388  xporderlem  6391  cnvoprab  6394  f1od2  6395  brtpos2  6412  reldmtpos  6414  dmtpos  6417  rntpos  6418  ovtposg  6420  dftpos3  6423  dftpos4  6424  tpostpos  6425  tpossym  6437  tfrlem3  6472  tfrlem5  6475  tfrlem8  6479  tfrlemisucfn  6485  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemibex  6490  tfrlemi14d  6494  tfrexlem  6495  tfr1onlem3  6499  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  tfrcl  6525  rdgtfr  6535  rdgruledefgg  6536  rdgivallem  6542  rdgon  6547  rdg0g  6549  frec0g  6558  frecabex  6559  frecabcl  6560  frectfr  6561  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  oafnex  6607  sucinc  6608  fnoa  6610  oaexg  6611  omfnex  6612  fnom  6613  omexg  6614  fnoei  6615  oeiexg  6616  oeiv  6619  oacl  6623  omcl  6624  oeicl  6625  oav2  6626  nnsucelsuc  6654  nnsucuniel  6658  ercnv  6718  iserd  6723  eqerlem  6728  eqer  6729  ecdmn0m  6741  erth  6743  qsss  6758  ecid  6762  ecidg  6763  qsid  6764  iinerm  6771  qsel  6776  erovlem  6791  ecopovsym  6795  ecopover  6797  th3qlem2  6802  mapprc  6816  fnmap  6819  fnpm  6820  mapdm0  6827  mapval2  6842  mapsn  6854  mapsncnv  6859  mapsnf1o2  6860  ixpconstg  6871  ixpprc  6883  ixpin  6887  ixpiinm  6888  ixpssmap2g  6891  ixpssmapg  6892  elixpsn  6899  ixpsnf1o  6900  bren  6912  brdomg  6914  domen  6917  domeng  6918  idssen  6945  domssr  6946  ener  6948  domtr  6954  ensn1g  6966  en1  6968  en1bg  6969  fundmen  6976  fundmeng  6977  mapsnen  6981  fiprc  6985  unen  6986  rex2dom  6991  en2m  6994  dom1o  6997  xpsnen  7000  xpsneng  7001  xpcomco  7005  xpcomeng  7007  xpassen  7009  xpdom2  7010  xpdom2g  7011  pw2f1odc  7016  xpf1o  7025  mapen  7027  mapxpen  7029  xpmapenlem  7030  ssenen  7032  phplem4  7036  phplem3g  7037  nneneq  7038  php5  7039  phpm  7047  findcard  7072  findcard2  7073  findcard2s  7074  isinfinf  7081  ac6sfi  7082  exmidpw  7095  exmidpweq  7096  exmidpw2en  7099  unfidisj  7109  fiintim  7118  xpfi  7119  fisseneq  7121  ssfirab  7123  snexxph  7143  fidcenumlemr  7148  sbthlemi10  7159  isbth  7160  ssfii  7167  fi0  7168  fiss  7170  cnvinfex  7211  eqinfti  7213  infvalti  7215  infglbti  7218  infmoti  7221  ordiso2  7228  djuf1olem  7246  djuss  7263  ctm  7302  ctssdccl  7304  ctssdclemr  7305  finomni  7333  exmidomni  7335  fodjuomnilemdc  7337  nninfwlpoimlemginf  7369  pm54.43  7389  pr2cv1  7394  exmidfodomrlemim  7405  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  finacn  7412  acfun  7415  ccfunen  7476  cc2lem  7478  cc3  7480  acnccim  7484  indpi  7555  dfplpq2  7567  enq0sym  7645  enq0ref  7646  enq0tr  7647  nqnq0pi  7651  nqnq0  7654  mulnnnq0  7663  nqprm  7755  nqprrnd  7756  nqprdisj  7757  nqprloc  7758  nqprl  7764  nqpru  7765  addnqprlemrl  7770  addnqprlemru  7771  addnqprlemfl  7772  addnqprlemfu  7773  mulnqprlemrl  7786  mulnqprlemru  7787  mulnqprlemfl  7788  mulnqprlemfu  7789  ltnqpr  7806  ltnqpri  7807  archpr  7856  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlem2  7873  caucvgprlemladdfu  7890  caucvgprlem2  7893  caucvgprprlemopu  7912  suplocexprlemmu  7931  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemub  7936  cnm  8045  ltresr  8052  peano1nnnn  8065  peano2nnnn  8066  axcnre  8094  axpre-apti  8098  renfdisj  8232  dfinfre  9129  1nn  9147  peano2nn  9148  indstr  9820  cnref1o  9878  ioof  10199  fzpr  10305  frec2uzrand  10660  frec2uzf1od  10661  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  frecfzennn  10681  seqp1g  10721  seqclg  10727  seqf1og  10776  seqfeq4g  10786  ser3le  10792  hashinfom  11033  hashunlem  11060  hashun  11061  hashxp  11083  hashfacen  11093  zfz1isolem1  11097  zfz1iso  11098  fundm2domnop0  11102  wrdexb  11118  fnpfx  11251  cats1un  11295  wrdind  11296  wrd2ind  11297  shftfvalg  11372  ovshftex  11373  shftfibg  11374  shftfval  11375  shftfib  11377  shftfn  11378  2shfti  11385  shftvalg  11390  shftval4g  11391  maxabslemval  11762  fimaxre2  11781  xrmaxiflemval  11804  fclim  11848  climshft  11858  zsumdc  11938  fsum3  11941  fsum2dlemstep  11988  fsumcnv  11991  fisumcom2  11992  fisum0diag2  12001  fsumconst  12008  modfsummodlemstep  12011  fsumabs  12019  fsumrelem  12025  fsumiun  12031  ntrivcvgap  12102  fprod2dlemstep  12176  fprodcnv  12179  fprodcom2fi  12180  fprodmodd  12195  nninfct  12605  algrf  12610  qredeu  12662  isprm2  12682  prmind2  12685  4sqlemafi  12961  4sqlem12  12968  ennnfonelemex  13028  ennnfonelemrn  13033  exmidunben  13040  ctinfom  13042  ctinf  13044  qnnen  13045  enctlem  13046  ctiunctlemfo  13053  slotslfn  13101  setscomd  13116  restfn  13319  elrest  13322  ptex  13340  prdsex  13345  prdsvallem  13348  prdsval  13349  prdsbaslemss  13350  prdsbas  13352  imasex  13381  imasival  13382  imasbas  13383  imasplusg  13384  imasmulr  13385  imasaddfnlemg  13390  fnpr2ob  13416  ismgm  13433  plusffng  13441  fn0g  13451  fngsum  13464  gsumsplit1r  13474  gsumprval  13475  issgrp  13479  ismnddef  13494  gsumfzz  13571  gsumfzcl  13575  mulgnngsum  13707  subgintm  13778  releqgg  13800  eqgex  13801  eqgfval  13802  eqgval  13803  isghm  13823  fnmgp  13928  isrng  13940  isring  14006  ringn0  14066  opprrngbg  14084  opprsubgg  14090  opprunitd  14117  dfrhm2  14161  rhmex  14164  opprsubrngg  14218  subrngintm  14219  subrngpropd  14223  subrgpropd  14260  isdomn  14276  opprdomnbg  14281  scaffng  14316  rmodislmodlem  14357  rmodislmod  14358  lssex  14361  lsssn0  14377  lss1d  14390  lssintclm  14391  ellspsn  14424  rlmfn  14460  isridl  14511  blfn  14558  mopnset  14559  metuex  14562  znval  14643  znleval  14660  psrval  14673  fnpsr  14674  mplvalcoe  14697  fnmpl  14700  bastg  14778  distop  14802  topnex  14803  epttop  14807  tgrest  14886  resttopon  14888  restco  14891  cnrest2  14953  cnptopresti  14955  cnptoprest  14956  cnptoprest2  14957  txuni2  14973  txbas  14975  eltx  14976  txcnp  14988  txcnmpt  14990  txrest  14993  txdis1cn  14995  txlm  14996  cnmpt1st  15005  cnmpt2nd  15006  txhmeo  15036  txswaphmeolem  15037  xmetec  15154  metrest  15223  reldvg  15396  dvfgg  15405  dvcj  15426  dvmptfsum  15442  elply2  15452  pilem3  15500  lgsquadlem1  15799  lgsquadlem2  15800  upgrex  15947  upgr1een  15968  umgredg  15989  umgredgnlp  15996  usgredgreu  16060  uspgredg2vtxeu  16062  ushgredgedg  16070  ushgredgedgloop  16072  griedg0ssusgr  16095  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlk1walkdom  16170  bdcvv  16402  bdsnss  16418  bdop  16420  bj-vprc  16441  bdinex1g  16446  bdssexg  16449  bj-inex  16452  bj-zfpair2  16455  bj-uniexg  16463  bdunexb  16465  bj-unexg  16466  bj-indint  16476  bj-ssom  16481  bj-om  16482  bj-2inf  16483  bj-bdfindis  16492  bj-nn0suc0  16495  bj-nnelirr  16498  bj-inf2vnlem1  16515  bj-inf2vnlem2  16516  bj-omex2  16522  bj-nn0sucALT  16523  bj-findis  16524  ss1oel2o  16536  domomsubct  16552  pw1nct  16554  nninfsellemeq  16566  exmidsbthrlem  16576  gfsumval  16630