Theorem vex 2755

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

Syntax hints:   ∈ wcel 2160  Vcvv 2752

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  elv  2756  elvd  2757  isset  2758  eqvisset  2762  ralv  2769  rexv  2770  reuv  2771  rmov  2772  rabab  2773  sbhypf  2801  ceqex  2879  ralab  2912  rexab  2914  mo2icl  2931  reu8  2948  csbvarg  3100  csbiebg  3114  sbcnestgf  3123  sbnfc2  3132  ddifnel  3281  ddifstab  3282  csbing  3357  unssdif  3385  unssin  3389  inssun  3390  invdif  3392  vn0  3448  vn0m  3449  eqv  3457  abvor0dc  3461  sbss  3546  velpw  3597  elpwg  3598  velsn  3624  vsnid  3639  exsnrex  3649  dftp2  3656  prmg  3728  prnzg  3731  snssgOLD  3743  difprsnss  3745  sneqrg  3777  preq12bg  3788  pwprss  3820  pwtpss  3821  pwv  3823  unipr  3838  uniprg  3839  unisng  3841  elintg  3867  elintrabg  3872  intss1  3874  ssint  3875  intmin  3879  intss  3880  intssunim  3881  intmin4  3887  intab  3888  intun  3890  intpr  3891  intprg  3892  uniintsnr  3895  iinconstm  3910  iuniin  3911  iinss1  3913  dfiin2g  3934  dfiunv2  3937  ssiinf  3951  iinss  3953  iinss2  3954  0iin  3960  iinab  3963  iundif2ss  3967  iindif2m  3969  iinin2m  3970  iinuniss  3984  sspwuni  3986  pwpwab  3989  iinpw  3992  iunpwss  3993  brab1  4065  csbopabg  4096  mptv  4115  trint  4131  vnex  4149  inex1g  4154  ssexg  4157  inteximm  4167  inuni  4173  repizf2  4180  axpweq  4189  bnd2  4191  pwuni  4210  exmidundif  4224  exmidundifim  4225  zfpair2  4228  rext  4233  sspwb  4234  unipw  4235  ssextss  4238  euabex  4243  mss  4244  exss  4245  opth  4255  opthg  4256  copsexg  4262  copsex4g  4265  moop2  4269  euotd  4272  opabid  4275  elopab  4276  opelopabsbALT  4277  opelopabsb  4278  opabm  4298  pwin  4300  pwunss  4301  epelg  4308  epel  4310  pofun  4330  epse  4360  tron  4400  sucel  4428  suctr  4439  vuniex  4456  uniexg  4457  unexb  4460  snnex  4466  pwnex  4467  uniuni  4469  eusvnf  4471  eusvnfb  4472  iunpw  4498  unon  4528  ordunisuc2r  4531  ordtri2or2exmidlem  4543  onsucelsucexmidlem  4546  ordsucunielexmid  4548  elirr  4558  en2lp  4571  dtruex  4576  onintexmid  4590  reg3exmidlemwe  4596  dcextest  4598  finds  4617  finds2  4618  elomssom  4622  limom  4631  0nelxp  4672  opelxp  4674  opeliunxp  4699  elvv  4706  elvvv  4707  elvvuni  4708  xpsspw  4756  relopabi  4770  opabid2  4776  difopab  4778  xpiindim  4782  raliunxp  4786  rexiunxp  4787  ralxpf  4791  rexxpf  4792  relop  4795  cnvco  4830  dfrn2  4833  dfdm4  4837  dmss  4844  dmin  4853  dmiun  4854  dmuni  4855  dm0  4859  dmi  4860  reldm0  4863  elreldm  4871  elrnmpt1  4896  dmrnssfld  4908  dmcoss  4914  dmcosseq  4916  opelresg  4932  resieq  4935  dmres  4946  elres  4961  relssres  4963  resopab  4969  resiexg  4970  iss  4971  dfres2  4977  restidsing  4981  dfima2  4990  imadmrn  4998  imai  5002  csbima12g  5007  elimasng  5014  args  5015  epini  5017  iniseg  5018  dfse2  5019  exse2  5020  cotr  5028  issref  5029  cnvsym  5030  intasym  5031  asymref  5032  intirr  5033  brcodir  5034  codir  5035  qfto  5036  poirr2  5039  cnvopab  5048  cnv0  5050  cnvi  5051  cnvdif  5053  rniun  5057  dminss  5061  imainss  5062  inimasn  5064  xpmlem  5067  dmxpss  5077  rnxpid  5081  ssrnres  5089  rninxp  5090  dminxp  5091  cnvcnv3  5096  dfrel2  5097  dmsnm  5112  dmsnopg  5118  cnvcnvsn  5123  dmsnsnsng  5124  cnvsng  5132  elxp4  5134  elxp5  5135  cnvresima  5136  dfco2  5146  dfco2a  5147  cores  5150  resco  5151  imaco  5152  rnco  5153  coiun  5156  co02  5160  coi1  5162  coass  5165  relssdmrn  5167  unielrel  5174  ressn  5187  cnviinm  5188  cnvpom  5189  cnvsom  5190  uniabio  5206  iotaval  5207  iotass  5213  sniota  5226  csbiotag  5228  dffun2  5245  dffun7  5262  dffun8  5263  dffun9  5264  funopg  5269  funssres  5277  funun  5279  funcnvsn  5280  funinsn  5284  funcnv2  5295  funcnv  5296  funcnv3  5297  funcnveq  5298  fun2cnv  5299  funcnvuni  5304  imadif  5315  funimaexglem  5318  isarep1  5321  2elresin  5346  fnres  5351  fcnvres  5418  fconstg  5431  fun11iun  5501  f1osng  5521  dffv3g  5530  fvssunirng  5549  sefvex  5555  fv3  5557  fvres  5558  nfunsn  5569  funimass4  5587  ssimaexg  5599  dmfco  5605  fvopab6  5633  fndmdif  5642  fvelrn  5668  dffo4  5685  f1ompt  5688  fmptco  5703  fsn  5709  fsng  5710  dfmpt  5714  dfmptg  5716  fnressn  5723  fressnfv  5724  fvsng  5733  resfunexg  5758  funfvima3  5771  idref  5778  abrexco  5781  imaiun  5782  dff13  5790  foeqcnvco  5812  f1eqcocnv  5813  fliftcnv  5817  isocnv2  5834  isoini  5840  isose  5843  riotav  5858  csbriotag  5865  acexmidlem2  5894  oprabid  5929  csbov123g  5935  0neqopab  5942  brabvv  5943  dfoprab2  5944  rnoprab  5980  eloprabga  5984  mpov  5987  f1opw  6102  opabex3d  6147  opabex3  6148  ofmres  6162  op1stg  6176  op2ndg  6177  1stval2  6181  2ndval2  6182  fo1st  6183  fo2nd  6184  f1stres  6185  f2ndres  6186  fo1stresm  6187  fo2ndresm  6188  xp1st  6191  xp2nd  6192  releldm2  6211  reldm  6212  sbcopeq1a  6213  csbopeq1a  6214  dfoprab3  6217  eloprabi  6222  mpomptsx  6223  dmmpossx  6225  fmpox  6226  mpofvex  6229  mpoexxg  6236  fmpoco  6242  df1st2  6245  df2nd2  6246  1stconst  6247  2ndconst  6248  dfmpo  6249  fo2ndf  6253  f1o2ndf1  6254  xporderlem  6257  cnvoprab  6260  f1od2  6261  brtpos2  6277  reldmtpos  6279  dmtpos  6282  rntpos  6283  ovtposg  6285  dftpos3  6288  dftpos4  6289  tpostpos  6290  tpossym  6302  tfrlem3  6337  tfrlem5  6340  tfrlem8  6344  tfrlemisucfn  6350  tfrlemisucaccv  6351  tfrlemibxssdm  6353  tfrlemibfn  6354  tfrlemibex  6355  tfrlemi14d  6359  tfrexlem  6360  tfr1onlem3  6364  tfr1onlemsucaccv  6367  tfr1onlembxssdm  6369  tfr1onlembfn  6370  tfr1onlemres  6375  tfri1dALT  6377  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllembfn  6383  tfrcllemres  6388  tfrcl  6390  rdgtfr  6400  rdgruledefgg  6401  rdgivallem  6407  rdgon  6412  rdg0g  6414  frec0g  6423  frecabex  6424  frecabcl  6425  frectfr  6426  freccllem  6428  frecfcllem  6430  frecsuclem  6432  frecrdg  6434  oafnex  6470  sucinc  6471  fnoa  6473  oaexg  6474  omfnex  6475  fnom  6476  omexg  6477  fnoei  6478  oeiexg  6479  oeiv  6482  oacl  6486  omcl  6487  oeicl  6488  oav2  6489  nnsucelsuc  6517  nnsucuniel  6521  ercnv  6581  iserd  6586  eqerlem  6591  eqer  6592  ecdmn0m  6604  erth  6606  qsss  6621  ecid  6625  ecidg  6626  qsid  6627  iinerm  6634  qsel  6639  erovlem  6654  ecopovsym  6658  ecopover  6660  th3qlem2  6665  mapprc  6679  fnmap  6682  fnpm  6683  mapdm0  6690  mapval2  6705  mapsn  6717  mapsncnv  6722  mapsnf1o2  6723  ixpconstg  6734  ixpprc  6746  ixpin  6750  ixpiinm  6751  ixpssmap2g  6754  ixpssmapg  6755  elixpsn  6762  ixpsnf1o  6763  bren  6774  brdomg  6775  domen  6778  domeng  6779  idssen  6804  ener  6806  domtr  6812  ensn1g  6824  en1  6826  en1bg  6827  fundmen  6833  fundmeng  6834  mapsnen  6838  fiprc  6842  unen  6843  xpsnen  6848  xpsneng  6849  xpcomco  6853  xpcomeng  6855  xpassen  6857  xpdom2  6858  xpdom2g  6859  pw2f1odc  6864  xpf1o  6873  mapen  6875  mapxpen  6877  xpmapenlem  6878  ssenen  6880  phplem4  6884  phplem3g  6885  nneneq  6886  php5  6887  phpm  6894  findcard  6917  findcard2  6918  findcard2s  6919  isinfinf  6926  ac6sfi  6927  exmidpw  6937  exmidpweq  6938  exmidpw2en  6941  unfidisj  6951  fiintim  6958  xpfi  6959  fisseneq  6961  ssfirab  6963  snexxph  6980  fidcenumlemr  6985  sbthlemi10  6996  isbth  6997  ssfii  7004  fi0  7005  fiss  7007  cnvinfex  7048  eqinfti  7050  infvalti  7052  infglbti  7055  infmoti  7058  ordiso2  7065  djuf1olem  7083  djuss  7100  ctm  7139  ctssdccl  7141  ctssdclemr  7142  finomni  7169  exmidomni  7171  fodjuomnilemdc  7173  nninfwlpoimlemginf  7205  pm54.43  7220  exmidfodomrlemim  7231  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  acfun  7237  ccfunen  7294  cc2lem  7296  cc3  7298  indpi  7372  dfplpq2  7384  enq0sym  7462  enq0ref  7463  enq0tr  7464  nqnq0pi  7468  nqnq0  7471  mulnnnq0  7480  nqprm  7572  nqprrnd  7573  nqprdisj  7574  nqprloc  7575  nqprl  7581  nqpru  7582  addnqprlemrl  7587  addnqprlemru  7588  addnqprlemfl  7589  addnqprlemfu  7590  mulnqprlemrl  7603  mulnqprlemru  7604  mulnqprlemfl  7605  mulnqprlemfu  7606  ltnqpr  7623  ltnqpri  7624  archpr  7673  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  cauappcvgprlem2  7690  caucvgprlemladdfu  7707  caucvgprlem2  7710  caucvgprprlemopu  7729  suplocexprlemmu  7748  suplocexprlemdisj  7750  suplocexprlemloc  7751  suplocexprlemub  7753  cnm  7862  ltresr  7869  peano1nnnn  7882  peano2nnnn  7883  axcnre  7911  axpre-apti  7915  renfdisj  8048  dfinfre  8944  1nn  8961  peano2nn  8962  indstr  9625  cnref1o  9682  ioof  10003  fzpr  10109  frec2uzrand  10438  frec2uzf1od  10439  frecuzrdgtcl  10445  frecuzrdgfunlem  10452  frecfzennn  10459  seqfeq4g  10546  ser3le  10552  hashinfom  10793  hashunlem  10819  hashun  10820  hashxp  10841  hashfacen  10851  zfz1isolem1  10855  zfz1iso  10856  shftfvalg  10862  ovshftex  10863  shftfibg  10864  shftfval  10865  shftfib  10867  shftfn  10868  2shfti  10875  shftvalg  10880  shftval4g  10881  maxabslemval  11252  fimaxre2  11270  xrmaxiflemval  11293  fclim  11337  climshft  11347  zsumdc  11427  fsum3  11430  fsum2dlemstep  11477  fsumcnv  11480  fisumcom2  11481  fisum0diag2  11490  fsumconst  11497  modfsummodlemstep  11500  fsumabs  11508  fsumrelem  11514  fsumiun  11520  ntrivcvgap  11591  fprod2dlemstep  11665  fprodcnv  11668  fprodcom2fi  11669  fprodmodd  11684  algrf  12080  qredeu  12132  isprm2  12152  prmind2  12155  4sqlemafi  12430  4sqlem12  12437  ennnfonelemex  12468  ennnfonelemrn  12473  exmidunben  12480  ctinfom  12482  ctinf  12484  qnnen  12485  enctlem  12486  ctiunctlemfo  12493  slotslfn  12541  setscomd  12556  restfn  12751  elrest  12754  ptex  12772  prdsex  12777  imasex  12785  imasival  12786  imasbas  12787  imasplusg  12788  imasmulr  12789  imasaddfnlemg  12794  fnpr2ob  12819  ismgm  12836  plusffng  12844  fn0g  12854  fngsum  12867  gsumsplit1r  12876  gsumprval  12877  issgrp  12881  ismnddef  12894  mulgnngsum  13084  subgintm  13154  releqgg  13176  eqgex  13177  eqgfval  13178  eqgval  13179  isghm  13199  fnmgp  13293  isrng  13305  isring  13371  ringn0  13429  opprrngbg  13445  opprsubgg  13451  opprunitd  13477  dfrhm2  13521  rhmex  13524  opprsubrngg  13575  subrngintm  13576  subrngpropd  13580  subrgpropd  13612  scaffng  13642  rmodislmodlem  13683  rmodislmod  13684  lssex  13687  lsssn0  13703  lss1d  13716  lssintclm  13717  lspsnel  13750  rlmfn  13786  isridl  13836  znval  13949  psrval  13961  fnpsr  13962  bastg  14038  distop  14062  topnex  14063  epttop  14067  tgrest  14146  resttopon  14148  restco  14151  cnrest2  14213  cnptopresti  14215  cnptoprest  14216  cnptoprest2  14217  txuni2  14233  txbas  14235  eltx  14236  txcnp  14248  txcnmpt  14250  txrest  14253  txdis1cn  14255  txlm  14256  cnmpt1st  14265  cnmpt2nd  14266  txhmeo  14296  txswaphmeolem  14297  xmetec  14414  metrest  14483  reldvg  14625  dvfgg  14634  dvcj  14650  pilem3  14681  bdcvv  15087  bdsnss  15103  bdop  15105  bj-vprc  15126  bdinex1g  15131  bdssexg  15134  bj-inex  15137  bj-zfpair2  15140  bj-uniexg  15148  bdunexb  15150  bj-unexg  15151  bj-indint  15161  bj-ssom  15166  bj-om  15167  bj-2inf  15168  bj-bdfindis  15177  bj-nn0suc0  15180  bj-nnelirr  15183  bj-inf2vnlem1  15200  bj-inf2vnlem2  15201  bj-omex2  15207  bj-nn0sucALT  15208  bj-findis  15209  ss1oel2o  15222  pw1nct  15231  nninfsellemeq  15242  exmidsbthrlem  15249