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

Theorem vex 2613
Description: All setvar variables are sets (see isset 2614). 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 1630 . 2  |-  x  =  x
2 df-v 2612 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2193 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 144 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   _Vcvv 2610
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-v 2612
This theorem is referenced by:  isset  2614  eqvisset  2618  ralv  2625  rexv  2626  reuv  2627  rmov  2628  rabab  2629  sbhypf  2657  ceqex  2730  ralab  2761  rexab  2763  mo2icl  2780  reu8  2797  csbvarg  2942  csbiebg  2954  sbcnestgf  2962  sbnfc2  2971  ddifnel  3113  ddifstab  3114  csbing  3189  unssdif  3215  unssin  3219  inssun  3220  invdif  3222  vn0  3274  vn0m  3275  eqv  3283  abvor0dc  3285  sbss  3366  selpw  3407  elpwg  3408  velsn  3433  vsnid  3444  exsnrex  3453  dftp2  3459  prmg  3529  prnzg  3532  snssg  3541  difprsnss  3543  sneqrg  3574  preq12bg  3585  pwprss  3617  pwtpss  3618  pwv  3620  unipr  3635  uniprg  3636  unisng  3638  elintg  3664  elintrabg  3669  intss1  3671  ssint  3672  intmin  3676  intss  3677  intssunim  3678  intmin4  3684  intab  3685  intun  3687  intpr  3688  intprg  3689  uniintsnr  3692  iinconstm  3707  iuniin  3708  iinss1  3710  dfiin2g  3731  dfiunv2  3734  ssiinf  3747  iinss  3749  iinss2  3750  0iin  3756  iinab  3759  iundif2ss  3763  iindif2m  3765  iinin2m  3766  iinuniss  3778  sspwuni  3780  iinpw  3783  iunpwss  3784  brab1  3850  csbopabg  3876  mptv  3894  trint  3910  trintssmOLD  3912  vprc  3929  inex1g  3934  ssexg  3937  inteximm  3944  inuni  3950  repizf2  3956  axpweq  3965  bnd2  3967  pwexg  3974  pwuni  3983  exmidundif  3991  zfpair2  3993  rext  3998  sspwb  3999  unipw  4000  ssextss  4003  euabex  4008  mss  4009  exss  4010  opth  4020  opthg  4021  copsexg  4027  copsex4g  4030  moop2  4034  euotd  4037  opabid  4040  elopab  4041  opelopabsbALT  4042  opelopabsb  4043  opabm  4063  pwin  4065  pwunss  4066  epelg  4073  epel  4075  pofun  4095  epse  4125  tron  4165  sucel  4193  suctr  4204  uniexg  4221  unexb  4223  snnex  4227  uniuni  4229  eusvnf  4231  eusvnfb  4232  iunpw  4257  unon  4283  ordunisuc2r  4286  ordtri2or2exmidlem  4297  onsucelsucexmidlem  4300  ordsucunielexmid  4302  elirr  4312  en2lp  4325  dtruex  4330  onintexmid  4343  reg3exmidlemwe  4349  finds  4369  finds2  4370  elnn  4374  limom  4382  0nelxp  4418  opelxp  4420  opeliunxp  4441  elvv  4448  elvvv  4449  elvvuni  4450  xpsspw  4498  relopabi  4511  opabid2  4515  difopab  4517  xpiindim  4521  raliunxp  4525  rexiunxp  4526  ralxpf  4530  rexxpf  4531  relop  4534  cnvco  4568  dfrn2  4571  dfdm4  4575  dmss  4582  dmin  4591  dmiun  4592  dmuni  4593  dm0  4597  dmi  4598  reldm0  4601  elreldm  4608  elrnmpt1  4633  dmrnssfld  4643  dmcoss  4649  dmcosseq  4651  opelresg  4667  resieq  4670  dmres  4680  elres  4694  relssres  4696  resopab  4702  resiexg  4703  iss  4704  dfres2  4708  dfima2  4720  imadmrn  4728  imai  4731  csbima12g  4736  elimasng  4743  args  4744  epini  4746  iniseg  4747  dfse2  4748  exse2  4749  cotr  4756  issref  4757  cnvsym  4758  intasym  4759  asymref  4760  intirr  4761  brcodir  4762  codir  4763  qfto  4764  poirr2  4767  cnvopab  4776  cnv0  4777  cnvi  4778  cnvdif  4780  rniun  4784  dminss  4788  imainss  4789  inimasn  4791  xpmlem  4794  dmxpss  4803  rnxpid  4805  ssrnres  4813  rninxp  4814  dminxp  4815  cnvcnv3  4820  dfrel2  4821  dmsnm  4836  dmsnopg  4842  cnvcnvsn  4847  dmsnsnsng  4848  cnvsng  4856  elxp4  4858  elxp5  4859  cnvresima  4860  dfco2  4870  dfco2a  4871  cores  4874  resco  4875  imaco  4876  rnco  4877  coiun  4880  co02  4884  coi1  4886  coass  4889  relssdmrn  4891  unielrel  4895  ressn  4908  cnviinm  4909  cnvpom  4910  cnvsom  4911  uniabio  4927  iotaval  4928  iotass  4934  sniota  4944  csbiotag  4945  dffun2  4962  dffun7  4978  dffun8  4979  dffun9  4980  funopg  4984  funssres  4992  funun  4994  funcnvsn  4995  funinsn  4999  funcnv2  5010  funcnv  5011  funcnv3  5012  funcnveq  5013  fun2cnv  5014  funcnvuni  5019  imadif  5030  funimaexglem  5033  isarep1  5036  2elresin  5061  fnres  5066  fcnvres  5124  fconstg  5134  fun11iun  5199  f1osng  5219  dffv3g  5226  fvssunirng  5242  sefvex  5248  fv3  5250  fvres  5251  nfunsn  5260  funimass4  5277  ssimaexg  5288  dmfco  5294  fvopab6  5317  fndmdif  5325  fvelrn  5351  dffo4  5368  f1ompt  5373  fmptco  5383  fsn  5388  fsng  5389  dfmpt  5393  dfmptg  5395  fnressn  5402  fressnfv  5403  fvsng  5412  resfunexg  5435  funfvima3  5445  idref  5449  abrexco  5451  imaiun  5452  dff13  5460  foeqcnvco  5482  f1eqcocnv  5483  fliftcnv  5487  isocnv2  5504  isoini  5509  isose  5512  riotav  5525  csbriotag  5532  acexmidlem2  5561  oprabid  5589  csbov123g  5595  0neqopab  5602  brabvv  5603  dfoprab2  5604  rnoprab  5639  eloprabga  5643  mpt2v  5646  f1opw  5759  opabex3d  5800  opabex3  5801  ofmres  5815  op1stg  5829  op2ndg  5830  1stval2  5834  2ndval2  5835  fo1st  5836  fo2nd  5837  f1stres  5838  f2ndres  5839  fo1stresm  5840  fo2ndresm  5841  xp1st  5844  xp2nd  5845  releldm2  5863  reldm  5864  sbcopeq1a  5865  csbopeq1a  5866  dfoprab3  5869  eloprabi  5874  mpt2mptsx  5875  dmmpt2ssx  5877  fmpt2x  5878  mpt2fvex  5881  mpt2exxg  5885  fmpt2co  5889  df1st2  5892  df2nd2  5893  1stconst  5894  2ndconst  5895  dfmpt2  5896  fo2ndf  5900  f1o2ndf1  5901  xporderlem  5904  cnvoprab  5907  f1od2  5908  brtpos2  5921  reldmtpos  5923  dmtpos  5926  rntpos  5927  ovtposg  5929  dftpos3  5932  dftpos4  5933  tpostpos  5934  tpossym  5946  tfrlem3  5981  tfrlem5  5984  tfrlem8  5988  tfrlemisucfn  5994  tfrlemisucaccv  5995  tfrlemibxssdm  5997  tfrlemibfn  5998  tfrlemibex  5999  tfrlemi14d  6003  tfrexlem  6004  tfr1onlem3  6008  tfr1onlemsucaccv  6011  tfr1onlembxssdm  6013  tfr1onlembfn  6014  tfr1onlemres  6019  tfri1dALT  6021  tfrcllemsucaccv  6024  tfrcllembxssdm  6026  tfrcllembfn  6027  tfrcllemres  6032  tfrcl  6034  rdgtfr  6044  rdgruledefgg  6045  rdgivallem  6051  rdgon  6056  rdg0g  6058  frec0g  6067  frecabex  6068  frecabcl  6069  frectfr  6070  freccllem  6072  frecfcllem  6074  frecsuclem  6076  frecrdg  6078  oafnex  6109  sucinc  6110  fnoa  6112  oaexg  6113  omfnex  6114  fnom  6115  omexg  6116  fnoei  6117  oeiexg  6118  oeiv  6121  oacl  6125  omcl  6126  oeicl  6127  oav2  6128  nnsucelsuc  6156  nnsucuniel  6160  ercnv  6215  iserd  6220  eqerlem  6225  eqer  6226  ecdmn0m  6236  erth  6238  qsss  6253  ecid  6257  ecidg  6258  qsid  6259  iinerm  6266  qsel  6271  erovlem  6286  ecopovsym  6290  ecopover  6292  th3qlem2  6297  bren  6316  brdomg  6317  domen  6320  domeng  6321  ctex  6322  idssen  6346  ener  6348  domtr  6354  ensn1g  6366  en1  6368  en1bg  6369  fundmen  6375  fundmeng  6376  fiprc  6382  unen  6383  xpsnen  6387  xpsneng  6388  xpcomco  6392  xpcomeng  6394  xpassen  6396  xpdom2  6397  xpdom2g  6398  xpf1o  6407  phplem4  6412  phplem3g  6413  nneneq  6414  php5  6415  phpm  6422  findcard  6445  findcard2  6446  findcard2s  6447  isinfinf  6454  ac6sfi  6455  unfidisj  6467  xpfi  6473  fisseneq  6475  ssfirab  6476  cnvinfex  6526  eqinfti  6528  infvalti  6530  infglbti  6533  infmoti  6536  ordiso2  6541  djulf1o  6556  djurf1o  6557  inlresf  6558  inrresf  6560  djuss  6564  djuun  6568  pm54.43  6588  indpi  6664  dfplpq2  6676  enq0sym  6754  enq0ref  6755  enq0tr  6756  nqnq0pi  6760  nqnq0  6763  mulnnnq0  6772  nqprm  6864  nqprrnd  6865  nqprdisj  6866  nqprloc  6867  nqprl  6873  nqpru  6874  addnqprlemrl  6879  addnqprlemru  6880  addnqprlemfl  6881  addnqprlemfu  6882  mulnqprlemrl  6895  mulnqprlemru  6896  mulnqprlemfl  6897  mulnqprlemfu  6898  ltnqpr  6915  ltnqpri  6916  archpr  6965  cauappcvgprlemladdfu  6976  cauappcvgprlemladdfl  6977  cauappcvgprlem2  6982  caucvgprlemladdfu  6999  caucvgprlem2  7002  caucvgprprlemopu  7021  ltresr  7139  peano1nnnn  7152  peano2nnnn  7153  axcnre  7179  axpre-apti  7183  renfdisj  7309  dfinfre  8171  1nn  8187  peano2nn  8188  indstr  8832  cnref1o  8884  ioof  9140  fzpr  9240  frec2uzrand  9557  frec2uzf1od  9558  frecuzrdgtcl  9564  frecuzrdgfunlem  9571  frecfzennn  9578  serile  9641  ibcval5  9857  hashinfom  9872  hashunlem  9898  hashun  9899  hashxp  9920  shftfvalg  9925  ovshftex  9926  shftfibg  9927  shftfval  9928  shftfib  9930  shftfn  9931  2shfti  9938  shftvalg  9943  shftval4g  9944  rexfiuz  10094  maxabslemval  10313  fimaxre2  10328  fclim  10352  climshft  10362  qredeu  10704  isprm2  10724  prmind2  10727  bdcvv  10933  bdsnss  10949  bdop  10951  bj-vprc  10972  bdinex1g  10977  bdssexg  10980  bj-inex  10983  bj-zfpair2  10986  bj-uniexg  10994  bdunexb  10996  bj-unexg  10997  bj-indint  11011  bj-ssom  11016  bj-om  11017  bj-2inf  11018  bj-bdfindis  11027  bj-nn0suc0  11030  bj-nnelirr  11033  bj-inf2vnlem1  11050  bj-inf2vnlem2  11051  bj-omex2  11057  bj-nn0sucALT  11058  bj-findis  11059
  Copyright terms: Public domain W3C validator