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

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

Proof of Theorem vex
StepHypRef Expression
1 equid 1630 . 2 𝑥 = 𝑥
2 df-v 2604 . . 3 V = {𝑥𝑥 = 𝑥}
32abeq2i 2190 . 2 (𝑥 ∈ V ↔ 𝑥 = 𝑥)
41, 3mpbir 144 1 𝑥 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1434  Vcvv 2602
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 2064
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604
This theorem is referenced by:  isset  2606  eqvisset  2610  ralv  2617  rexv  2618  reuv  2619  rmov  2620  rabab  2621  sbhypf  2649  ceqex  2723  ralab  2753  rexab  2755  mo2icl  2772  reu8  2789  csbvarg  2934  csbiebg  2946  sbcnestgf  2954  sbnfc2  2963  ddifnel  3104  ddifstab  3105  csbing  3174  unssdif  3200  unssin  3204  inssun  3205  invdif  3207  vn0  3259  vn0m  3260  eqv  3268  abvor0dc  3270  sbss  3351  selpw  3391  elpwg  3392  velsn  3417  vsnid  3428  exsnrex  3437  dftp2  3443  prmg  3513  prnzg  3516  snssg  3524  difprsnss  3526  sneqrg  3556  preq12bg  3567  pwprss  3599  pwtpss  3600  pwv  3602  unipr  3617  uniprg  3618  unisng  3620  elintg  3646  elintrabg  3651  intss1  3653  ssint  3654  intmin  3658  intss  3659  intssunim  3660  intmin4  3666  intab  3667  intun  3669  intpr  3670  intprg  3671  uniintsnr  3674  iinconstm  3689  iuniin  3690  iinss1  3692  dfiin2g  3713  dfiunv2  3716  ssiinf  3729  iinss  3731  iinss2  3732  0iin  3738  iinab  3741  iundif2ss  3745  iindif2m  3747  iinin2m  3748  iinuniss  3760  sspwuni  3762  iinpw  3765  iunpwss  3766  brab1  3832  csbopabg  3858  mptv  3876  trint  3892  trintssmOLD  3894  vprc  3911  inex1g  3916  ssexg  3919  inteximm  3926  inuni  3932  repizf2  3938  axpweq  3947  bnd2  3949  pwexg  3956  pwuni  3965  zfpair2  3967  rext  3972  sspwb  3973  unipw  3974  ssextss  3977  euabex  3982  mss  3983  exss  3984  opth  3994  opthg  3995  copsexg  4001  copsex4g  4004  moop2  4008  euotd  4011  opabid  4014  elopab  4015  opelopabsbALT  4016  opelopabsb  4017  opabm  4037  pwin  4039  pwunss  4040  epelg  4047  epel  4049  pofun  4069  epse  4099  tron  4139  sucel  4167  suctr  4178  uniexg  4195  unexb  4197  snnex  4201  uniuni  4203  eusvnf  4205  eusvnfb  4206  iunpw  4231  unon  4257  ordunisuc2r  4260  ordtri2or2exmidlem  4271  onsucelsucexmidlem  4274  ordsucunielexmid  4276  elirr  4286  en2lp  4299  dtruex  4304  onintexmid  4317  reg3exmidlemwe  4323  finds  4343  finds2  4344  elnn  4348  limom  4356  0nelxp  4392  opelxp  4394  opeliunxp  4415  elvv  4422  elvvv  4423  elvvuni  4424  xpsspw  4472  relopabi  4485  opabid2  4489  difopab  4491  xpiindim  4495  raliunxp  4499  rexiunxp  4500  ralxpf  4504  rexxpf  4505  relop  4508  cnvco  4542  dfrn2  4545  dfdm4  4549  dmss  4556  dmin  4565  dmiun  4566  dmuni  4567  dm0  4571  dmi  4572  reldm0  4575  elreldm  4582  elrnmpt1  4607  dmrnssfld  4617  dmcoss  4623  dmcosseq  4625  opelresg  4641  resieq  4644  dmres  4654  elres  4668  relssres  4670  resopab  4676  resiexg  4677  iss  4678  dfres2  4682  dfima2  4694  imadmrn  4702  imai  4705  csbima12g  4710  elimasng  4717  args  4718  epini  4720  iniseg  4721  dfse2  4722  exse2  4723  cotr  4730  issref  4731  cnvsym  4732  intasym  4733  asymref  4734  intirr  4735  brcodir  4736  codir  4737  qfto  4738  poirr2  4741  cnvopab  4750  cnv0  4751  cnvi  4752  cnvdif  4754  rniun  4758  dminss  4762  imainss  4763  inimasn  4765  xpmlem  4768  dmxpss  4777  rnxpid  4779  ssrnres  4787  rninxp  4788  dminxp  4789  cnvcnv3  4794  dfrel2  4795  dmsnm  4810  dmsnopg  4816  cnvcnvsn  4821  dmsnsnsng  4822  cnvsng  4830  elxp4  4832  elxp5  4833  cnvresima  4834  dfco2  4844  dfco2a  4845  cores  4848  resco  4849  imaco  4850  rnco  4851  coiun  4854  co02  4858  coi1  4860  coass  4863  relssdmrn  4865  unielrel  4869  ressn  4882  cnviinm  4883  cnvpom  4884  cnvsom  4885  uniabio  4901  iotaval  4902  iotass  4908  sniota  4918  csbiotag  4919  dffun2  4936  dffun7  4952  dffun8  4953  dffun9  4954  funopg  4958  funssres  4966  funun  4968  funcnvsn  4969  funinsn  4973  funcnv2  4984  funcnv  4985  funcnv3  4986  funcnveq  4987  fun2cnv  4988  funcnvuni  4993  imadif  5004  funimaexglem  5007  isarep1  5010  2elresin  5035  fnres  5040  fcnvres  5098  fconstg  5108  fun11iun  5172  f1osng  5192  dffv3g  5199  fvssunirng  5215  sefvex  5221  fv3  5223  fvres  5224  nfunsn  5233  funimass4  5250  ssimaexg  5261  dmfco  5267  fvopab6  5290  fndmdif  5298  fvelrn  5324  dffo4  5341  f1ompt  5346  fmptco  5356  fsn  5361  fsng  5362  dfmpt  5366  dfmptg  5368  fnressn  5375  fressnfv  5376  fvsng  5385  resfunexg  5408  funfvima3  5418  idref  5422  abrexco  5424  imaiun  5425  dff13  5433  foeqcnvco  5455  f1eqcocnv  5456  fliftcnv  5460  isocnv2  5477  isoini  5482  isose  5485  riotav  5498  csbriotag  5505  acexmidlem2  5534  oprabid  5562  csbov123g  5568  0neqopab  5575  brabvv  5576  dfoprab2  5577  rnoprab  5612  eloprabga  5616  mpt2v  5619  f1opw  5732  opabex3d  5773  opabex3  5774  ofmres  5788  op1stg  5802  op2ndg  5803  1stval2  5807  2ndval2  5808  fo1st  5809  fo2nd  5810  f1stres  5811  f2ndres  5812  fo1stresm  5813  fo2ndresm  5814  xp1st  5817  xp2nd  5818  releldm2  5836  reldm  5837  sbcopeq1a  5838  csbopeq1a  5839  dfoprab3  5842  eloprabi  5847  mpt2mptsx  5848  dmmpt2ssx  5850  fmpt2x  5851  mpt2fvex  5854  mpt2exxg  5858  fmpt2co  5862  df1st2  5865  df2nd2  5866  1stconst  5867  2ndconst  5868  dfmpt2  5869  fo2ndf  5873  f1o2ndf1  5874  xporderlem  5877  cnvoprab  5880  f1od2  5881  brtpos2  5894  reldmtpos  5896  dmtpos  5899  rntpos  5900  ovtposg  5902  dftpos3  5905  dftpos4  5906  tpostpos  5907  tpossym  5919  tfrlem3  5954  tfrlem5  5957  tfrlem8  5961  tfrlemisucfn  5967  tfrlemisucaccv  5968  tfrlemibxssdm  5970  tfrlemibfn  5971  tfrlemibex  5972  tfrlemi14d  5976  tfrexlem  5977  tfr1onlem3  5981  tfr1onlemsucaccv  5984  tfr1onlembxssdm  5986  tfr1onlembfn  5987  tfr1onlemres  5992  tfri1dALT  5994  tfrcllemsucaccv  5997  tfrcllembxssdm  5999  tfrcllembfn  6000  tfrcllemres  6005  tfrcl  6007  rdgtfr  6017  rdgruledefgg  6018  rdgivallem  6024  rdgon  6029  rdg0g  6031  frec0g  6040  frecabex  6041  frecabcl  6042  frectfr  6043  freccllem  6045  frecfcllem  6047  frecsuclem  6049  frecrdg  6051  oafnex  6082  sucinc  6083  fnoa  6085  oaexg  6086  omfnex  6087  fnom  6088  omexg  6089  fnoei  6090  oeiexg  6091  oeiv  6094  oacl  6098  omcl  6099  oeicl  6100  oav2  6101  nnsucelsuc  6128  nnsucuniel  6132  ercnv  6186  iserd  6191  eqerlem  6196  eqer  6197  ecdmn0m  6207  erth  6209  qsss  6224  ecid  6228  ecidg  6229  qsid  6230  iinerm  6237  qsel  6242  erovlem  6257  ecopovsym  6261  ecopover  6263  th3qlem2  6268  bren  6287  brdomg  6288  domen  6291  domeng  6292  idssen  6316  ener  6318  domtr  6324  ensn1g  6336  en1  6338  en1bg  6339  fundmen  6345  fundmeng  6346  fiprc  6351  unen  6352  xpsnen  6355  xpsneng  6356  xpcomco  6360  xpcomeng  6362  xpassen  6364  xpdom2  6365  xpdom2g  6366  xpf1o  6375  phplem4  6380  phplem3g  6381  nneneq  6382  php5  6383  phpm  6390  findcard  6412  findcard2  6413  findcard2s  6414  ac6sfi  6421  unfidisj  6432  cnvinfex  6480  eqinfti  6482  infvalti  6484  infglbti  6487  infmoti  6490  ordiso2  6495  pm54.43  6508  indpi  6583  dfplpq2  6595  enq0sym  6673  enq0ref  6674  enq0tr  6675  nqnq0pi  6679  nqnq0  6682  mulnnnq0  6691  nqprm  6783  nqprrnd  6784  nqprdisj  6785  nqprloc  6786  nqprl  6792  nqpru  6793  addnqprlemrl  6798  addnqprlemru  6799  addnqprlemfl  6800  addnqprlemfu  6801  mulnqprlemrl  6814  mulnqprlemru  6815  mulnqprlemfl  6816  mulnqprlemfu  6817  ltnqpr  6834  ltnqpri  6835  archpr  6884  cauappcvgprlemladdfu  6895  cauappcvgprlemladdfl  6896  cauappcvgprlem2  6901  caucvgprlemladdfu  6918  caucvgprlem2  6921  caucvgprprlemopu  6940  ltresr  7058  peano1nnnn  7071  peano2nnnn  7072  axcnre  7098  axpre-apti  7102  renfdisj  7228  dfinfre  8090  1nn  8106  peano2nn  8107  indstr  8751  cnref1o  8803  ioof  9059  fzpr  9159  frec2uzrand  9476  frec2uzf1od  9477  frecuzrdgtcl  9483  frecuzrdgfunlem  9490  frecfzennn  9497  serile  9560  ibcval5  9776  sizeinf  9791  sizeunlem  9817  sizeun  9818  shftfvalg  9833  ovshftex  9834  shftfibg  9835  shftfval  9836  shftfib  9838  shftfn  9839  2shfti  9846  shftvalg  9851  shftval4g  9852  rexfiuz  10002  maxabslemval  10221  fimaxre2  10236  fclim  10260  climshft  10270  qredeu  10612  isprm2  10632  prmind2  10635  bdcvv  10791  bdsnss  10807  bdop  10809  bj-vprc  10830  bdinex1g  10835  bdssexg  10838  bj-inex  10841  bj-zfpair2  10844  bj-uniexg  10852  bdunexb  10854  bj-unexg  10855  bj-indint  10869  bj-ssom  10874  bj-om  10875  bj-2inf  10876  bj-bdfindis  10885  bj-nn0suc0  10888  bj-nnelirr  10891  bj-inf2vnlem1  10908  bj-inf2vnlem2  10909  bj-omex2  10915  bj-nn0sucALT  10916  bj-findis  10917
  Copyright terms: Public domain W3C validator