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

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

Proof of Theorem vex
StepHypRef Expression
1 equid 1571 . 2 x = x
2 df-v 2536 . . 3 V = {xx = x}
32abeq2i 2131 . 2 (x V ↔ x = x)
41, 3mpbir 134 1 x V
Colors of variables: wff set class
Syntax hints:   wcel 1376  Vcvv 2534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  isset  2538  ralv  2547  rexv  2548  reuv  2549  rmov  2550  rabab  2551  sbhypf  2579  ceqex  2647  ralab  2677  rexab  2679  mo2icl  2696  reu8  2713  csbvarg  2854  csbiebg  2866  sbcnestgf  2874  sbnfc2  2885  ddifnel  3054  csbing  3123  unssdif  3151  unssin  3155  inssun  3156  invdif  3158  vn0  3210  vn0m  3211  eqv  3219  abvor0dc  3221  sbss  3310  selpw  3319  elpwg  3320  ssnid  3356  exsnrex  3365  dftp2  3371  prmg  3441  prnzg  3444  snssg  3452  difprsnss  3454  sneqrg  3486  preq12bg  3497  pwprss  3529  pwtpss  3530  pwv  3532  unipr  3547  uniprg  3548  unisng  3550  elintg  3576  elintrabg  3581  intss1  3583  ssint  3584  intmin  3588  intss  3589  intssunim  3590  intmin4  3596  intab  3597  intun  3599  intpr  3600  intprg  3601  uniintsnr  3604  iinconstm  3619  iuniin  3620  iinss1  3622  dfiin2g  3643  dfiunv2  3646  ssiinf  3659  iinss  3661  iinss2  3662  0iin  3668  iinab  3671  iundif2ss  3675  iindif2m  3677  iinin2m  3678  iinuniss  3690  sspwuni  3692  iinpw  3695  iunpwss  3696  brab1  3762  csbopabg  3788  mptv  3806  trint  3822  trintssm  3823  vprc  3841  inex1g  3846  ssexg  3849  inteximm  3856  inuni  3862  repizf2  3868  axpweq  3877  bnd2  3879  pwexg  3886  pwuni  3896  zfpair2  3898  rext  3904  sspwb  3905  unipw  3906  ssextss  3909  euabex  3914  mss  3915  exss  3916  opth  3927  opthg  3928  copsexg  3934  copsex4g  3937  moop2  3941  euotd  3944  opabid  3947  elopab  3948  opelopabsbOLD  3949  opelopabsb  3951  opabm  3971  pwin  3973  pwunss  3974  epelg  3981  epel  3983  pofun  4003  epse  4024  tron  4044  sucel  4072  suctrALT  4083  uniexg  4101  unexb  4103  snnex  4107  uniuni  4109  eusvnf  4111  eusvnfb  4112  iunpw  4137  unon  4162  ordunisuc2r  4165  onsucelsucexmidlem  4174  ordsucunielexmid  4176  elirr  4184  en2lp  4192  dtruex  4197  finds  4226  finds2  4227  elnn  4231  limom  4239  0nelxp  4275  opelxp  4277  opeliunxp  4298  elvv  4305  elvvv  4306  elvvuni  4307  xpsspw  4353  relopabi  4366  opabid2  4370  difopab  4372  xpiindim  4376  raliunxp  4380  rexiunxp  4381  ralxpf  4385  rexxpf  4386  relop  4389  cnvco  4423  dfrn2  4426  dfdm4  4430  dmss  4437  dmin  4446  dmiun  4447  dmuni  4448  dm0  4452  dmi  4453  reldm0  4456  elreldm  4463  elrnmpt1  4488  dmrnssfld  4498  dmcoss  4504  dmcosseq  4506  opelresg  4522  resieq  4525  dmres  4536  elres  4550  relssres  4552  resopab  4556  resiexg  4557  iss  4558  dfres2  4562  dfima2  4574  imadmrn  4582  imai  4585  csbima12g  4590  elimasng  4597  args  4598  epini  4600  iniseg  4601  dfse2  4602  exse2  4603  cotr  4610  issref  4611  cnvsym  4612  intasym  4613  asymref  4614  intirr  4615  brcodir  4616  codir  4617  qfto  4618  poirr2  4621  cnvopab  4630  cnv0  4631  cnvi  4632  cnvdif  4634  rniun  4638  dminss  4642  imainss  4643  inimasn  4645  xpmlem  4648  dmxpss  4657  rnxpid  4659  ssrnres  4667  rninxp  4668  dminxp  4669  cnvcnv3  4674  dfrel2  4675  dmsnm  4690  dmsnopg  4696  cnvcnvsn  4701  dmsnsnsng  4702  cnvsng  4710  elxp4  4712  elxp5  4713  cnvresima  4714  dfco2  4724  dfco2a  4725  cores  4728  resco  4729  imaco  4730  rnco  4731  coiun  4734  co02  4738  coi1  4740  coass  4743  relssdmrn  4745  unielrel  4749  ressn  4762  cnviinm  4763  cnvpom  4764  cnvsom  4765  uniabio  4781  iotaval  4782  iotass  4788  sniota  4798  csbiotag  4799  dffun2  4816  dffun7  4831  dffun8  4832  dffun9  4833  funopg  4837  funssres  4845  funun  4847  funcnvsn  4848  funcnv2  4862  funcnv  4863  funcnv3  4864  funcnveq  4865  fun2cnv  4866  funcnvuni  4871  imadif  4882  funimaexglem  4885  isarep1  4888  2elresin  4913  fnres  4918  fcnvres  4975  fconstg  4985  fun11iun  5049  f1osng  5069  dffv3g  5076  fvssunirng  5092  sefvex  5098  fv3  5099  fvres  5100  nfunsn  5109  funimass4  5126  ssimaexg  5137  dmfco  5143  fvopab6  5166  fndmdif  5174  fvelrn  5200  dffo4  5217  f1ompt  5222  fmptco  5232  fsn  5237  fsng  5238  dfmpt  5242  dfmptg  5244  fnressn  5251  fressnfv  5252  fvsng  5261  resfunexg  5284  funfvima3  5294  idref  5298  abrexco  5300  imaiun  5301  dff13  5309  foeqcnvco  5332  f1eqcocnv  5333  fliftcnv  5337  isocnv2  5354  isoini  5359  isose  5362  riotav  5374  csbriotag  5382  acexmidlem2  5412  oprabid  5440  csbov123g  5445  0neqopab  5452  brabvv  5453  dfoprab2  5454  rnoprab  5489  eloprabga  5493  mpt2v  5496  f1opw  5606  opabex3d  5647  opabex3  5648  ofmres  5662  op1stg  5676  op2ndg  5677  1stval2  5681  2ndval2  5682  fo1st  5683  fo2nd  5684  f1stres  5685  f2ndres  5686  fo1stresm  5687  fo2ndresm  5688  xp1st  5691  xp2nd  5692  releldm2  5710  reldm  5711  sbcopeq1a  5712  csbopeq1a  5713  dfoprab3  5716  eloprabi  5721  mpt2mptsx  5722  dmmpt2ssx  5724  fmpt2x  5725  mpt2fvex  5728  mpt2exxg  5732  fmpt2co  5736  df1st2  5739  df2nd2  5740  1stconst  5741  2ndconst  5742  dfmpt2  5743  fo2ndf  5747  f1o2ndf1  5748  xporderlem  5750  brtpos2  5764  reldmtpos  5766  dmtpos  5769  rntpos  5770  ovtposg  5772  dftpos3  5775  dftpos4  5776  tpostpos  5777  tpossym  5789  tfrlem3  5823  tfrlem5  5827  tfrlem8  5831  tfrlemisucfn  5834  tfrlemisucaccv  5835  tfrlemibxssdm  5837  tfrlemibfn  5838  tfrlemibex  5839  tfrlemi14d  5843  tfrlemi14  5844  tfrexlem  5845  rdgruledefgg  5857  rdgivallem  5863  rdgon  5868  frecabex  5874  frectfr  5875  frec0g  5877  frecsuclem3  5881  oafnex  5914  sucinc  5915  fnoa  5917  oaexg  5918  omfnex  5919  fnom  5920  omexg  5921  fnoei  5922  oeiexg  5923  oeiv  5926  oa0  5927  oei0  5929  oacl  5930  omcl  5931  oeicl  5932  oav2  5933  nnsucelsuc  5959  ercnv  6010  iserd  6015  eqerlem  6020  eqer  6021  ecdmn0m  6030  erth  6032  qsss  6047  ecid  6051  qsid  6052  iinerm  6059  qsel  6064  erovlem  6079  ecopovsym  6083  ecopover  6085  th3qlem2  6090
  Copyright terms: Public domain W3C validator