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

Theorem vex 2618
Description: All setvar variables are sets (see isset 2619). 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 1632 . 2  |-  x  =  x
2 df-v 2617 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2195 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 144 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1436   _Vcvv 2615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-v 2617
This theorem is referenced by:  isset  2619  eqvisset  2623  ralv  2630  rexv  2631  reuv  2632  rmov  2633  rabab  2634  sbhypf  2662  ceqex  2735  ralab  2766  rexab  2768  mo2icl  2785  reu8  2802  csbvarg  2947  csbiebg  2959  sbcnestgf  2968  sbnfc2  2977  ddifnel  3120  ddifstab  3121  csbing  3196  unssdif  3223  unssin  3227  inssun  3228  invdif  3230  vn0  3282  vn0m  3283  eqv  3291  abvor0dc  3295  sbss  3377  selpw  3422  elpwg  3423  velsn  3448  vsnid  3461  exsnrex  3470  dftp2  3476  prmg  3546  prnzg  3549  snssg  3558  difprsnss  3560  sneqrg  3591  preq12bg  3602  pwprss  3634  pwtpss  3635  pwv  3637  unipr  3652  uniprg  3653  unisng  3655  elintg  3681  elintrabg  3686  intss1  3688  ssint  3689  intmin  3693  intss  3694  intssunim  3695  intmin4  3701  intab  3702  intun  3704  intpr  3705  intprg  3706  uniintsnr  3709  iinconstm  3724  iuniin  3725  iinss1  3727  dfiin2g  3748  dfiunv2  3751  ssiinf  3764  iinss  3766  iinss2  3767  0iin  3773  iinab  3776  iundif2ss  3780  iindif2m  3782  iinin2m  3783  iinuniss  3795  sspwuni  3797  iinpw  3800  iunpwss  3801  brab1  3867  csbopabg  3893  mptv  3912  trint  3928  trintssmOLD  3930  vnex  3947  inex1g  3952  ssexg  3955  inteximm  3962  inuni  3968  repizf2  3974  axpweq  3983  bnd2  3985  pwuni  4003  exmidundif  4011  zfpair2  4013  rext  4018  sspwb  4019  unipw  4020  ssextss  4023  euabex  4028  mss  4029  exss  4030  opth  4040  opthg  4041  copsexg  4047  copsex4g  4050  moop2  4054  euotd  4057  opabid  4060  elopab  4061  opelopabsbALT  4062  opelopabsb  4063  opabm  4083  pwin  4085  pwunss  4086  epelg  4093  epel  4095  pofun  4115  epse  4145  tron  4185  sucel  4213  suctr  4224  uniexg  4241  unexb  4243  snnex  4247  uniuni  4249  eusvnf  4251  eusvnfb  4252  iunpw  4277  unon  4303  ordunisuc2r  4306  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  ordsucunielexmid  4322  elirr  4332  en2lp  4345  dtruex  4350  onintexmid  4363  reg3exmidlemwe  4369  dcextest  4371  finds  4390  finds2  4391  elnn  4395  limom  4403  0nelxp  4440  opelxp  4442  opeliunxp  4463  elvv  4470  elvvv  4471  elvvuni  4472  xpsspw  4520  relopabi  4533  opabid2  4537  difopab  4539  xpiindim  4543  raliunxp  4547  rexiunxp  4548  ralxpf  4552  rexxpf  4553  relop  4556  cnvco  4591  dfrn2  4594  dfdm4  4598  dmss  4605  dmin  4614  dmiun  4615  dmuni  4616  dm0  4620  dmi  4621  reldm0  4624  elreldm  4631  elrnmpt1  4656  dmrnssfld  4666  dmcoss  4672  dmcosseq  4674  opelresg  4690  resieq  4693  dmres  4703  elres  4717  relssres  4719  resopab  4725  resiexg  4726  iss  4727  dfres2  4733  dfima2  4745  imadmrn  4753  imai  4757  csbima12g  4762  elimasng  4769  args  4770  epini  4772  iniseg  4773  dfse2  4774  exse2  4775  cotr  4782  issref  4783  cnvsym  4784  intasym  4785  asymref  4786  intirr  4787  brcodir  4788  codir  4789  qfto  4790  poirr2  4793  cnvopab  4802  cnv0  4803  cnvi  4804  cnvdif  4806  rniun  4810  dminss  4814  imainss  4815  inimasn  4817  xpmlem  4820  dmxpss  4829  rnxpid  4833  ssrnres  4841  rninxp  4842  dminxp  4843  cnvcnv3  4848  dfrel2  4849  dmsnm  4864  dmsnopg  4870  cnvcnvsn  4875  dmsnsnsng  4876  cnvsng  4884  elxp4  4886  elxp5  4887  cnvresima  4888  dfco2  4898  dfco2a  4899  cores  4902  resco  4903  imaco  4904  rnco  4905  coiun  4908  co02  4912  coi1  4914  coass  4917  relssdmrn  4919  unielrel  4926  ressn  4939  cnviinm  4940  cnvpom  4941  cnvsom  4942  uniabio  4958  iotaval  4959  iotass  4965  sniota  4975  csbiotag  4976  dffun2  4993  dffun7  5009  dffun8  5010  dffun9  5011  funopg  5015  funssres  5023  funun  5025  funcnvsn  5026  funinsn  5030  funcnv2  5041  funcnv  5042  funcnv3  5043  funcnveq  5044  fun2cnv  5045  funcnvuni  5050  imadif  5061  funimaexglem  5064  isarep1  5067  2elresin  5092  fnres  5097  fcnvres  5159  fconstg  5172  fun11iun  5239  f1osng  5259  dffv3g  5266  fvssunirng  5285  sefvex  5291  fv3  5293  fvres  5294  nfunsn  5303  funimass4  5320  ssimaexg  5331  dmfco  5337  fvopab6  5361  fndmdif  5369  fvelrn  5395  dffo4  5412  f1ompt  5415  fmptco  5429  fsn  5434  fsng  5435  dfmpt  5439  dfmptg  5441  fnressn  5448  fressnfv  5449  fvsng  5458  resfunexg  5481  funfvima3  5491  idref  5499  abrexco  5501  imaiun  5502  dff13  5510  foeqcnvco  5532  f1eqcocnv  5533  fliftcnv  5537  isocnv2  5554  isoini  5560  isose  5563  riotav  5576  csbriotag  5583  acexmidlem2  5612  oprabid  5640  csbov123g  5646  0neqopab  5653  brabvv  5654  dfoprab2  5655  rnoprab  5690  eloprabga  5694  mpt2v  5697  f1opw  5810  opabex3d  5851  opabex3  5852  ofmres  5866  op1stg  5880  op2ndg  5881  1stval2  5885  2ndval2  5886  fo1st  5887  fo2nd  5888  f1stres  5889  f2ndres  5890  fo1stresm  5891  fo2ndresm  5892  xp1st  5895  xp2nd  5896  releldm2  5914  reldm  5915  sbcopeq1a  5916  csbopeq1a  5917  dfoprab3  5920  eloprabi  5925  mpt2mptsx  5926  dmmpt2ssx  5928  fmpt2x  5929  mpt2fvex  5932  mpt2exxg  5936  fmpt2co  5940  df1st2  5943  df2nd2  5944  1stconst  5945  2ndconst  5946  dfmpt2  5947  fo2ndf  5951  f1o2ndf1  5952  xporderlem  5955  cnvoprab  5958  f1od2  5959  brtpos2  5972  reldmtpos  5974  dmtpos  5977  rntpos  5978  ovtposg  5980  dftpos3  5983  dftpos4  5984  tpostpos  5985  tpossym  5997  tfrlem3  6032  tfrlem5  6035  tfrlem8  6039  tfrlemisucfn  6045  tfrlemisucaccv  6046  tfrlemibxssdm  6048  tfrlemibfn  6049  tfrlemibex  6050  tfrlemi14d  6054  tfrexlem  6055  tfr1onlem3  6059  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemres  6083  tfrcl  6085  rdgtfr  6095  rdgruledefgg  6096  rdgivallem  6102  rdgon  6107  rdg0g  6109  frec0g  6118  frecabex  6119  frecabcl  6120  frectfr  6121  freccllem  6123  frecfcllem  6125  frecsuclem  6127  frecrdg  6129  oafnex  6161  sucinc  6162  fnoa  6164  oaexg  6165  omfnex  6166  fnom  6167  omexg  6168  fnoei  6169  oeiexg  6170  oeiv  6173  oacl  6177  omcl  6178  oeicl  6179  oav2  6180  nnsucelsuc  6208  nnsucuniel  6212  ercnv  6267  iserd  6272  eqerlem  6277  eqer  6278  ecdmn0m  6288  erth  6290  qsss  6305  ecid  6309  ecidg  6310  qsid  6311  iinerm  6318  qsel  6323  erovlem  6338  ecopovsym  6342  ecopover  6344  th3qlem2  6349  mapprc  6363  fnmap  6366  fnpm  6367  mapdm0  6374  mapval2  6389  mapsn  6401  mapsncnv  6406  mapsnf1o2  6407  bren  6418  brdomg  6419  domen  6422  domeng  6423  ctex  6424  idssen  6448  ener  6450  domtr  6456  ensn1g  6468  en1  6470  en1bg  6471  fundmen  6477  fundmeng  6478  mapsnen  6482  fiprc  6486  unen  6487  xpsnen  6491  xpsneng  6492  xpcomco  6496  xpcomeng  6498  xpassen  6500  xpdom2  6501  xpdom2g  6502  xpf1o  6514  mapen  6516  mapxpen  6518  xpmapenlem  6519  ssenen  6521  phplem4  6525  phplem3g  6526  nneneq  6527  php5  6528  phpm  6535  findcard  6558  findcard2  6559  findcard2s  6560  isinfinf  6567  ac6sfi  6568  exmidpw  6578  unfidisj  6586  xpfi  6593  fisseneq  6595  ssfirab  6596  snexxph  6611  sbthlemi10  6622  isbth  6623  cnvinfex  6660  eqinfti  6662  infvalti  6664  infglbti  6667  infmoti  6670  ordiso2  6675  djuf1olem  6692  djuun  6707  djuss  6708  finomni  6743  exmidomniim  6744  exmidomni  6745  fodjuomnilemdc  6746  pm54.43  6765  exmidfodomrlemim  6774  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  indpi  6848  dfplpq2  6860  enq0sym  6938  enq0ref  6939  enq0tr  6940  nqnq0pi  6944  nqnq0  6947  mulnnnq0  6956  nqprm  7048  nqprrnd  7049  nqprdisj  7050  nqprloc  7051  nqprl  7057  nqpru  7058  addnqprlemrl  7063  addnqprlemru  7064  addnqprlemfl  7065  addnqprlemfu  7066  mulnqprlemrl  7079  mulnqprlemru  7080  mulnqprlemfl  7081  mulnqprlemfu  7082  ltnqpr  7099  ltnqpri  7100  archpr  7149  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlem2  7166  caucvgprlemladdfu  7183  caucvgprlem2  7186  caucvgprprlemopu  7205  ltresr  7323  peano1nnnn  7336  peano2nnnn  7337  axcnre  7363  axpre-apti  7367  renfdisj  7493  dfinfre  8355  1nn  8371  peano2nn  8372  indstr  9016  cnref1o  9068  ioof  9324  fzpr  9424  frec2uzrand  9743  frec2uzf1od  9744  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  frecfzennn  9764  serile  9855  ibcval5  10071  hashinfom  10086  hashunlem  10112  hashun  10113  hashxp  10134  hashfacen  10141  zfz1isolem1  10145  zfz1iso  10146  shftfvalg  10152  ovshftex  10153  shftfibg  10154  shftfval  10155  shftfib  10157  shftfn  10158  2shfti  10165  shftvalg  10170  shftval4g  10171  rexfiuz  10321  maxabslemval  10540  fimaxre2  10556  fclim  10580  climshft  10590  zisum  10668  fisum  10670  qredeu  10985  isprm2  11005  prmind2  11008  bdcvv  11217  bdsnss  11233  bdop  11235  bj-vprc  11256  bdinex1g  11261  bdssexg  11264  bj-inex  11267  bj-zfpair2  11270  bj-uniexg  11278  bdunexb  11280  bj-unexg  11281  bj-indint  11295  bj-ssom  11300  bj-om  11301  bj-2inf  11302  bj-bdfindis  11311  bj-nn0suc0  11314  bj-nnelirr  11317  bj-inf2vnlem1  11334  bj-inf2vnlem2  11335  bj-omex2  11341  bj-nn0sucALT  11342  bj-findis  11343  ss1oel2o  11357  nninfsellemeq  11375  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator