ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  vex GIF version

Theorem vex 2689
Description: All setvar variables are sets (see isset 2692). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
vex 𝑥 ∈ V

Proof of Theorem vex
StepHypRef Expression
1 equid 1677 . 2 𝑥 = 𝑥
2 df-v 2688 . . 3 V = {𝑥𝑥 = 𝑥}
32abeq2i 2250 . 2 (𝑥 ∈ V ↔ 𝑥 = 𝑥)
41, 3mpbir 145 1 𝑥 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1480  Vcvv 2686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688
This theorem is referenced by:  elv  2690  elvd  2691  isset  2692  eqvisset  2696  ralv  2703  rexv  2704  reuv  2705  rmov  2706  rabab  2707  sbhypf  2735  ceqex  2812  ralab  2844  rexab  2846  mo2icl  2863  reu8  2880  csbvarg  3030  csbiebg  3042  sbcnestgf  3051  sbnfc2  3060  ddifnel  3207  ddifstab  3208  csbing  3283  unssdif  3311  unssin  3315  inssun  3316  invdif  3318  vn0  3373  vn0m  3374  eqv  3382  abvor0dc  3386  sbss  3471  velpw  3517  elpwg  3518  velsn  3544  vsnid  3557  exsnrex  3566  dftp2  3572  prmg  3644  prnzg  3647  snssg  3656  difprsnss  3658  sneqrg  3689  preq12bg  3700  pwprss  3732  pwtpss  3733  pwv  3735  unipr  3750  uniprg  3751  unisng  3753  elintg  3779  elintrabg  3784  intss1  3786  ssint  3787  intmin  3791  intss  3792  intssunim  3793  intmin4  3799  intab  3800  intun  3802  intpr  3803  intprg  3804  uniintsnr  3807  iinconstm  3822  iuniin  3823  iinss1  3825  dfiin2g  3846  dfiunv2  3849  ssiinf  3862  iinss  3864  iinss2  3865  0iin  3871  iinab  3874  iundif2ss  3878  iindif2m  3880  iinin2m  3881  iinuniss  3895  sspwuni  3897  pwpwab  3900  iinpw  3903  iunpwss  3904  brab1  3975  csbopabg  4006  mptv  4025  trint  4041  vnex  4059  inex1g  4064  ssexg  4067  inteximm  4074  inuni  4080  repizf2  4086  axpweq  4095  bnd2  4097  pwuni  4116  exmidundif  4129  exmidundifim  4130  zfpair2  4132  rext  4137  sspwb  4138  unipw  4139  ssextss  4142  euabex  4147  mss  4148  exss  4149  opth  4159  opthg  4160  copsexg  4166  copsex4g  4169  moop2  4173  euotd  4176  opabid  4179  elopab  4180  opelopabsbALT  4181  opelopabsb  4182  opabm  4202  pwin  4204  pwunss  4205  epelg  4212  epel  4214  pofun  4234  epse  4264  tron  4304  sucel  4332  suctr  4343  vuniex  4360  uniexg  4361  unexb  4363  snnex  4369  pwnex  4370  uniuni  4372  eusvnf  4374  eusvnfb  4375  iunpw  4401  unon  4427  ordunisuc2r  4430  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsucunielexmid  4446  elirr  4456  en2lp  4469  dtruex  4474  onintexmid  4487  reg3exmidlemwe  4493  dcextest  4495  finds  4514  finds2  4515  elnn  4519  limom  4527  0nelxp  4567  opelxp  4569  opeliunxp  4594  elvv  4601  elvvv  4602  elvvuni  4603  xpsspw  4651  relopabi  4665  opabid2  4670  difopab  4672  xpiindim  4676  raliunxp  4680  rexiunxp  4681  ralxpf  4685  rexxpf  4686  relop  4689  cnvco  4724  dfrn2  4727  dfdm4  4731  dmss  4738  dmin  4747  dmiun  4748  dmuni  4749  dm0  4753  dmi  4754  reldm0  4757  elreldm  4765  elrnmpt1  4790  dmrnssfld  4802  dmcoss  4808  dmcosseq  4810  opelresg  4826  resieq  4829  dmres  4840  elres  4855  relssres  4857  resopab  4863  resiexg  4864  iss  4865  dfres2  4871  dfima2  4883  imadmrn  4891  imai  4895  csbima12g  4900  elimasng  4907  args  4908  epini  4910  iniseg  4911  dfse2  4912  exse2  4913  cotr  4920  issref  4921  cnvsym  4922  intasym  4923  asymref  4924  intirr  4925  brcodir  4926  codir  4927  qfto  4928  poirr2  4931  cnvopab  4940  cnv0  4942  cnvi  4943  cnvdif  4945  rniun  4949  dminss  4953  imainss  4954  inimasn  4956  xpmlem  4959  dmxpss  4969  rnxpid  4973  ssrnres  4981  rninxp  4982  dminxp  4983  cnvcnv3  4988  dfrel2  4989  dmsnm  5004  dmsnopg  5010  cnvcnvsn  5015  dmsnsnsng  5016  cnvsng  5024  elxp4  5026  elxp5  5027  cnvresima  5028  dfco2  5038  dfco2a  5039  cores  5042  resco  5043  imaco  5044  rnco  5045  coiun  5048  co02  5052  coi1  5054  coass  5057  relssdmrn  5059  unielrel  5066  ressn  5079  cnviinm  5080  cnvpom  5081  cnvsom  5082  uniabio  5098  iotaval  5099  iotass  5105  sniota  5115  csbiotag  5116  dffun2  5133  dffun7  5150  dffun8  5151  dffun9  5152  funopg  5157  funssres  5165  funun  5167  funcnvsn  5168  funinsn  5172  funcnv2  5183  funcnv  5184  funcnv3  5185  funcnveq  5186  fun2cnv  5187  funcnvuni  5192  imadif  5203  funimaexglem  5206  isarep1  5209  2elresin  5234  fnres  5239  fcnvres  5306  fconstg  5319  fun11iun  5388  f1osng  5408  dffv3g  5417  fvssunirng  5436  sefvex  5442  fv3  5444  fvres  5445  nfunsn  5455  funimass4  5472  ssimaexg  5483  dmfco  5489  fvopab6  5517  fndmdif  5525  fvelrn  5551  dffo4  5568  f1ompt  5571  fmptco  5586  fsn  5592  fsng  5593  dfmpt  5597  dfmptg  5599  fnressn  5606  fressnfv  5607  fvsng  5616  resfunexg  5641  funfvima3  5651  idref  5658  abrexco  5660  imaiun  5661  dff13  5669  foeqcnvco  5691  f1eqcocnv  5692  fliftcnv  5696  isocnv2  5713  isoini  5719  isose  5722  riotav  5735  csbriotag  5742  acexmidlem2  5771  oprabid  5803  csbov123g  5809  0neqopab  5816  brabvv  5817  dfoprab2  5818  rnoprab  5854  eloprabga  5858  mpov  5861  f1opw  5977  opabex3d  6019  opabex3  6020  ofmres  6034  op1stg  6048  op2ndg  6049  1stval2  6053  2ndval2  6054  fo1st  6055  fo2nd  6056  f1stres  6057  f2ndres  6058  fo1stresm  6059  fo2ndresm  6060  xp1st  6063  xp2nd  6064  releldm2  6083  reldm  6084  sbcopeq1a  6085  csbopeq1a  6086  dfoprab3  6089  eloprabi  6094  mpomptsx  6095  dmmpossx  6097  fmpox  6098  mpofvex  6101  mpoexxg  6108  fmpoco  6113  df1st2  6116  df2nd2  6117  1stconst  6118  2ndconst  6119  dfmpo  6120  fo2ndf  6124  f1o2ndf1  6125  xporderlem  6128  cnvoprab  6131  f1od2  6132  brtpos2  6148  reldmtpos  6150  dmtpos  6153  rntpos  6154  ovtposg  6156  dftpos3  6159  dftpos4  6160  tpostpos  6161  tpossym  6173  tfrlem3  6208  tfrlem5  6211  tfrlem8  6215  tfrlemisucfn  6221  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemibex  6226  tfrlemi14d  6230  tfrexlem  6231  tfr1onlem3  6235  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  tfrcl  6261  rdgtfr  6271  rdgruledefgg  6272  rdgivallem  6278  rdgon  6283  rdg0g  6285  frec0g  6294  frecabex  6295  frecabcl  6296  frectfr  6297  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  oafnex  6340  sucinc  6341  fnoa  6343  oaexg  6344  omfnex  6345  fnom  6346  omexg  6347  fnoei  6348  oeiexg  6349  oeiv  6352  oacl  6356  omcl  6357  oeicl  6358  oav2  6359  nnsucelsuc  6387  nnsucuniel  6391  ercnv  6450  iserd  6455  eqerlem  6460  eqer  6461  ecdmn0m  6471  erth  6473  qsss  6488  ecid  6492  ecidg  6493  qsid  6494  iinerm  6501  qsel  6506  erovlem  6521  ecopovsym  6525  ecopover  6527  th3qlem2  6532  mapprc  6546  fnmap  6549  fnpm  6550  mapdm0  6557  mapval2  6572  mapsn  6584  mapsncnv  6589  mapsnf1o2  6590  ixpconstg  6601  ixpprc  6613  ixpin  6617  ixpiinm  6618  ixpssmap2g  6621  ixpssmapg  6622  elixpsn  6629  ixpsnf1o  6630  bren  6641  brdomg  6642  domen  6645  domeng  6646  idssen  6671  ener  6673  domtr  6679  ensn1g  6691  en1  6693  en1bg  6694  fundmen  6700  fundmeng  6701  mapsnen  6705  fiprc  6709  unen  6710  xpsnen  6715  xpsneng  6716  xpcomco  6720  xpcomeng  6722  xpassen  6724  xpdom2  6725  xpdom2g  6726  xpf1o  6738  mapen  6740  mapxpen  6742  xpmapenlem  6743  ssenen  6745  phplem4  6749  phplem3g  6750  nneneq  6751  php5  6752  phpm  6759  findcard  6782  findcard2  6783  findcard2s  6784  isinfinf  6791  ac6sfi  6792  exmidpw  6802  unfidisj  6810  fiintim  6817  xpfi  6818  fisseneq  6820  ssfirab  6822  snexxph  6838  fidcenumlemr  6843  sbthlemi10  6854  isbth  6855  ssfii  6862  fi0  6863  fiss  6865  cnvinfex  6905  eqinfti  6907  infvalti  6909  infglbti  6912  infmoti  6915  ordiso2  6920  djuf1olem  6938  djuss  6955  ctm  6994  ctssdccl  6996  ctssdclemr  6997  finomni  7012  exmidomni  7014  fodjuomnilemdc  7016  pm54.43  7051  exmidfodomrlemim  7062  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  acfun  7068  ccfunen  7084  cc2lem  7086  cc3  7088  indpi  7162  dfplpq2  7174  enq0sym  7252  enq0ref  7253  enq0tr  7254  nqnq0pi  7258  nqnq0  7261  mulnnnq0  7270  nqprm  7362  nqprrnd  7363  nqprdisj  7364  nqprloc  7365  nqprl  7371  nqpru  7372  addnqprlemrl  7377  addnqprlemru  7378  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemrl  7393  mulnqprlemru  7394  mulnqprlemfl  7395  mulnqprlemfu  7396  ltnqpr  7413  ltnqpri  7414  archpr  7463  cauappcvgprlemladdfu  7474  cauappcvgprlemladdfl  7475  cauappcvgprlem2  7480  caucvgprlemladdfu  7497  caucvgprlem2  7500  caucvgprprlemopu  7519  suplocexprlemmu  7538  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  cnm  7652  ltresr  7659  peano1nnnn  7672  peano2nnnn  7673  axcnre  7701  axpre-apti  7705  renfdisj  7836  dfinfre  8726  1nn  8743  peano2nn  8744  indstr  9400  cnref1o  9452  ioof  9766  fzpr  9869  frec2uzrand  10190  frec2uzf1od  10191  frecuzrdgtcl  10197  frecuzrdgfunlem  10204  frecfzennn  10211  ser3le  10303  hashinfom  10536  hashunlem  10562  hashun  10563  hashxp  10584  hashfacen  10591  zfz1isolem1  10595  zfz1iso  10596  shftfvalg  10602  ovshftex  10603  shftfibg  10604  shftfval  10605  shftfib  10607  shftfn  10608  2shfti  10615  shftvalg  10620  shftval4g  10621  maxabslemval  10992  fimaxre2  11010  xrmaxiflemval  11031  fclim  11075  climshft  11085  zsumdc  11165  fsum3  11168  fsum2dlemstep  11215  fsumcnv  11218  fisumcom2  11219  fisum0diag2  11228  fsumconst  11235  modfsummodlemstep  11238  fsumabs  11246  fsumrelem  11252  fsumiun  11258  ntrivcvgap  11329  algrf  11737  qredeu  11789  isprm2  11809  prmind2  11812  ennnfonelemex  11938  ennnfonelemrn  11943  exmidunben  11950  ctinfom  11952  ctinf  11954  qnnen  11955  enctlem  11956  ctiunctlemfo  11963  slotslfn  11999  restfn  12138  elrest  12141  bastg  12244  distop  12268  topnex  12269  epttop  12273  tgrest  12352  resttopon  12354  restco  12357  cnrest2  12419  cnptopresti  12421  cnptoprest  12422  cnptoprest2  12423  txuni2  12439  txbas  12441  eltx  12442  txcnp  12454  txcnmpt  12456  txrest  12459  txdis1cn  12461  txlm  12462  cnmpt1st  12471  cnmpt2nd  12472  txhmeo  12502  txswaphmeolem  12503  xmetec  12620  metrest  12689  reldvg  12831  dvfgg  12840  dvcj  12856  pilem3  12886  bdcvv  13160  bdsnss  13176  bdop  13178  bj-vprc  13199  bdinex1g  13204  bdssexg  13207  bj-inex  13210  bj-zfpair2  13213  bj-uniexg  13221  bdunexb  13223  bj-unexg  13224  bj-indint  13234  bj-ssom  13239  bj-om  13240  bj-2inf  13241  bj-bdfindis  13250  bj-nn0suc0  13253  bj-nnelirr  13256  bj-inf2vnlem1  13273  bj-inf2vnlem2  13274  bj-omex2  13280  bj-nn0sucALT  13281  bj-findis  13282  ss1oel2o  13294  pw1nct  13303  nninfsellemeq  13317  exmidsbthrlem  13324
  Copyright terms: Public domain W3C validator