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

Theorem vex 2661
Description: All setvar variables are sets (see isset 2664). 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 1660 . 2  |-  x  =  x
2 df-v 2660 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2226 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 145 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1463   _Vcvv 2658
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2660
This theorem is referenced by:  elv  2662  elvd  2663  isset  2664  eqvisset  2668  ralv  2675  rexv  2676  reuv  2677  rmov  2678  rabab  2679  sbhypf  2707  ceqex  2784  ralab  2815  rexab  2817  mo2icl  2834  reu8  2851  csbvarg  2998  csbiebg  3010  sbcnestgf  3019  sbnfc2  3028  ddifnel  3175  ddifstab  3176  csbing  3251  unssdif  3279  unssin  3283  inssun  3284  invdif  3286  vn0  3341  vn0m  3342  eqv  3350  abvor0dc  3354  sbss  3439  velpw  3485  elpwg  3486  velsn  3512  vsnid  3525  exsnrex  3534  dftp2  3540  prmg  3612  prnzg  3615  snssg  3624  difprsnss  3626  sneqrg  3657  preq12bg  3668  pwprss  3700  pwtpss  3701  pwv  3703  unipr  3718  uniprg  3719  unisng  3721  elintg  3747  elintrabg  3752  intss1  3754  ssint  3755  intmin  3759  intss  3760  intssunim  3761  intmin4  3767  intab  3768  intun  3770  intpr  3771  intprg  3772  uniintsnr  3775  iinconstm  3790  iuniin  3791  iinss1  3793  dfiin2g  3814  dfiunv2  3817  ssiinf  3830  iinss  3832  iinss2  3833  0iin  3839  iinab  3842  iundif2ss  3846  iindif2m  3848  iinin2m  3849  iinuniss  3863  sspwuni  3865  pwpwab  3868  iinpw  3871  iunpwss  3872  brab1  3943  csbopabg  3974  mptv  3993  trint  4009  vnex  4027  inex1g  4032  ssexg  4035  inteximm  4042  inuni  4048  repizf2  4054  axpweq  4063  bnd2  4065  pwuni  4084  exmidundif  4097  exmidundifim  4098  zfpair2  4100  rext  4105  sspwb  4106  unipw  4107  ssextss  4110  euabex  4115  mss  4116  exss  4117  opth  4127  opthg  4128  copsexg  4134  copsex4g  4137  moop2  4141  euotd  4144  opabid  4147  elopab  4148  opelopabsbALT  4149  opelopabsb  4150  opabm  4170  pwin  4172  pwunss  4173  epelg  4180  epel  4182  pofun  4202  epse  4232  tron  4272  sucel  4300  suctr  4311  vuniex  4328  uniexg  4329  unexb  4331  snnex  4337  pwnex  4338  uniuni  4340  eusvnf  4342  eusvnfb  4343  iunpw  4369  unon  4395  ordunisuc2r  4398  ordtri2or2exmidlem  4409  onsucelsucexmidlem  4412  ordsucunielexmid  4414  elirr  4424  en2lp  4437  dtruex  4442  onintexmid  4455  reg3exmidlemwe  4461  dcextest  4463  finds  4482  finds2  4483  elnn  4487  limom  4495  0nelxp  4535  opelxp  4537  opeliunxp  4562  elvv  4569  elvvv  4570  elvvuni  4571  xpsspw  4619  relopabi  4633  opabid2  4638  difopab  4640  xpiindim  4644  raliunxp  4648  rexiunxp  4649  ralxpf  4653  rexxpf  4654  relop  4657  cnvco  4692  dfrn2  4695  dfdm4  4699  dmss  4706  dmin  4715  dmiun  4716  dmuni  4717  dm0  4721  dmi  4722  reldm0  4725  elreldm  4733  elrnmpt1  4758  dmrnssfld  4770  dmcoss  4776  dmcosseq  4778  opelresg  4794  resieq  4797  dmres  4808  elres  4823  relssres  4825  resopab  4831  resiexg  4832  iss  4833  dfres2  4839  dfima2  4851  imadmrn  4859  imai  4863  csbima12g  4868  elimasng  4875  args  4876  epini  4878  iniseg  4879  dfse2  4880  exse2  4881  cotr  4888  issref  4889  cnvsym  4890  intasym  4891  asymref  4892  intirr  4893  brcodir  4894  codir  4895  qfto  4896  poirr2  4899  cnvopab  4908  cnv0  4910  cnvi  4911  cnvdif  4913  rniun  4917  dminss  4921  imainss  4922  inimasn  4924  xpmlem  4927  dmxpss  4937  rnxpid  4941  ssrnres  4949  rninxp  4950  dminxp  4951  cnvcnv3  4956  dfrel2  4957  dmsnm  4972  dmsnopg  4978  cnvcnvsn  4983  dmsnsnsng  4984  cnvsng  4992  elxp4  4994  elxp5  4995  cnvresima  4996  dfco2  5006  dfco2a  5007  cores  5010  resco  5011  imaco  5012  rnco  5013  coiun  5016  co02  5020  coi1  5022  coass  5025  relssdmrn  5027  unielrel  5034  ressn  5047  cnviinm  5048  cnvpom  5049  cnvsom  5050  uniabio  5066  iotaval  5067  iotass  5073  sniota  5083  csbiotag  5084  dffun2  5101  dffun7  5118  dffun8  5119  dffun9  5120  funopg  5125  funssres  5133  funun  5135  funcnvsn  5136  funinsn  5140  funcnv2  5151  funcnv  5152  funcnv3  5153  funcnveq  5154  fun2cnv  5155  funcnvuni  5160  imadif  5171  funimaexglem  5174  isarep1  5177  2elresin  5202  fnres  5207  fcnvres  5274  fconstg  5287  fun11iun  5354  f1osng  5374  dffv3g  5383  fvssunirng  5402  sefvex  5408  fv3  5410  fvres  5411  nfunsn  5421  funimass4  5438  ssimaexg  5449  dmfco  5455  fvopab6  5483  fndmdif  5491  fvelrn  5517  dffo4  5534  f1ompt  5537  fmptco  5552  fsn  5558  fsng  5559  dfmpt  5563  dfmptg  5565  fnressn  5572  fressnfv  5573  fvsng  5582  resfunexg  5607  funfvima3  5617  idref  5624  abrexco  5626  imaiun  5627  dff13  5635  foeqcnvco  5657  f1eqcocnv  5658  fliftcnv  5662  isocnv2  5679  isoini  5685  isose  5688  riotav  5701  csbriotag  5708  acexmidlem2  5737  oprabid  5769  csbov123g  5775  0neqopab  5782  brabvv  5783  dfoprab2  5784  rnoprab  5820  eloprabga  5824  mpov  5827  f1opw  5943  opabex3d  5985  opabex3  5986  ofmres  6000  op1stg  6014  op2ndg  6015  1stval2  6019  2ndval2  6020  fo1st  6021  fo2nd  6022  f1stres  6023  f2ndres  6024  fo1stresm  6025  fo2ndresm  6026  xp1st  6029  xp2nd  6030  releldm2  6049  reldm  6050  sbcopeq1a  6051  csbopeq1a  6052  dfoprab3  6055  eloprabi  6060  mpomptsx  6061  dmmpossx  6063  fmpox  6064  mpofvex  6067  mpoexxg  6074  fmpoco  6079  df1st2  6082  df2nd2  6083  1stconst  6084  2ndconst  6085  dfmpo  6086  fo2ndf  6090  f1o2ndf1  6091  xporderlem  6094  cnvoprab  6097  f1od2  6098  brtpos2  6114  reldmtpos  6116  dmtpos  6119  rntpos  6120  ovtposg  6122  dftpos3  6125  dftpos4  6126  tpostpos  6127  tpossym  6139  tfrlem3  6174  tfrlem5  6177  tfrlem8  6181  tfrlemisucfn  6187  tfrlemisucaccv  6188  tfrlemibxssdm  6190  tfrlemibfn  6191  tfrlemibex  6192  tfrlemi14d  6196  tfrexlem  6197  tfr1onlem3  6201  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemres  6212  tfri1dALT  6214  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemres  6225  tfrcl  6227  rdgtfr  6237  rdgruledefgg  6238  rdgivallem  6244  rdgon  6249  rdg0g  6251  frec0g  6260  frecabex  6261  frecabcl  6262  frectfr  6263  freccllem  6265  frecfcllem  6267  frecsuclem  6269  frecrdg  6271  oafnex  6306  sucinc  6307  fnoa  6309  oaexg  6310  omfnex  6311  fnom  6312  omexg  6313  fnoei  6314  oeiexg  6315  oeiv  6318  oacl  6322  omcl  6323  oeicl  6324  oav2  6325  nnsucelsuc  6353  nnsucuniel  6357  ercnv  6416  iserd  6421  eqerlem  6426  eqer  6427  ecdmn0m  6437  erth  6439  qsss  6454  ecid  6458  ecidg  6459  qsid  6460  iinerm  6467  qsel  6472  erovlem  6487  ecopovsym  6491  ecopover  6493  th3qlem2  6498  mapprc  6512  fnmap  6515  fnpm  6516  mapdm0  6523  mapval2  6538  mapsn  6550  mapsncnv  6555  mapsnf1o2  6556  ixpconstg  6567  ixpprc  6579  ixpin  6583  ixpiinm  6584  ixpssmap2g  6587  ixpssmapg  6588  elixpsn  6595  ixpsnf1o  6596  bren  6607  brdomg  6608  domen  6611  domeng  6612  idssen  6637  ener  6639  domtr  6645  ensn1g  6657  en1  6659  en1bg  6660  fundmen  6666  fundmeng  6667  mapsnen  6671  fiprc  6675  unen  6676  xpsnen  6681  xpsneng  6682  xpcomco  6686  xpcomeng  6688  xpassen  6690  xpdom2  6691  xpdom2g  6692  xpf1o  6704  mapen  6706  mapxpen  6708  xpmapenlem  6709  ssenen  6711  phplem4  6715  phplem3g  6716  nneneq  6717  php5  6718  phpm  6725  findcard  6748  findcard2  6749  findcard2s  6750  isinfinf  6757  ac6sfi  6758  exmidpw  6768  unfidisj  6776  fiintim  6783  xpfi  6784  fisseneq  6786  ssfirab  6788  snexxph  6804  fidcenumlemr  6809  sbthlemi10  6820  isbth  6821  ssfii  6828  fi0  6829  fiss  6831  cnvinfex  6871  eqinfti  6873  infvalti  6875  infglbti  6878  infmoti  6881  ordiso2  6886  djuf1olem  6904  djuss  6921  ctm  6960  ctssdccl  6962  ctssdclemr  6963  finomni  6978  exmidomni  6980  fodjuomnilemdc  6982  pm54.43  7012  exmidfodomrlemim  7021  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  acfun  7027  ccfunen  7043  indpi  7114  dfplpq2  7126  enq0sym  7204  enq0ref  7205  enq0tr  7206  nqnq0pi  7210  nqnq0  7213  mulnnnq0  7222  nqprm  7314  nqprrnd  7315  nqprdisj  7316  nqprloc  7317  nqprl  7323  nqpru  7324  addnqprlemrl  7329  addnqprlemru  7330  addnqprlemfl  7331  addnqprlemfu  7332  mulnqprlemrl  7345  mulnqprlemru  7346  mulnqprlemfl  7347  mulnqprlemfu  7348  ltnqpr  7365  ltnqpri  7366  archpr  7415  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlem2  7432  caucvgprlemladdfu  7449  caucvgprlem2  7452  caucvgprprlemopu  7471  suplocexprlemmu  7490  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  cnm  7604  ltresr  7611  peano1nnnn  7624  peano2nnnn  7625  axcnre  7653  axpre-apti  7657  renfdisj  7788  dfinfre  8674  1nn  8691  peano2nn  8692  indstr  9340  cnref1o  9392  ioof  9705  fzpr  9808  frec2uzrand  10129  frec2uzf1od  10130  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  frecfzennn  10150  ser3le  10242  hashinfom  10475  hashunlem  10501  hashun  10502  hashxp  10523  hashfacen  10530  zfz1isolem1  10534  zfz1iso  10535  shftfvalg  10541  ovshftex  10542  shftfibg  10543  shftfval  10544  shftfib  10546  shftfn  10547  2shfti  10554  shftvalg  10559  shftval4g  10560  maxabslemval  10931  fimaxre2  10949  xrmaxiflemval  10970  fclim  11014  climshft  11024  zsumdc  11104  fsum3  11107  fsum2dlemstep  11154  fsumcnv  11157  fisumcom2  11158  fisum0diag2  11167  fsumconst  11174  modfsummodlemstep  11177  fsumabs  11185  fsumrelem  11191  fsumiun  11197  algrf  11633  qredeu  11685  isprm2  11705  prmind2  11708  ennnfonelemex  11833  ennnfonelemrn  11838  exmidunben  11845  ctinfom  11847  ctinf  11849  qnnen  11850  enctlem  11851  ctiunctlemfo  11858  slotslfn  11891  restfn  12030  elrest  12033  bastg  12136  distop  12160  topnex  12161  epttop  12165  tgrest  12244  resttopon  12246  restco  12249  cnrest2  12311  cnptopresti  12313  cnptoprest  12314  cnptoprest2  12315  txuni2  12331  txbas  12333  eltx  12334  txcnp  12346  txcnmpt  12348  txrest  12351  txdis1cn  12353  txlm  12354  cnmpt1st  12363  cnmpt2nd  12364  txhmeo  12394  txswaphmeolem  12395  xmetec  12512  metrest  12581  reldvg  12723  dvfgg  12732  dvcj  12748  bdcvv  12889  bdsnss  12905  bdop  12907  bj-vprc  12928  bdinex1g  12933  bdssexg  12936  bj-inex  12939  bj-zfpair2  12942  bj-uniexg  12950  bdunexb  12952  bj-unexg  12953  bj-indint  12963  bj-ssom  12968  bj-om  12969  bj-2inf  12970  bj-bdfindis  12979  bj-nn0suc0  12982  bj-nnelirr  12985  bj-inf2vnlem1  13002  bj-inf2vnlem2  13003  bj-omex2  13009  bj-nn0sucALT  13010  bj-findis  13011  ss1oel2o  13023  nninfsellemeq  13044  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator