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

Theorem vex 2663
Description: All setvar variables are sets (see isset 2666). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
vex  |-  x  e. 
_V

Proof of Theorem vex
StepHypRef Expression
1 equid 1662 . 2  |-  x  =  x
2 df-v 2662 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2228 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 145 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1465   _Vcvv 2660
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  elv  2664  elvd  2665  isset  2666  eqvisset  2670  ralv  2677  rexv  2678  reuv  2679  rmov  2680  rabab  2681  sbhypf  2709  ceqex  2786  ralab  2817  rexab  2819  mo2icl  2836  reu8  2853  csbvarg  3000  csbiebg  3012  sbcnestgf  3021  sbnfc2  3030  ddifnel  3177  ddifstab  3178  csbing  3253  unssdif  3281  unssin  3285  inssun  3286  invdif  3288  vn0  3343  vn0m  3344  eqv  3352  abvor0dc  3356  sbss  3441  velpw  3487  elpwg  3488  velsn  3514  vsnid  3527  exsnrex  3536  dftp2  3542  prmg  3614  prnzg  3617  snssg  3626  difprsnss  3628  sneqrg  3659  preq12bg  3670  pwprss  3702  pwtpss  3703  pwv  3705  unipr  3720  uniprg  3721  unisng  3723  elintg  3749  elintrabg  3754  intss1  3756  ssint  3757  intmin  3761  intss  3762  intssunim  3763  intmin4  3769  intab  3770  intun  3772  intpr  3773  intprg  3774  uniintsnr  3777  iinconstm  3792  iuniin  3793  iinss1  3795  dfiin2g  3816  dfiunv2  3819  ssiinf  3832  iinss  3834  iinss2  3835  0iin  3841  iinab  3844  iundif2ss  3848  iindif2m  3850  iinin2m  3851  iinuniss  3865  sspwuni  3867  pwpwab  3870  iinpw  3873  iunpwss  3874  brab1  3945  csbopabg  3976  mptv  3995  trint  4011  vnex  4029  inex1g  4034  ssexg  4037  inteximm  4044  inuni  4050  repizf2  4056  axpweq  4065  bnd2  4067  pwuni  4086  exmidundif  4099  exmidundifim  4100  zfpair2  4102  rext  4107  sspwb  4108  unipw  4109  ssextss  4112  euabex  4117  mss  4118  exss  4119  opth  4129  opthg  4130  copsexg  4136  copsex4g  4139  moop2  4143  euotd  4146  opabid  4149  elopab  4150  opelopabsbALT  4151  opelopabsb  4152  opabm  4172  pwin  4174  pwunss  4175  epelg  4182  epel  4184  pofun  4204  epse  4234  tron  4274  sucel  4302  suctr  4313  vuniex  4330  uniexg  4331  unexb  4333  snnex  4339  pwnex  4340  uniuni  4342  eusvnf  4344  eusvnfb  4345  iunpw  4371  unon  4397  ordunisuc2r  4400  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  ordsucunielexmid  4416  elirr  4426  en2lp  4439  dtruex  4444  onintexmid  4457  reg3exmidlemwe  4463  dcextest  4465  finds  4484  finds2  4485  elnn  4489  limom  4497  0nelxp  4537  opelxp  4539  opeliunxp  4564  elvv  4571  elvvv  4572  elvvuni  4573  xpsspw  4621  relopabi  4635  opabid2  4640  difopab  4642  xpiindim  4646  raliunxp  4650  rexiunxp  4651  ralxpf  4655  rexxpf  4656  relop  4659  cnvco  4694  dfrn2  4697  dfdm4  4701  dmss  4708  dmin  4717  dmiun  4718  dmuni  4719  dm0  4723  dmi  4724  reldm0  4727  elreldm  4735  elrnmpt1  4760  dmrnssfld  4772  dmcoss  4778  dmcosseq  4780  opelresg  4796  resieq  4799  dmres  4810  elres  4825  relssres  4827  resopab  4833  resiexg  4834  iss  4835  dfres2  4841  dfima2  4853  imadmrn  4861  imai  4865  csbima12g  4870  elimasng  4877  args  4878  epini  4880  iniseg  4881  dfse2  4882  exse2  4883  cotr  4890  issref  4891  cnvsym  4892  intasym  4893  asymref  4894  intirr  4895  brcodir  4896  codir  4897  qfto  4898  poirr2  4901  cnvopab  4910  cnv0  4912  cnvi  4913  cnvdif  4915  rniun  4919  dminss  4923  imainss  4924  inimasn  4926  xpmlem  4929  dmxpss  4939  rnxpid  4943  ssrnres  4951  rninxp  4952  dminxp  4953  cnvcnv3  4958  dfrel2  4959  dmsnm  4974  dmsnopg  4980  cnvcnvsn  4985  dmsnsnsng  4986  cnvsng  4994  elxp4  4996  elxp5  4997  cnvresima  4998  dfco2  5008  dfco2a  5009  cores  5012  resco  5013  imaco  5014  rnco  5015  coiun  5018  co02  5022  coi1  5024  coass  5027  relssdmrn  5029  unielrel  5036  ressn  5049  cnviinm  5050  cnvpom  5051  cnvsom  5052  uniabio  5068  iotaval  5069  iotass  5075  sniota  5085  csbiotag  5086  dffun2  5103  dffun7  5120  dffun8  5121  dffun9  5122  funopg  5127  funssres  5135  funun  5137  funcnvsn  5138  funinsn  5142  funcnv2  5153  funcnv  5154  funcnv3  5155  funcnveq  5156  fun2cnv  5157  funcnvuni  5162  imadif  5173  funimaexglem  5176  isarep1  5179  2elresin  5204  fnres  5209  fcnvres  5276  fconstg  5289  fun11iun  5356  f1osng  5376  dffv3g  5385  fvssunirng  5404  sefvex  5410  fv3  5412  fvres  5413  nfunsn  5423  funimass4  5440  ssimaexg  5451  dmfco  5457  fvopab6  5485  fndmdif  5493  fvelrn  5519  dffo4  5536  f1ompt  5539  fmptco  5554  fsn  5560  fsng  5561  dfmpt  5565  dfmptg  5567  fnressn  5574  fressnfv  5575  fvsng  5584  resfunexg  5609  funfvima3  5619  idref  5626  abrexco  5628  imaiun  5629  dff13  5637  foeqcnvco  5659  f1eqcocnv  5660  fliftcnv  5664  isocnv2  5681  isoini  5687  isose  5690  riotav  5703  csbriotag  5710  acexmidlem2  5739  oprabid  5771  csbov123g  5777  0neqopab  5784  brabvv  5785  dfoprab2  5786  rnoprab  5822  eloprabga  5826  mpov  5829  f1opw  5945  opabex3d  5987  opabex3  5988  ofmres  6002  op1stg  6016  op2ndg  6017  1stval2  6021  2ndval2  6022  fo1st  6023  fo2nd  6024  f1stres  6025  f2ndres  6026  fo1stresm  6027  fo2ndresm  6028  xp1st  6031  xp2nd  6032  releldm2  6051  reldm  6052  sbcopeq1a  6053  csbopeq1a  6054  dfoprab3  6057  eloprabi  6062  mpomptsx  6063  dmmpossx  6065  fmpox  6066  mpofvex  6069  mpoexxg  6076  fmpoco  6081  df1st2  6084  df2nd2  6085  1stconst  6086  2ndconst  6087  dfmpo  6088  fo2ndf  6092  f1o2ndf1  6093  xporderlem  6096  cnvoprab  6099  f1od2  6100  brtpos2  6116  reldmtpos  6118  dmtpos  6121  rntpos  6122  ovtposg  6124  dftpos3  6127  dftpos4  6128  tpostpos  6129  tpossym  6141  tfrlem3  6176  tfrlem5  6179  tfrlem8  6183  tfrlemisucfn  6189  tfrlemisucaccv  6190  tfrlemibxssdm  6192  tfrlemibfn  6193  tfrlemibex  6194  tfrlemi14d  6198  tfrexlem  6199  tfr1onlem3  6203  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemres  6214  tfri1dALT  6216  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemres  6227  tfrcl  6229  rdgtfr  6239  rdgruledefgg  6240  rdgivallem  6246  rdgon  6251  rdg0g  6253  frec0g  6262  frecabex  6263  frecabcl  6264  frectfr  6265  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecrdg  6273  oafnex  6308  sucinc  6309  fnoa  6311  oaexg  6312  omfnex  6313  fnom  6314  omexg  6315  fnoei  6316  oeiexg  6317  oeiv  6320  oacl  6324  omcl  6325  oeicl  6326  oav2  6327  nnsucelsuc  6355  nnsucuniel  6359  ercnv  6418  iserd  6423  eqerlem  6428  eqer  6429  ecdmn0m  6439  erth  6441  qsss  6456  ecid  6460  ecidg  6461  qsid  6462  iinerm  6469  qsel  6474  erovlem  6489  ecopovsym  6493  ecopover  6495  th3qlem2  6500  mapprc  6514  fnmap  6517  fnpm  6518  mapdm0  6525  mapval2  6540  mapsn  6552  mapsncnv  6557  mapsnf1o2  6558  ixpconstg  6569  ixpprc  6581  ixpin  6585  ixpiinm  6586  ixpssmap2g  6589  ixpssmapg  6590  elixpsn  6597  ixpsnf1o  6598  bren  6609  brdomg  6610  domen  6613  domeng  6614  idssen  6639  ener  6641  domtr  6647  ensn1g  6659  en1  6661  en1bg  6662  fundmen  6668  fundmeng  6669  mapsnen  6673  fiprc  6677  unen  6678  xpsnen  6683  xpsneng  6684  xpcomco  6688  xpcomeng  6690  xpassen  6692  xpdom2  6693  xpdom2g  6694  xpf1o  6706  mapen  6708  mapxpen  6710  xpmapenlem  6711  ssenen  6713  phplem4  6717  phplem3g  6718  nneneq  6719  php5  6720  phpm  6727  findcard  6750  findcard2  6751  findcard2s  6752  isinfinf  6759  ac6sfi  6760  exmidpw  6770  unfidisj  6778  fiintim  6785  xpfi  6786  fisseneq  6788  ssfirab  6790  snexxph  6806  fidcenumlemr  6811  sbthlemi10  6822  isbth  6823  ssfii  6830  fi0  6831  fiss  6833  cnvinfex  6873  eqinfti  6875  infvalti  6877  infglbti  6880  infmoti  6883  ordiso2  6888  djuf1olem  6906  djuss  6923  ctm  6962  ctssdccl  6964  ctssdclemr  6965  finomni  6980  exmidomni  6982  fodjuomnilemdc  6984  pm54.43  7014  exmidfodomrlemim  7025  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  acfun  7031  ccfunen  7047  indpi  7118  dfplpq2  7130  enq0sym  7208  enq0ref  7209  enq0tr  7210  nqnq0pi  7214  nqnq0  7217  mulnnnq0  7226  nqprm  7318  nqprrnd  7319  nqprdisj  7320  nqprloc  7321  nqprl  7327  nqpru  7328  addnqprlemrl  7333  addnqprlemru  7334  addnqprlemfl  7335  addnqprlemfu  7336  mulnqprlemrl  7349  mulnqprlemru  7350  mulnqprlemfl  7351  mulnqprlemfu  7352  ltnqpr  7369  ltnqpri  7370  archpr  7419  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlem2  7436  caucvgprlemladdfu  7453  caucvgprlem2  7456  caucvgprprlemopu  7475  suplocexprlemmu  7494  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  cnm  7608  ltresr  7615  peano1nnnn  7628  peano2nnnn  7629  axcnre  7657  axpre-apti  7661  renfdisj  7792  dfinfre  8682  1nn  8699  peano2nn  8700  indstr  9356  cnref1o  9408  ioof  9722  fzpr  9825  frec2uzrand  10146  frec2uzf1od  10147  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  frecfzennn  10167  ser3le  10259  hashinfom  10492  hashunlem  10518  hashun  10519  hashxp  10540  hashfacen  10547  zfz1isolem1  10551  zfz1iso  10552  shftfvalg  10558  ovshftex  10559  shftfibg  10560  shftfval  10561  shftfib  10563  shftfn  10564  2shfti  10571  shftvalg  10576  shftval4g  10577  maxabslemval  10948  fimaxre2  10966  xrmaxiflemval  10987  fclim  11031  climshft  11041  zsumdc  11121  fsum3  11124  fsum2dlemstep  11171  fsumcnv  11174  fisumcom2  11175  fisum0diag2  11184  fsumconst  11191  modfsummodlemstep  11194  fsumabs  11202  fsumrelem  11208  fsumiun  11214  algrf  11653  qredeu  11705  isprm2  11725  prmind2  11728  ennnfonelemex  11854  ennnfonelemrn  11859  exmidunben  11866  ctinfom  11868  ctinf  11870  qnnen  11871  enctlem  11872  ctiunctlemfo  11879  slotslfn  11912  restfn  12051  elrest  12054  bastg  12157  distop  12181  topnex  12182  epttop  12186  tgrest  12265  resttopon  12267  restco  12270  cnrest2  12332  cnptopresti  12334  cnptoprest  12335  cnptoprest2  12336  txuni2  12352  txbas  12354  eltx  12355  txcnp  12367  txcnmpt  12369  txrest  12372  txdis1cn  12374  txlm  12375  cnmpt1st  12384  cnmpt2nd  12385  txhmeo  12415  txswaphmeolem  12416  xmetec  12533  metrest  12602  reldvg  12744  dvfgg  12753  dvcj  12769  pilem3  12791  bdcvv  12982  bdsnss  12998  bdop  13000  bj-vprc  13021  bdinex1g  13026  bdssexg  13029  bj-inex  13032  bj-zfpair2  13035  bj-uniexg  13043  bdunexb  13045  bj-unexg  13046  bj-indint  13056  bj-ssom  13061  bj-om  13062  bj-2inf  13063  bj-bdfindis  13072  bj-nn0suc0  13075  bj-nnelirr  13078  bj-inf2vnlem1  13095  bj-inf2vnlem2  13096  bj-omex2  13102  bj-nn0sucALT  13103  bj-findis  13104  ss1oel2o  13116  nninfsellemeq  13137  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator