Theorem vex 2782

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

Syntax hints:   ∈ wcel 2180  Vcvv 2779

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-v 2781

This theorem is referenced by:  elv  2783  elvd  2784  el2v  2785  isset  2786  eqvisset  2790  ralv  2797  rexv  2798  reuv  2799  rmov  2800  rabab  2801  sbhypf  2830  ceqex  2910  ralab  2943  rexab  2945  mo2icl  2962  reu8  2979  csbvarg  3132  csbiebg  3147  sbcnestgf  3156  sbnfc2  3165  ddifnel  3315  ddifstab  3316  csbing  3391  unssdif  3419  unssin  3423  inssun  3424  invdif  3426  vn0  3482  vn0m  3483  eqv  3491  abvor0dc  3495  sbss  3579  velpw  3636  elpwg  3637  velsn  3663  vsnid  3678  exsnrex  3688  dftp2  3695  prmg  3768  prnzg  3771  snssgOLD  3783  difprsnss  3785  sneqrg  3819  preq12bg  3830  pwprss  3863  pwtpss  3864  pwv  3866  unipr  3881  uniprg  3882  unisng  3884  elintg  3910  elintrabg  3915  intss1  3917  ssint  3918  intmin  3922  intss  3923  intssunim  3924  intmin4  3930  intab  3931  intun  3933  intpr  3934  intprg  3935  uniintsnr  3938  iinconstm  3953  iuniin  3954  iinss1  3956  dfiin2g  3977  dfiunv2  3980  ssiinf  3994  iinss  3996  iinss2  3997  0iin  4003  iinab  4006  iundif2ss  4010  iindif2m  4012  iinin2m  4013  iinuniss  4027  sspwuni  4029  pwpwab  4032  iinpw  4035  iunpwss  4036  brab1  4110  csbopabg  4141  mptv  4160  trint  4176  vnex  4194  inex1g  4199  ssexg  4202  inteximm  4212  inuni  4218  repizf2  4225  axpweq  4234  bnd2  4236  pwuni  4255  exmidundif  4269  exmidundifim  4270  zfpair2  4273  rext  4280  sspwb  4281  unipw  4282  ssextss  4285  euabex  4290  mss  4291  exss  4292  opth  4302  opthg  4303  copsexg  4309  copsex4g  4312  moop2  4317  euotd  4320  opabid  4323  elopab  4325  opelopabsbALT  4326  opelopabsb  4327  opabm  4348  pwin  4350  pwunss  4351  epelg  4358  epel  4360  pofun  4380  epse  4410  tron  4450  sucel  4478  suctr  4489  vuniex  4506  uniexg  4507  unexb  4510  snnex  4516  pwnex  4517  uniuni  4519  eusvnf  4521  eusvnfb  4522  iunpw  4548  unon  4580  ordunisuc2r  4583  ordtri2or2exmidlem  4595  onsucelsucexmidlem  4598  ordsucunielexmid  4600  elirr  4610  en2lp  4623  dtruex  4628  onintexmid  4642  reg3exmidlemwe  4648  dcextest  4650  finds  4669  finds2  4670  elomssom  4674  limom  4683  0nelxp  4724  opelxp  4726  opeliunxp  4751  elvv  4758  elvvv  4759  elvvuni  4760  xpsspw  4808  relopabiv  4822  relopabi  4824  opabid2  4830  difopab  4832  xpiindim  4836  raliunxp  4840  rexiunxp  4841  ralxpf  4845  rexxpf  4846  relop  4849  cnvco  4884  dfrn2  4887  dfdm4  4892  dmss  4899  dmin  4908  dmiun  4909  dmuni  4910  dm0  4914  dmi  4915  reldm0  4918  elreldm  4926  elrnmpt1  4951  dmrnssfld  4963  dmcoss  4970  dmcosseq  4972  opelresg  4988  resieq  4991  dmres  5002  elres  5017  relssres  5019  resopab  5025  resiexg  5026  iss  5027  dfres2  5033  restidsing  5037  dfima2  5046  imadmrn  5054  imai  5060  csbima12g  5065  elimasng  5072  args  5073  epini  5075  iniseg  5076  dfse2  5077  exse2  5078  cotr  5086  issref  5087  cnvsym  5088  intasym  5089  asymref  5090  intirr  5091  brcodir  5092  codir  5093  qfto  5094  poirr2  5097  cnvopab  5106  cnv0  5108  cnvi  5109  cnvdif  5111  rniun  5115  dminss  5119  imainss  5120  inimasn  5122  xpmlem  5125  dmxpss  5135  rnxpid  5139  ssrnres  5147  rninxp  5148  dminxp  5149  cnvcnv3  5154  dfrel2  5155  dmsnm  5170  dmsnopg  5176  cnvcnvsn  5181  dmsnsnsng  5182  cnvsng  5190  elxp4  5192  elxp5  5193  cnvresima  5194  dfco2  5204  dfco2a  5205  cores  5208  resco  5209  imaco  5210  rnco  5211  coiun  5214  co02  5218  coi1  5220  coass  5223  relssdmrn  5225  unielrel  5232  ressn  5245  cnviinm  5246  cnvpom  5247  cnvsom  5248  uniabio  5265  iotaval  5266  iotass  5272  sniota  5285  csbiotag  5287  dffun2  5304  dffun7  5321  dffun8  5322  dffun9  5323  funopg  5328  funssres  5336  funun  5338  funcnvsn  5342  funinsn  5346  funcnv2  5357  funcnv  5358  funcnv3  5359  funcnveq  5360  fun2cnv  5361  funcnvuni  5366  imadif  5377  funimaexglem  5380  isarep1  5383  2elresin  5410  fnres  5416  fcnvres  5485  fconstg  5498  fun11iun  5569  f1osng  5590  dffv3g  5599  fvssunirng  5618  sefvex  5624  fv3  5626  fvres  5627  nfunsn  5638  funimass4  5657  ssimaexg  5669  dmfco  5675  fvopab6  5704  fndmdif  5713  fvelrn  5739  dffo4  5756  f1ompt  5759  fmptco  5774  fsn  5780  fsng  5781  dfmpt  5785  dfmptg  5787  funopsn  5790  funop  5791  funopdmsn  5792  fnressn  5798  fressnfv  5799  fvsng  5808  resfunexg  5833  funfvima3  5846  idref  5853  abrexco  5856  imaiun  5857  dff13  5865  foeqcnvco  5887  f1eqcocnv  5888  fliftcnv  5892  isocnv2  5909  isoini  5915  isose  5918  riotav  5933  csbriotag  5941  acexmidlem2  5971  oprabid  6006  csbov123g  6013  0neqopab  6020  brabvv  6021  dfoprab2  6022  rnoprab  6058  eloprabga  6062  mpov  6065  f1opw  6183  opabex3d  6236  opabex3  6237  ofmres  6251  uchoice  6253  op1stg  6266  op2ndg  6267  1stval2  6271  2ndval2  6272  fo1st  6273  fo2nd  6274  f1stres  6275  f2ndres  6276  fo1stresm  6277  fo2ndresm  6278  xp1st  6281  xp2nd  6282  releldm2  6301  reldm  6302  sbcopeq1a  6303  csbopeq1a  6304  dfoprab3  6307  eloprabi  6312  mpomptsx  6313  dmmpossx  6315  fmpox  6316  mpofvex  6321  mpoexxg  6326  fmpoco  6332  df1st2  6335  df2nd2  6336  1stconst  6337  2ndconst  6338  dfmpo  6339  fo2ndf  6343  f1o2ndf1  6344  xporderlem  6347  cnvoprab  6350  f1od2  6351  brtpos2  6367  reldmtpos  6369  dmtpos  6372  rntpos  6373  ovtposg  6375  dftpos3  6378  dftpos4  6379  tpostpos  6380  tpossym  6392  tfrlem3  6427  tfrlem5  6430  tfrlem8  6434  tfrlemisucfn  6440  tfrlemisucaccv  6441  tfrlemibxssdm  6443  tfrlemibfn  6444  tfrlemibex  6445  tfrlemi14d  6449  tfrexlem  6450  tfr1onlem3  6454  tfr1onlemsucaccv  6457  tfr1onlembxssdm  6459  tfr1onlembfn  6460  tfr1onlemres  6465  tfri1dALT  6467  tfrcllemsucaccv  6470  tfrcllembxssdm  6472  tfrcllembfn  6473  tfrcllemres  6478  tfrcl  6480  rdgtfr  6490  rdgruledefgg  6491  rdgivallem  6497  rdgon  6502  rdg0g  6504  frec0g  6513  frecabex  6514  frecabcl  6515  frectfr  6516  freccllem  6518  frecfcllem  6520  frecsuclem  6522  frecrdg  6524  oafnex  6560  sucinc  6561  fnoa  6563  oaexg  6564  omfnex  6565  fnom  6566  omexg  6567  fnoei  6568  oeiexg  6569  oeiv  6572  oacl  6576  omcl  6577  oeicl  6578  oav2  6579  nnsucelsuc  6607  nnsucuniel  6611  ercnv  6671  iserd  6676  eqerlem  6681  eqer  6682  ecdmn0m  6694  erth  6696  qsss  6711  ecid  6715  ecidg  6716  qsid  6717  iinerm  6724  qsel  6729  erovlem  6744  ecopovsym  6748  ecopover  6750  th3qlem2  6755  mapprc  6769  fnmap  6772  fnpm  6773  mapdm0  6780  mapval2  6795  mapsn  6807  mapsncnv  6812  mapsnf1o2  6813  ixpconstg  6824  ixpprc  6836  ixpin  6840  ixpiinm  6841  ixpssmap2g  6844  ixpssmapg  6845  elixpsn  6852  ixpsnf1o  6853  bren  6865  brdomg  6867  domen  6870  domeng  6871  idssen  6898  domssr  6899  ener  6901  domtr  6907  ensn1g  6919  en1  6921  en1bg  6922  fundmen  6929  fundmeng  6930  mapsnen  6934  fiprc  6938  unen  6939  rex2dom  6941  en2m  6944  xpsnen  6948  xpsneng  6949  xpcomco  6953  xpcomeng  6955  xpassen  6957  xpdom2  6958  xpdom2g  6959  pw2f1odc  6964  xpf1o  6973  mapen  6975  mapxpen  6977  xpmapenlem  6978  ssenen  6980  phplem4  6984  phplem3g  6985  nneneq  6986  php5  6987  phpm  6995  findcard  7018  findcard2  7019  findcard2s  7020  isinfinf  7027  ac6sfi  7028  exmidpw  7038  exmidpweq  7039  exmidpw2en  7042  unfidisj  7052  fiintim  7061  xpfi  7062  fisseneq  7064  ssfirab  7066  snexxph  7085  fidcenumlemr  7090  sbthlemi10  7101  isbth  7102  ssfii  7109  fi0  7110  fiss  7112  cnvinfex  7153  eqinfti  7155  infvalti  7157  infglbti  7160  infmoti  7163  ordiso2  7170  djuf1olem  7188  djuss  7205  ctm  7244  ctssdccl  7246  ctssdclemr  7247  finomni  7275  exmidomni  7277  fodjuomnilemdc  7279  nninfwlpoimlemginf  7311  pm54.43  7331  pr2cv1  7336  exmidfodomrlemim  7347  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  finacn  7354  acfun  7357  ccfunen  7418  cc2lem  7420  cc3  7422  acnccim  7426  indpi  7497  dfplpq2  7509  enq0sym  7587  enq0ref  7588  enq0tr  7589  nqnq0pi  7593  nqnq0  7596  mulnnnq0  7605  nqprm  7697  nqprrnd  7698  nqprdisj  7699  nqprloc  7700  nqprl  7706  nqpru  7707  addnqprlemrl  7712  addnqprlemru  7713  addnqprlemfl  7714  addnqprlemfu  7715  mulnqprlemrl  7728  mulnqprlemru  7729  mulnqprlemfl  7730  mulnqprlemfu  7731  ltnqpr  7748  ltnqpri  7749  archpr  7798  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  cauappcvgprlem2  7815  caucvgprlemladdfu  7832  caucvgprlem2  7835  caucvgprprlemopu  7854  suplocexprlemmu  7873  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  cnm  7987  ltresr  7994  peano1nnnn  8007  peano2nnnn  8008  axcnre  8036  axpre-apti  8040  renfdisj  8174  dfinfre  9071  1nn  9089  peano2nn  9090  indstr  9756  cnref1o  9814  ioof  10135  fzpr  10241  frec2uzrand  10594  frec2uzf1od  10595  frecuzrdgtcl  10601  frecuzrdgfunlem  10608  frecfzennn  10615  seqp1g  10655  seqclg  10661  seqf1og  10710  seqfeq4g  10720  ser3le  10726  hashinfom  10967  hashunlem  10993  hashun  10994  hashxp  11015  hashfacen  11025  zfz1isolem1  11029  zfz1iso  11030  fundm2domnop0  11034  wrdexb  11050  fnpfx  11175  cats1un  11219  wrdind  11220  wrd2ind  11221  shftfvalg  11295  ovshftex  11296  shftfibg  11297  shftfval  11298  shftfib  11300  shftfn  11301  2shfti  11308  shftvalg  11313  shftval4g  11314  maxabslemval  11685  fimaxre2  11704  xrmaxiflemval  11727  fclim  11771  climshft  11781  zsumdc  11861  fsum3  11864  fsum2dlemstep  11911  fsumcnv  11914  fisumcom2  11915  fisum0diag2  11924  fsumconst  11931  modfsummodlemstep  11934  fsumabs  11942  fsumrelem  11948  fsumiun  11954  ntrivcvgap  12025  fprod2dlemstep  12099  fprodcnv  12102  fprodcom2fi  12103  fprodmodd  12118  nninfct  12528  algrf  12533  qredeu  12585  isprm2  12605  prmind2  12608  4sqlemafi  12884  4sqlem12  12891  ennnfonelemex  12951  ennnfonelemrn  12956  exmidunben  12963  ctinfom  12965  ctinf  12967  qnnen  12968  enctlem  12969  ctiunctlemfo  12976  slotslfn  13024  setscomd  13039  restfn  13242  elrest  13245  ptex  13263  prdsex  13268  prdsvallem  13271  prdsval  13272  prdsbaslemss  13273  prdsbas  13275  imasex  13304  imasival  13305  imasbas  13306  imasplusg  13307  imasmulr  13308  imasaddfnlemg  13313  fnpr2ob  13339  ismgm  13356  plusffng  13364  fn0g  13374  fngsum  13387  gsumsplit1r  13397  gsumprval  13398  issgrp  13402  ismnddef  13417  gsumfzz  13494  gsumfzcl  13498  mulgnngsum  13630  subgintm  13701  releqgg  13723  eqgex  13724  eqgfval  13725  eqgval  13726  isghm  13746  fnmgp  13851  isrng  13863  isring  13929  ringn0  13989  opprrngbg  14007  opprsubgg  14013  opprunitd  14039  dfrhm2  14083  rhmex  14086  opprsubrngg  14140  subrngintm  14141  subrngpropd  14145  subrgpropd  14182  isdomn  14198  opprdomnbg  14203  scaffng  14238  rmodislmodlem  14279  rmodislmod  14280  lssex  14283  lsssn0  14299  lss1d  14312  lssintclm  14313  ellspsn  14346  rlmfn  14382  isridl  14433  blfn  14480  mopnset  14481  metuex  14484  znval  14565  znleval  14582  psrval  14595  fnpsr  14596  mplvalcoe  14619  fnmpl  14622  bastg  14700  distop  14724  topnex  14725  epttop  14729  tgrest  14808  resttopon  14810  restco  14813  cnrest2  14875  cnptopresti  14877  cnptoprest  14878  cnptoprest2  14879  txuni2  14895  txbas  14897  eltx  14898  txcnp  14910  txcnmpt  14912  txrest  14915  txdis1cn  14917  txlm  14918  cnmpt1st  14927  cnmpt2nd  14928  txhmeo  14958  txswaphmeolem  14959  xmetec  15076  metrest  15145  reldvg  15318  dvfgg  15327  dvcj  15348  dvmptfsum  15364  elply2  15374  pilem3  15422  lgsquadlem1  15721  lgsquadlem2  15722  upgrex  15868  umgredg  15908  umgredgnlp  15915  usgredgreu  15979  uspgredg2vtxeu  15981  ushgredgedg  15989  ushgredgedgloop  15991  bdcvv  16130  bdsnss  16146  bdop  16148  bj-vprc  16169  bdinex1g  16174  bdssexg  16177  bj-inex  16180  bj-zfpair2  16183  bj-uniexg  16191  bdunexb  16193  bj-unexg  16194  bj-indint  16204  bj-ssom  16209  bj-om  16210  bj-2inf  16211  bj-bdfindis  16220  bj-nn0suc0  16223  bj-nnelirr  16226  bj-inf2vnlem1  16243  bj-inf2vnlem2  16244  bj-omex2  16250  bj-nn0sucALT  16251  bj-findis  16252  ss1oel2o  16265  dom1o  16266  domomsubct  16278  pw1nct  16280  nninfsellemeq  16291  exmidsbthrlem  16301