Theorem visset 1813

Description: All set variables are sets (see isset 1814). Theorem 6.8 of [Quine] p. 43.

Assertion

Ref	Expression
visset	|- x e. V

Proof of Theorem visset

Step	Hyp	Ref	Expression
1		eqid 1475	. 2 |- x = x
2		df-v 1812	. . 3 |- V = {x | x = x}
3	2	abeq2i 1570	. 2 |- (x e. V <-> x = x)
4	1, 3	mpbir 190	1 |- x e. V

Syntax hints:   = wceq 956   e. wcel 958  Vcvv 1811

This theorem is referenced by:  isset 1814  ralv 1820  rexv 1821  rabab 1822  eqvinc 1883  ceqex 1886  cbvab 1908  moeq3 1921  mo2icl 1923  moi2 1924  moi 1925  reu8 1936  sbhypf 1939  sbhyp 1940  sbc2or 1958  sbccomg 1989  sbcralt 1990  sbcralgf 1992  sbcel12g 2011  sbceqdig 2012  csbvarg 2021  csbiegft 2029  csbnestg 2036  csbabg 2043  uniiunlem 2132  ddif 2169  dfun2 2243  dfin2 2244  difab 2269  eqv 2295  elpwg 2405  hbpw 2407  hbpr 2426  ralpr 2428  dftp2 2440  snssg 2463  difprsn 2465  prss 2471  prssg 2472  tpss 2476  prsspw 2480  pwv 2502  unipr 2515  uniprg 2516  unisng 2518  elintg 2541  elinti 2542  hbint 2543  elintrabg 2546  intss1 2548  ssint 2549  intmin 2553  intss 2554  intssuni 2555  intmin4 2559  intab 2560  intun 2562  intpr 2563  iuniin 2573  dfiun2g 2586  dfiin2 2588  ssiin 2599  iinss 2600  0iin 2606  iinun2 2609  iundif2 2610  iindif2 2611  iinuni 2615  iinpw 2617  iunpwss 2618  brab1 2660  sbcbrg 2662  dftr4 2685  nalset 2712  nvelv 2713  inex1g 2718  ssexg 2721  intex 2729  pwexg 2746  abssexg 2747  snex 2750  el 2751  rext 2754  sspwb 2755  unipw 2756  pwuni 2757  ssextss 2762  nnullss 2768  exss 2769  axpr 2778  zfpair2 2780  opthg 2788  opthgg 2789  eqvinop 2791  copsexg 2792  copsex4g 2794  opprc1b 2796  opth2 2800  moop2 2801  opabid 2810  pwin 2825  pwunss 2826  pwssun 2827  pwundif 2828  epel 2834  dfid3 2836  uniexg 2871  unexb 2873  opeluu 2879  uniuni 2880  euuni 2881  reucl 2885  reuunisn 2895  iunpw 2914  dffr2 2919  frirr 2924  fr2nr 2925  fr3nr 2926  wefrc 2943  onfr 2986  ordon 2987  ssorduni 2993  onint 3006  onminex 3020  hbsuc 3040  sucel 3042  sucidg 3052  ordpwsuc 3066  unon 3088  ordunisuc 3089  onuninsuc 3108  orduninsuc 3114  onzsl 3117  limsssuc 3121  limuni3 3123  dfom2 3133  elomg 3135  omsson 3136  limomss 3137  ordom 3141  peano5 3153  finds 3156  findsg 3157  finds2 3158  findes 3160  tfinds 3161  tfindsg 3162  tfindsg2 3163  tfindes 3164  tfinds2 3165  opelxp1 3205  opelxp 3214  opelxpg 3216  ralxp 3218  ralxpf 3220  elxp3 3224  elvv 3228  optocl 3235  onxpdisj 3241  ssxp 3256  xpsspw 3257  relopab 3266  opabid2 3267  inxp 3269  relop 3275  ididg 3278  opelcog 3290  cnvco 3300  dfrn2 3303  dfdm4 3305  eldm2g 3309  dmss 3310  breldmg 3316  dmun 3317  dmin 3318  dmuni 3319  dmsnsn0 3325  dmi 3326  dmsnop 3328  reldm0 3331  elreldm 3338  hbrn 3351  dmrnssfld 3357  dmcoss 3363  dmcosseq 3365  opelresg 3374  resieq 3376  dmres 3380  relssres 3392  resopab 3395  resiexg 3396  iss 3397  dfima2 3405  hbima 3411  csbima12g 3413  imadmrn 3414  imai 3417  elimasng 3427  args 3428  eliniseg 3429  iniseg 3430  dffr3 3431  intasym 3438  asymref 3439  asymref2 3440  intirr 3441  cnvopab 3445  cnv0 3446  cnvi 3447  cnvsn 3449  elxp4 3453  elxp5 3454  cnvun 3455  cnvin 3456  rnuni 3459  dminss 3462  imainss 3463  cnvxp 3464  xpnz 3466  ssrnres 3481  rninxp 3482  dminxp 3483  dfrel2 3485  cores 3499  resco 3500  imaco 3501  rnco 3502  co02 3508  coi1 3510  coass 3512  relssdr 3513  cnvpo 3522  cnvso 3523  dffun2 3526  dffun6 3539  dffun7 3540  dffun8 3541  funsn 3543  funopg 3547  funco 3550  funssres 3552  funun 3554  funcnv2 3556  funcnv 3557  funcnv3 3558  fun2cnv 3559  fncnv 3561  funcnvuni 3564  imadif 3574  isarep1 3577  fneu 3592  2elresin 3598  fn0 3605  zfrep6 3614  fcoi1 3645  fcoi2 3646  feu 3647  fcnvres 3648  fabexg 3653  fconst 3658  fconstg 3659  f11 3664  fvprc 3721  fvex 3732  fv3 3733  tz6.12f 3738  tz6.12-2 3739  csbfv12g 3742  ndmfv 3745  funbrfv 3750  funopfvg 3752  fnbrfvb 3753  funbrfvbg 3757  fnopabfv 3758  fnrnfv 3759  dfimafn 3761  funimass4 3763  fvelima 3764  fnsnfv 3767  ssimaexg 3769  dmfco 3773  fvco 3774  fvopab4gf 3781  fvopabg 3785  fvopabn 3786  fvopabgf 3787  fvopabnf 3788  fvopab2 3791  eqfnfv 3797  funfvop 3803  fvelrn 3812  dff2 3817  dff3 3818  dffo4 3820  exfo 3822  fopabcos 3833  fsn 3834  fnressn 3837  fressnfv 3838  fvi 3842  funfvima3 3854  fvclss 3855  fvresex 3857  abrexexlem2 3859  abrexex 3860  abrexexg 3861  imaiun 3864  funiunfv 3866  abexssex 3872  f1fv 3874  f1ofveu 3882  cbvfo 3885  isomin 3899  isoini 3900  isofrlem 3901  f1oweALT 3906  tfrlem2 3912  tfrlem3 3913  tfrlem8 3918  tfrlem9 3919  tfrlem10 3920  tfrlem11 3921  tz7.44lem1 3927  rdg0t 3944  rdglim2 3949  tz7.48-1 3956  abianfplem 3961  csboprg 3986  eloprabg 4007  resoprab 4009  oprabval2gf 4026  oprabval5 4029  oprssdm 4042  caoprmo 4070  op1stg 4087  op2ndg 4088  1stval2 4089  2ndval2 4090  fo1st 4091  fo2nd 4092  f1stres 4093  f2ndres 4094  1st2val 4095  2nd2val 4096  2ndconst 4097  curry1 4098  sbcopeq1a 4111  csbopeq1a 4112  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  dfoprab4 4116  df1st2 4126  df2nd2 4127  oacl 4170  omcl 4171  oecl 4172  oa0r 4173  om0r 4174  om1r 4177  oe1m 4179  oaordi 4180  oawordri 4184  oawordeulem 4188  oalimcl 4194  oaass 4195  oarec 4196  omordi 4197  omwordri 4203  omlimcl 4209  odi 4210  omass 4211  oen0 4213  oeordi 4214  oewordri 4219  oeworde 4220  oaabs 4252  omsmolem 4256  ider 4269  eqerlem 4270  erref 4275  erdmrn 4276  ecdmn0 4280  erthi 4281  erth 4282  erdisj 4286  elqsi 4291  0nelqs 4298  ecid 4300  qsid 4301  brecop 4306  ecopoprdm 4309  ecopoprsym 4310  ecopoprtrn 4311  ecopoprer 4312  th3qlem1 4314  mapprc 4326  fnmap 4329  mapvalg 4330  pmvalg 4331  mapval2 4335  map0 4344  mapsn 4345  ixpconst 4352  ss2ixp 4354  ixp0 4361  mapixp 4362  breng 4375  brdomg 4376  domen 4379  domeng 4380  idssen 4406  ener 4410  ensymg 4411  entrt 4414  domtr 4415  ensn1g 4425  en1 4426  fundmen 4428  mapsnen 4429  unen 4434  xpsnen 4435  xpsneng 4436  xpcomen 4439  xpcomeng 4440  xpassen 4441  xpdom2 4442  xpdom1g 4444  xpdom3 4445  pw2en 4446  sbth 4457  sbthcl 4459  fodomr 4483  canth2 4484  canth2g 4485  mapenlem1 4489  mapenlem2 4490  mapdom1 4492  mapdom2lem 4493  mapdom2 4494  mapunen 4502  pwen 4503  ssenen 4504  nneneq 4512  php 4513  php2 4514  php3 4515  php3OLD 4516  0sdom1dom 4525  ominfOLD 4529  pssnn 4534  ssfi 4537  ssfiOLD 4538  domfiOLD 4539  unbnn2 4545  isfinite2OLD 4546  infcntss 4554  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii2OLD 4562  abfii3OLD 4563  abfii4OLD 4564  fodomfiOLD 4566  pwfilemOLD 4570  pwfiOLD 4571  pm54.43 4572  suppr 4590  elirrv 4598  zfregfr 4601  en2lp 4602  inf0 4606  inf3lema 4609  inf3lemd 4612  inf3lem1 4613  inf3lem2 4614  inf3lem3 4615  inf3lem5 4617  inf3lem6 4618  inf3lem7 4619  inf3 4620  infeq5 4621  omex 4627  dfom3 4630  infensuc 4638  unbnnt 4639  zfregs 4647  setind2 4649  r1tr 4654  r1ord 4655  r1val1 4658  tz9.12lem1 4659  tz9.12lem3 4661  tz9.13 4663  tz9.13g 4664  rankwflem 4665  jech9.3 4666  rankvalg 4669  rankr1 4674  rankr1g 4675  r1val2 4678  rankval3 4681  bndrank 4682  ranklim 4685  r1pw 4686  r1pwcl 4687  rankuni2 4690  rankun 4691  rankonid 4695  rankr1id 4697  rankuni 4698  rankval4 4702  rankxplim 4712  rankxplim3 4714  rankxpsuc 4715  cp 4722  bnd2 4724  kardex 4725  karden 4726  aceq3lem 4732  aceq3 4733  aceq4 4734  aceq5lem1 4735  aceq5lem2 4736  aceq5lem3 4737  aceq5lem4 4738  aceq5lem5 4739  aceq5 4740  aceq6a 4741  aceq6b 4742  ac6lem 4754  ac6s 4756  ac9s 4764  kmlem1 4765  kmlem2 4766  kmlem4 4768  kmlem9 4773  kmlem10 4774  kmlem11 4775  kmlem12 4776  kmlem13 4777  numthlem 4783  numth2 4785  numthcor 4786  zorn2lem1 4788  zorn2lem7 4794  zornlem 4795  fodom 4798  fodomg 4799  brdom3 4801  brdom5 4802  brdom4 4803  brdom7disj 4804  brdom6disj 4805  unidomg 4809  cardval 4826  unxpdomlem 4843  unxpdom 4844  sucxpdom 4846  cardlim 4851  iscard2 4854  ondomon 4856  ondomcard 4857  carduni 4858  cardiun 4859  cardmin 4860  alephon 4865  alephcard 4867  alephordi 4874  cardaleph 4885  alephval2 4902  alephval3 4903  dominf 4904  cffnon 4907  cflim 4909  cardcf 4911  cfeq0 4914  cfsuc 4915  cfom 4916  cdavalt 4919  ltpiord 5015  indpi 5034  dmenq 5045  enqer 5046  addcmpblnq 5052  mulcmpblnq 5053  addpipq 5054  mulpipq 5055  ordpipq 5056  addcompq 5062  addasspq 5063  mulcompq 5064  mulasspq 5065  distrpqlem 5066  distrpq 5067  mulidpq 5069  recmulpq 5070  ltsopq 5075  ltapq 5076  ltmpq 5077  ltexpq 5080  ltexpq2 5081  halfpq 5082  nsmallpq 5083  ltbtwnpq 5084  ltrpq 5085  prnmadd 5100  genpv 5102  genpdm 5105  genpnnp 5108  genpcd 5109  genpnmax 5110  genpcl 5111  genpass 5112  1pr 5117  addclprlem1 5118  addclprlem2 5119  addclpr 5120  mulclprlem 5121  mulclpr 5122  addcompr 5123  addasspr 5124  mulcompr 5125  mulasspr 5126  distrlem1pr 5127  distrlem2pr 5128  distrlem4pr 5130  distrlem5pr 5131  1idpr 5133  prlem934a 5137  prlem934b 5138  prlem934 5139  ltaddpr 5140  ltexprlem1 5142  ltexprlem2 5143  ltexprlem3 5144  ltexprlem4 5145  ltexprlem6 5147  ltexprlem7 5148  ltexpri 5149  ltaprlem 5150  prlem936a 5153  prlem936 5155  reclem1pr 5156  reclem2pr 5157  reclem3pr 5158  reclem4pr 5159  recexpr 5160  suplem1pr 5161  suplem2pr 5162  dmenr 5175  enrer 5176  addcmpblnr 5181  mulcmpblnrlem 5182  addsrpr 5184  mulsrpr 5185  ltsrpr 5186  addcomsr 5196  addasssr 5197  mulcomsr 5198  mulasssr 5199  distrsr 5200  ltsosr 5203  0idsr 5206  1idsr 5207  ltasr 5209  recexsrlem 5212  mulgt0sr 5214  sqgt0sr 5215  recexsr 5216  map2psrpr 5220  suppsrlem 5221  suppsr 5222  suppsr2 5223  suppsr3 5224  supsrlem2 5226  supsrlem3 5227  supsrlem6 5230  ltresr 5258  supre 5260  ltsor 5261  axmulrcl 5274  axaddcom 5275  axmulcom 5276  axaddass 5277  axmulass 5278  axdistr 5279  axrrecex 5284  axcnre 5286  pre-axltadd 5289  pre-axmulgt0 5290  csbnegg 5364  ssxr 5540  peano2nn 5935  lbinfm 6048  dfinfmr 6067  infmsup 6068  infmxrcl 6086  dfuz 6202  ser1ft 6328  uzind4s 6452  dfseq0 6563  sumex 6981  dffsum 6998  fsum1f 7007  fsum1slem 7008  fsump1f 7011  csbfsum 7027  climfnn 7092  climeu 7100  climreu 7101  climmulc2 7129  iserzext 7135  caucvg3lem 7166  isumclimtf 7195  isumclim2tf 7198  isumshft 7204  isumshft2 7205  isumclt 7209  isumreclt 7210  isummulc1ALT 7213  infcvglem1 7221  fsum0diaglem2 7257  fsum0diag2 7259  efseq0ex 7311  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  xpnnen 7499  infxpidmlem1 7552  infxpidmlem4 7555  infxpidmlem5 7556  infxpidmlem7 7558  infxpidmlem8 7559  infxpidmlem9 7560  infxpidmlem10 7561  infxpidmlem11 7562  infxpidmlem12 7563  infpss 7574  unictb 7576  unctb 7577  infmap2lem1 7579  infmap2lem2 7580  infmap2 7581  tgval2t 7617  tgval3t 7625  eltg3t 7626  tgss3t 7638  basgent 7640  subbasOLD 7644  subbas2OLD 7645  subtop 7646  sn0top 7647  indistop 7648  distop 7649  fctopOLD 7650  cctop 7652  ntrfval 7667  clsfval 7668  ntrval 7676  clsval 7677  clsval2 7685  neifval 7714  neif 7715  neival 7717  lpfval 7742  lpval 7743  islp2 7747  cncnplem2 7775  dfms2 7799  lmfval 7925  iscau 7936  iscaunns 7944  metcls 7966  metcld 7967  bopcnlem1 7981  bopcnlem3 7983  iscms2lem4 7992  cmsss 7997  cncms 7998  bcthlem13 8011  bcthlem32 8030  issubg 8116  nvvcop 8213  0vfval 8225  vsfval 8254  sqcn 8335  ipfval 8352  nmoubi 8435  ubthlem3 8531  ubthlem4 8532  minveclem10 8554  minveclem14 8558  psdmrn 8648  spwval2 8653  spwpr2 8658  spwpr3OLD 8662  circgrp 8740  axgroth2 8778  axgroth3 8779  grothprim 8783  axhcompl 8868  hhcmpl 9069  hhcms 9072  hlimreu 9110  hlimeu 9111  chcmh 9113  helch 9116  hsn0elch 9120  hhsscms 9150  occl 9181  projlem25 9210  projlem 9217  chintcl 9295  dfchj3 9325  spanun 9467  spansn 9480  osumlem4 9581  osumlem6 9583  osumlem7 9584  pjrn 9647  nmopubt 9832  nmfnleubt 9849  nmopunt 9939  nmcopexlem1 9951  nmcfnexlem1 9980  nlelch 9994  cnlnssadj 10013  adjbd1o 10018  branmfnt 10038  bra11 10041  pjnmop 10075  hmopidmch 10079  pjhmopidm 10110  ghomgrplem 10389  symggrp 10408  cayleythlem 10413  ntunte 10439  uninqs 10441  elo 10444  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  abfi 10451  abfiOLD 10452  stcat 10457  ficli 10472  ficliOLD 10473  fiv 10482  fivOLD 10483  mapudiscn 10512  hmphsyma 10528  hmpher 10536  hmeogrp 10538  homcard 10539  eqindhome 10541  subsp 10554  qusp 10555  oefil2 10567  fgsb 10570  fgsbOLD 10571  infi 10578  infiOLD 10579  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605  dtopcl 10615  dtt2 10618  eloi 10659  ishomd 10718  blkssatm 10767

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain