Theorem vex 2805

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

Syntax hints:   ∈ wcel 2202  Vcvv 2802

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 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elv  2806  elvd  2807  el2v  2808  isset  2809  eqvisset  2813  ralv  2820  rexv  2821  reuv  2822  rmov  2823  rabab  2824  sbhypf  2853  ceqex  2933  ralab  2966  rexab  2968  mo2icl  2985  reu8  3002  csbvarg  3155  csbiebg  3170  sbcnestgf  3179  sbnfc2  3188  ddifnel  3338  ddifstab  3339  csbing  3414  unssdif  3442  unssin  3446  inssun  3447  invdif  3449  vn0  3505  vn0m  3506  eqv  3514  abvor0dc  3518  sbss  3602  velpw  3659  elpwg  3660  velsn  3686  vsnid  3701  exsnrex  3711  dftp2  3718  prmg  3794  prnzg  3797  snssgOLD  3809  difprsnss  3811  sneqrg  3845  preq12bg  3856  pwprss  3889  pwtpss  3890  pwv  3892  unipr  3907  uniprg  3908  unisng  3910  elintg  3936  elintrabg  3941  intss1  3943  ssint  3944  intmin  3948  intss  3949  intssunim  3950  intmin4  3956  intab  3957  intun  3959  intpr  3960  intprg  3961  uniintsnr  3964  iinconstm  3979  iuniin  3980  iinss1  3982  dfiin2g  4003  dfiunv2  4006  ssiinf  4020  iinss  4022  iinss2  4023  0iin  4029  iinab  4032  iundif2ss  4036  iindif2m  4038  iinin2m  4039  iinuniss  4053  sspwuni  4055  pwpwab  4058  iinpw  4061  iunpwss  4062  brab1  4136  csbopabg  4167  mptv  4186  trint  4202  vnex  4220  inex1g  4225  ssexg  4228  inteximm  4239  inuni  4245  repizf2  4252  axpweq  4261  bnd2  4263  pwuni  4282  exmidundif  4296  exmidundifim  4297  zfpair2  4300  rext  4307  sspwb  4308  unipw  4309  ssextss  4312  euabex  4317  mss  4318  exss  4319  opth  4329  opthg  4330  copsexg  4336  copsex4g  4339  moop2  4344  euotd  4347  opabid  4350  elopab  4352  opelopabsbALT  4353  opelopabsb  4354  opabm  4375  pwin  4379  pwunss  4380  epelg  4387  epel  4389  pofun  4409  epse  4439  tron  4479  sucel  4507  suctr  4518  vuniex  4535  uniexg  4536  unexb  4539  snnex  4545  pwnex  4546  uniuni  4548  eusvnf  4550  eusvnfb  4551  iunpw  4577  unon  4609  ordunisuc2r  4612  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordsucunielexmid  4629  elirr  4639  en2lp  4652  dtruex  4657  onintexmid  4671  reg3exmidlemwe  4677  dcextest  4679  finds  4698  finds2  4699  elomssom  4703  limom  4712  0nelxp  4753  opelxp  4755  opeliunxp  4781  elvv  4788  elvvv  4789  elvvuni  4790  xpsspw  4838  relopabiv  4853  relopabi  4855  opabid2  4861  difopab  4863  xpiindim  4867  raliunxp  4871  rexiunxp  4872  ralxpf  4876  rexxpf  4877  relop  4880  cnvco  4915  dfrn2  4918  dfdm4  4923  dmss  4930  dmin  4939  dmiun  4940  dmuni  4941  dm0  4945  dmi  4946  reldm0  4949  reldmm  4950  elreldm  4958  elrnmpt1  4983  dmrnssfld  4995  dmcoss  5002  dmcosseq  5004  opelresg  5020  resieq  5023  dmres  5034  elres  5049  relssres  5051  resopab  5057  resiexg  5058  iss  5059  dfres2  5065  restidsing  5069  dfima2  5078  imadmrn  5086  imai  5092  csbima12g  5097  elimasng  5104  args  5105  epini  5107  iniseg  5108  dfse2  5109  exse2  5110  cotr  5118  issref  5119  cnvsym  5120  intasym  5121  asymref  5122  intirr  5123  brcodir  5124  codir  5125  qfto  5126  poirr2  5129  cnvopab  5138  cnv0  5140  cnvi  5141  cnvdif  5143  rniun  5147  dminss  5151  imainss  5152  inimasn  5154  xpmlem  5157  dmxpss  5167  rnxpid  5171  ssrnres  5179  rninxp  5180  dminxp  5181  cnvcnv3  5186  dfrel2  5187  dmsnm  5202  dmsnopg  5208  cnvcnvsn  5213  dmsnsnsng  5214  cnvsng  5222  elxp4  5224  elxp5  5225  cnvresima  5226  dfco2  5236  dfco2a  5237  cores  5240  resco  5241  imaco  5242  rnco  5243  coiun  5246  co02  5250  coi1  5252  coass  5255  relssdmrn  5257  unielrel  5264  ressn  5277  cnviinm  5278  cnvpom  5279  cnvsom  5280  uniabio  5297  iotaval  5298  iotass  5304  sniota  5317  csbiotag  5319  dffun2  5336  dffun7  5353  dffun8  5354  dffun9  5355  funopg  5360  funssres  5369  funun  5371  funcnvsn  5375  funinsn  5379  funcnv2  5390  funcnv  5391  funcnv3  5392  funcnveq  5393  fun2cnv  5394  funcnvuni  5399  imadif  5410  funimaexglem  5413  isarep1  5416  2elresin  5443  fnres  5449  fcnvres  5520  fconstg  5533  fun11iun  5604  f1osng  5626  dffv3g  5635  fvssunirng  5654  sefvex  5660  fv3  5662  fvres  5663  nfunsn  5676  funimass4  5696  ssimaexg  5708  dmfco  5714  fvopab6  5743  fndmdif  5752  fvelrn  5778  dffo4  5795  f1ompt  5798  fmptco  5813  fsn  5819  fsng  5820  fsn2g  5822  dfmpt  5825  dfmptg  5827  funopsn  5830  funop  5831  funopdmsn  5834  fnressn  5840  fressnfv  5841  fvsng  5850  resfunexg  5875  funfvima3  5888  idref  5897  abrexco  5900  imaiun  5901  dff13  5909  foeqcnvco  5931  f1eqcocnv  5932  fliftcnv  5936  isocnv2  5953  isoini  5959  isose  5962  riotav  5977  csbriotag  5985  acexmidlem2  6015  oprabid  6050  csbov123g  6057  0neqopab  6066  brabvv  6067  dfoprab2  6068  rnoprab  6104  eloprabga  6108  mpov  6111  f1opw  6230  opabex3d  6283  opabex3  6284  ofmres  6298  uchoice  6300  op1stg  6313  op2ndg  6314  1stval2  6318  2ndval2  6319  fo1st  6320  fo2nd  6321  f1stres  6322  f2ndres  6323  fo1stresm  6324  fo2ndresm  6325  xp1st  6328  xp2nd  6329  releldm2  6348  reldm  6349  sbcopeq1a  6350  csbopeq1a  6351  dfoprab3  6354  opabn1stprc  6358  eloprabi  6361  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  mpoexxg  6375  fmpoco  6381  df1st2  6384  df2nd2  6385  1stconst  6386  2ndconst  6387  dfmpo  6388  fo2ndf  6392  f1o2ndf1  6393  xporderlem  6396  cnvoprab  6399  f1od2  6400  brtpos2  6417  reldmtpos  6419  dmtpos  6422  rntpos  6423  ovtposg  6425  dftpos3  6428  dftpos4  6429  tpostpos  6430  tpossym  6442  tfrlem3  6477  tfrlem5  6480  tfrlem8  6484  tfrlemisucfn  6490  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemibex  6495  tfrlemi14d  6499  tfrexlem  6500  tfr1onlem3  6504  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  tfrcl  6530  rdgtfr  6540  rdgruledefgg  6541  rdgivallem  6547  rdgon  6552  rdg0g  6554  frec0g  6563  frecabex  6564  frecabcl  6565  frectfr  6566  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  oafnex  6612  sucinc  6613  fnoa  6615  oaexg  6616  omfnex  6617  fnom  6618  omexg  6619  fnoei  6620  oeiexg  6621  oeiv  6624  oacl  6628  omcl  6629  oeicl  6630  oav2  6631  nnsucelsuc  6659  nnsucuniel  6663  ercnv  6723  iserd  6728  eqerlem  6733  eqer  6734  ecdmn0m  6746  erth  6748  qsss  6763  ecid  6767  ecidg  6768  qsid  6769  iinerm  6776  qsel  6781  erovlem  6796  ecopovsym  6800  ecopover  6802  th3qlem2  6807  mapprc  6821  fnmap  6824  fnpm  6825  mapdm0  6832  mapval2  6847  mapsn  6859  mapsncnv  6864  mapsnf1o2  6865  ixpconstg  6876  ixpprc  6888  ixpin  6892  ixpiinm  6893  ixpssmap2g  6896  ixpssmapg  6897  elixpsn  6904  ixpsnf1o  6905  bren  6917  brdomg  6919  domen  6922  domeng  6923  idssen  6950  domssr  6951  ener  6953  domtr  6959  ensn1g  6971  en1  6973  en1bg  6974  fundmen  6981  fundmeng  6982  mapsnen  6986  fiprc  6990  unen  6991  rex2dom  6996  en2m  6999  dom1o  7002  xpsnen  7005  xpsneng  7006  xpcomco  7010  xpcomeng  7012  xpassen  7014  xpdom2  7015  xpdom2g  7016  pw2f1odc  7021  xpf1o  7030  mapen  7032  mapxpen  7034  xpmapenlem  7035  ssenen  7037  phplem4  7041  phplem3g  7042  nneneq  7043  php5  7044  phpm  7052  findcard  7077  findcard2  7078  findcard2s  7079  isinfinf  7086  ac6sfi  7087  exmidpw  7100  exmidpweq  7101  exmidpw2en  7104  unfidisj  7114  fiintim  7123  xpfi  7124  fisseneq  7127  ssfirab  7129  snexxph  7149  fidcenumlemr  7154  sbthlemi10  7165  isbth  7166  ssfii  7173  fi0  7174  fiss  7176  cnvinfex  7217  eqinfti  7219  infvalti  7221  infglbti  7224  infmoti  7227  ordiso2  7234  djuf1olem  7252  djuss  7269  ctm  7308  ctssdccl  7310  ctssdclemr  7311  finomni  7339  exmidomni  7341  fodjuomnilemdc  7343  nninfwlpoimlemginf  7375  pm54.43  7395  pr2cv1  7400  exmidfodomrlemim  7412  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  acfun  7422  ccfunen  7483  cc2lem  7485  cc3  7487  acnccim  7491  indpi  7562  dfplpq2  7574  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nqnq0  7661  mulnnnq0  7670  nqprm  7762  nqprrnd  7763  nqprdisj  7764  nqprloc  7765  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  ltnqpr  7813  ltnqpri  7814  archpr  7863  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlem2  7880  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemopu  7919  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  cnm  8052  ltresr  8059  peano1nnnn  8072  peano2nnnn  8073  axcnre  8101  axpre-apti  8105  renfdisj  8239  dfinfre  9136  1nn  9154  peano2nn  9155  indstr  9827  cnref1o  9885  ioof  10206  fzpr  10312  frec2uzrand  10668  frec2uzf1od  10669  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  frecfzennn  10689  seqp1g  10729  seqclg  10735  seqf1og  10784  seqfeq4g  10794  ser3le  10800  hashinfom  11041  hashunlem  11068  hashun  11069  hashxp  11091  hashfacen  11101  zfz1isolem1  11105  zfz1iso  11106  fundm2domnop0  11110  wrdexb  11126  fnpfx  11259  cats1un  11303  wrdind  11304  wrd2ind  11305  shftfvalg  11380  ovshftex  11381  shftfibg  11382  shftfval  11383  shftfib  11385  shftfn  11386  2shfti  11393  shftvalg  11398  shftval4g  11399  maxabslemval  11770  fimaxre2  11789  xrmaxiflemval  11812  fclim  11856  climshft  11866  zsumdc  11947  fsum3  11950  fsum2dlemstep  11997  fsumcnv  12000  fisumcom2  12001  fisum0diag2  12010  fsumconst  12017  modfsummodlemstep  12020  fsumabs  12028  fsumrelem  12034  fsumiun  12040  ntrivcvgap  12111  fprod2dlemstep  12185  fprodcnv  12188  fprodcom2fi  12189  fprodmodd  12204  nninfct  12614  algrf  12619  qredeu  12671  isprm2  12691  prmind2  12694  4sqlemafi  12970  4sqlem12  12977  ennnfonelemex  13037  ennnfonelemrn  13042  exmidunben  13049  ctinfom  13051  ctinf  13053  qnnen  13054  enctlem  13055  ctiunctlemfo  13062  slotslfn  13110  setscomd  13125  restfn  13328  elrest  13331  ptex  13349  prdsex  13354  prdsvallem  13357  prdsval  13358  prdsbaslemss  13359  prdsbas  13361  imasex  13390  imasival  13391  imasbas  13392  imasplusg  13393  imasmulr  13394  imasaddfnlemg  13399  fnpr2ob  13425  ismgm  13442  plusffng  13450  fn0g  13460  fngsum  13473  gsumsplit1r  13483  gsumprval  13484  issgrp  13488  ismnddef  13503  gsumfzz  13580  gsumfzcl  13584  mulgnngsum  13716  subgintm  13787  releqgg  13809  eqgex  13810  eqgfval  13811  eqgval  13812  isghm  13832  fnmgp  13938  isrng  13950  isring  14016  ringn0  14076  opprrngbg  14094  opprsubgg  14100  opprunitd  14127  dfrhm2  14171  rhmex  14174  opprsubrngg  14228  subrngintm  14229  subrngpropd  14233  subrgpropd  14270  isdomn  14286  opprdomnbg  14291  scaffng  14326  rmodislmodlem  14367  rmodislmod  14368  lssex  14371  lsssn0  14387  lss1d  14400  lssintclm  14401  ellspsn  14434  rlmfn  14470  isridl  14521  blfn  14568  mopnset  14569  metuex  14572  znval  14653  znleval  14670  psrval  14683  fnpsr  14684  mplvalcoe  14707  fnmpl  14710  bastg  14788  distop  14812  topnex  14813  epttop  14817  tgrest  14896  resttopon  14898  restco  14901  cnrest2  14963  cnptopresti  14965  cnptoprest  14966  cnptoprest2  14967  txuni2  14983  txbas  14985  eltx  14986  txcnp  14998  txcnmpt  15000  txrest  15003  txdis1cn  15005  txlm  15006  cnmpt1st  15015  cnmpt2nd  15016  txhmeo  15046  txswaphmeolem  15047  xmetec  15164  metrest  15233  reldvg  15406  dvfgg  15415  dvcj  15436  dvmptfsum  15452  elply2  15462  pilem3  15510  lgsquadlem1  15809  lgsquadlem2  15810  upgrex  15957  upgr1een  15978  umgredg  15999  umgredgnlp  16006  usgredgreu  16070  uspgredg2vtxeu  16072  ushgredgedg  16080  ushgredgedgloop  16082  griedg0ssusgr  16105  uhgrspansubgrlem  16130  upgrspanop  16137  umgrspanop  16138  usgrspanop  16139  wlkvtxiedg  16199  wlkvtxiedgg  16200  wlk1walkdom  16213  depindlem1  16346  bdcvv  16473  bdsnss  16489  bdop  16491  bj-vprc  16512  bdinex1g  16517  bdssexg  16520  bj-inex  16523  bj-zfpair2  16526  bj-uniexg  16534  bdunexb  16536  bj-unexg  16537  bj-indint  16547  bj-ssom  16552  bj-om  16553  bj-2inf  16554  bj-bdfindis  16563  bj-nn0suc0  16566  bj-nnelirr  16569  bj-inf2vnlem1  16586  bj-inf2vnlem2  16587  bj-omex2  16593  bj-nn0sucALT  16594  bj-findis  16595  ss1oel2o  16607  domomsubct  16623  pw1nct  16625  nninfsellemeq  16637  exmidsbthrlem  16647  gfsumval  16701