Theorem visset 1809

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

Assertion

Ref	Expression
visset	|- x e. V

Proof of Theorem visset

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

Syntax hints:   = wceq 954   e. wcel 956  Vcvv 1807

This theorem is referenced by:  isset 1810  ralv 1816  rexv 1817  rabab 1818  eqvinc 1879  ceqex 1882  cbvab 1904  moeq3 1917  mo2icl 1919  moi2 1920  moi 1921  reu8 1932  sbhypf 1935  sbhyp 1936  sbc2or 1954  sbccomg 1985  sbcralt 1986  sbcralgf 1988  sbcel12g 2007  sbceqdig 2008  csbvarg 2017  csbiegft 2025  csbnestg 2032  csbabg 2039  uniiunlem 2128  ddif 2165  dfun2 2239  dfin2 2240  difab 2265  eqv 2291  elpwg 2401  hbpw 2403  hbpr 2422  ralpr 2424  dftp2 2436  snssg 2459  difprsn 2461  prss 2467  prssg 2468  tpss 2472  prsspw 2476  pwv 2497  unipr 2510  uniprg 2511  unisng 2513  elintg 2536  elinti 2537  hbint 2538  elintrabg 2541  intss1 2543  ssint 2544  intmin 2548  intss 2549  intssuni 2550  intmin4 2554  intab 2555  intun 2557  intpr 2558  iuniin 2568  dfiun2g 2581  dfiin2 2583  ssiin 2594  iinss 2595  0iin 2601  iinun2 2604  iundif2 2605  iindif2 2606  iinuni 2610  iinpw 2612  iunpwss 2613  brab1 2655  sbcbrg 2657  dftr4 2680  nalset 2707  nvelv 2708  inex1g 2713  ssexg 2716  intex 2724  pwexg 2741  abssexg 2742  snex 2745  el 2746  rext 2749  sspwb 2750  unipw 2751  pwuni 2752  ssextss 2757  nnullss 2763  exss 2764  axpr 2773  zfpair2 2775  opthg 2783  opthgg 2784  eqvinop 2786  copsexg 2787  copsex4g 2789  opprc1b 2791  opth2 2795  moop2 2796  opabid 2805  pwin 2820  pwunss 2821  pwssun 2822  pwundif 2823  epel 2829  dfid3 2831  uniexg 2866  unexb 2868  opeluu 2874  uniuni 2875  euuni 2876  reucl 2880  reuunisn 2890  iunpw 2909  dffr2 2914  frirr 2919  fr2nr 2920  fr3nr 2921  wefrc 2938  onfr 2981  ordon 2982  ssorduni 2988  onint 3001  onminex 3015  hbsuc 3035  sucel 3037  sucidg 3047  ordpwsuc 3061  unon 3083  ordunisuc 3084  onuninsuc 3103  orduninsuc 3109  onzsl 3112  limsssuc 3116  limuni3 3118  dfom2 3128  elomg 3130  omsson 3131  limomss 3132  ordom 3136  peano5 3148  finds 3151  findsg 3152  finds2 3153  findes 3155  tfinds 3156  tfindsg 3157  tfindsg2 3158  tfindes 3159  tfinds2 3160  opelxp1 3200  opelxp 3209  opelxpg 3211  ralxp 3213  ralxpf 3215  elxp3 3219  elvv 3223  optocl 3230  onxpdisj 3236  ssxp 3251  xpsspw 3252  relopab 3261  opabid2 3262  inxp 3264  relop 3270  ididg 3273  opelcog 3285  cnvco 3295  dfrn2 3298  dfdm4 3300  eldm2g 3304  dmss 3305  breldmg 3311  dmun 3312  dmin 3313  dmuni 3314  dmsnsn0 3320  dmi 3321  dmsnop 3323  reldm0 3326  elreldm 3333  hbrn 3345  dmrnssfld 3351  dmcoss 3355  dmcosseq 3357  opelresg 3366  resieq 3368  dmres 3372  relssres 3384  resopab 3387  resiexg 3388  iss 3389  dfima2 3397  hbima 3403  csbima12g 3405  imadmrn 3406  imai 3409  elimasng 3419  args 3420  eliniseg 3421  iniseg 3422  dffr3 3423  intasym 3430  asymref 3431  asymref2 3432  intirr 3433  cnvopab 3437  cnv0 3438  cnvi 3439  cnvsn 3441  elxp4 3445  elxp5 3446  cnvun 3447  cnvin 3448  rnuni 3451  dminss 3454  imainss 3455  cnvxp 3456  xpnz 3458  ssrnres 3473  rninxp 3474  dminxp 3475  dfrel2 3477  cores 3491  resco 3492  imaco 3493  rnco 3494  co02 3500  coi1 3502  coass 3504  relssdr 3505  cnvpo 3514  cnvso 3515  dffun2 3518  dffun6 3531  dffun7 3532  dffun8 3533  funsn 3535  funopg 3539  funco 3542  funssres 3544  funun 3546  funcnv2 3548  funcnv 3549  funcnv3 3550  fun2cnv 3551  fncnv 3553  funcnvuni 3556  imadif 3566  isarep1 3569  fneu 3584  2elresin 3590  fn0 3597  zfrep6 3606  fcoi1 3636  fcoi2 3637  feu 3638  fcnvres 3639  fabexg 3644  fconst 3649  fconstg 3650  f11 3655  fvprc 3712  fvex 3723  fv3 3724  tz6.12f 3729  tz6.12-2 3730  csbfv12g 3733  ndmfv 3736  funbrfv 3741  funopfvg 3743  fnbrfvb 3744  funbrfvbg 3748  fnopabfv 3749  fnrnfv 3750  dfimafn 3752  funimass4 3754  fvelima 3755  fnsnfv 3758  ssimaexg 3760  dmfco 3764  fvco 3765  fvopab4gf 3772  fvopabg 3776  fvopabn 3777  fvopabgf 3778  fvopabnf 3779  fvopab2 3782  eqfnfv 3788  funfvop 3794  fvelrn 3803  dff2 3808  dff3 3809  dffo4 3811  exfo 3813  fopabcos 3824  fsn 3825  fnressn 3828  fressnfv 3829  fvi 3833  funfvima3 3845  fvclss 3846  fvresex 3848  abrexexlem2 3850  abrexex 3851  abrexexg 3852  imaiun 3855  funiunfv 3857  abexssex 3863  f1fv 3865  f1ofveu 3873  cbvfo 3876  isomin 3890  isoini 3891  isofrlem 3892  f1oweALT 3897  tfrlem2 3903  tfrlem3 3904  tfrlem8 3909  tfrlem9 3910  tfrlem10 3911  tfrlem11 3912  tz7.44lem1 3918  rdg0t 3935  rdglim2 3940  tz7.48-1 3947  abianfplem 3952  csboprg 3977  eloprabg 3998  resoprab 4000  oprabval2gf 4017  oprabval5 4020  oprssdm 4033  caoprmo 4062  op1stg 4077  op2ndg 4078  1stval2 4079  2ndval2 4080  fo1st 4081  fo2nd 4082  f1stres 4083  f2ndres 4084  1st2val 4085  2nd2val 4086  2ndconst 4087  curry1 4088  sbcopeq1a 4101  csbopeq1a 4102  dfopab2 4103  dfoprab3 4104  dfoprab5 4105  dfoprab4 4106  df1st2 4116  df2nd2 4117  oacl 4160  omcl 4161  oecl 4162  oa0r 4163  om0r 4164  om1r 4167  oe1m 4169  oaordi 4170  oawordri 4174  oawordeulem 4178  oalimcl 4184  oaass 4185  oarec 4186  omordi 4187  omwordri 4193  omlimcl 4199  odi 4200  omass 4201  oen0 4203  oeordi 4204  oewordri 4209  oeworde 4210  oaabs 4242  omsmolem 4246  ider 4259  eqerlem 4260  erref 4265  erdmrn 4266  ecdmn0 4270  erthi 4271  erth 4272  erdisj 4276  elqsi 4281  0nelqs 4288  ecid 4290  qsid 4291  brecop 4296  ecopoprdm 4299  ecopoprsym 4300  ecopoprtrn 4301  ecopoprer 4302  th3qlem1 4304  mapprc 4316  fnmap 4319  mapvalg 4320  pmvalg 4321  mapval2 4325  map0 4334  mapsn 4335  ixpconst 4342  ss2ixp 4344  ixp0 4351  mapixp 4352  breng 4363  brdomg 4364  domen 4367  domeng 4368  idssen 4393  ener 4397  ensymg 4398  entrt 4401  domtr 4402  ensn1g 4412  en1 4413  fundmen 4415  mapsnen 4416  unen 4420  xpsnen 4421  xpsneng 4422  xpcomen 4425  xpcomeng 4426  xpassen 4427  xpdom2 4428  xpdom1g 4430  xpdom3 4431  pw2en 4432  sbth 4443  sbthcl 4445  fodomr 4469  canth2 4470  canth2g 4471  mapenlem1 4475  mapenlem2 4476  mapdom1 4478  mapdom2lem 4479  mapdom2 4480  mapunen 4488  pwen 4489  ssenen 4490  nneneq 4498  php 4499  php2 4500  php3 4501  0sdom1dom 4510  ominf 4514  pssnn 4519  ssfi 4521  domfi 4522  unbnn2 4528  isfinite2 4529  infcntss 4536  unifi 4538  fiint 4540  abfii2 4542  abfii3 4543  abfii4 4544  fodomfi 4546  pwfilem 4550  pwfi 4551  pm54.43 4552  suppr 4570  elirrv 4578  zfregfr 4581  en2lp 4582  inf0 4586  inf3lema 4589  inf3lemd 4592  inf3lem1 4593  inf3lem2 4594  inf3lem3 4595  inf3lem5 4597  inf3lem6 4598  inf3lem7 4599  inf3 4600  infeq5 4601  omex 4607  dfom3 4610  infensuc 4618  unbnnt 4619  zfregs 4627  setind2 4629  r1tr 4634  r1ord 4635  r1val1 4638  tz9.12lem1 4639  tz9.12lem3 4641  tz9.13 4643  tz9.13g 4644  rankwflem 4645  jech9.3 4646  rankvalg 4649  rankr1 4654  rankr1g 4655  r1val2 4658  rankval3 4661  bndrank 4662  ranklim 4665  r1pw 4666  r1pwcl 4667  rankuni2 4670  rankun 4671  rankonid 4675  rankr1id 4677  rankuni 4678  rankval4 4682  rankxplim 4692  rankxplim3 4694  rankxpsuc 4695  cp 4702  bnd2 4704  kardex 4705  karden 4706  aceq3lem 4712  aceq3 4713  aceq4 4714  aceq5lem1 4715  aceq5lem2 4716  aceq5lem3 4717  aceq5lem4 4718  aceq5lem5 4719  aceq5 4720  aceq6a 4721  aceq6b 4722  ac6lem 4734  ac6s 4736  ac9s 4744  kmlem1 4745  kmlem2 4746  kmlem4 4748  kmlem9 4753  kmlem10 4754  kmlem11 4755  kmlem12 4756  kmlem13 4757  numthlem 4763  numth2 4765  numthcor 4766  zorn2lem1 4768  zorn2lem7 4774  zornlem 4775  fodom 4778  fodomg 4779  brdom3 4781  brdom5 4782  brdom4 4783  brdom7disj 4784  brdom6disj 4785  unidomg 4789  cardval 4806  unxpdomlem 4823  unxpdom 4824  sucxpdom 4826  cardlim 4831  iscard2 4834  ondomon 4836  ondomcard 4837  carduni 4838  cardiun 4839  cardmin 4840  alephon 4845  alephcard 4847  alephordi 4854  cardaleph 4865  alephval2 4882  alephval3 4883  dominf 4884  cffnon 4887  cflim 4889  cardcf 4891  cfeq0 4894  cfsuc 4895  cfom 4896  cdavalt 4899  ltpiord 4995  indpi 5014  dmenq 5025  enqer 5026  addcmpblnq 5032  mulcmpblnq 5033  addpipq 5034  mulpipq 5035  ordpipq 5036  addcompq 5042  addasspq 5043  mulcompq 5044  mulasspq 5045  distrpqlem 5046  distrpq 5047  mulidpq 5049  recmulpq 5050  ltsopq 5055  ltapq 5056  ltmpq 5057  ltexpq 5060  ltexpq2 5061  halfpq 5062  nsmallpq 5063  ltbtwnpq 5064  ltrpq 5065  prnmadd 5080  genpv 5082  genpdm 5085  genpnnp 5088  genpcd 5089  genpnmax 5090  genpcl 5091  genpass 5092  1pr 5097  addclprlem1 5098  addclprlem2 5099  addclpr 5100  mulclprlem 5101  mulclpr 5102  addcompr 5103  addasspr 5104  mulcompr 5105  mulasspr 5106  distrlem1pr 5107  distrlem2pr 5108  distrlem4pr 5110  distrlem5pr 5111  1idpr 5113  prlem934a 5117  prlem934b 5118  prlem934 5119  ltaddpr 5120  ltexprlem1 5122  ltexprlem2 5123  ltexprlem3 5124  ltexprlem4 5125  ltexprlem6 5127  ltexprlem7 5128  ltexpri 5129  ltaprlem 5130  prlem936a 5133  prlem936 5135  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  reclem4pr 5139  recexpr 5140  suplem1pr 5141  suplem2pr 5142  dmenr 5155  enrer 5156  addcmpblnr 5161  mulcmpblnrlem 5162  addsrpr 5164  mulsrpr 5165  ltsrpr 5166  addcomsr 5176  addasssr 5177  mulcomsr 5178  mulasssr 5179  distrsr 5180  ltsosr 5183  0idsr 5186  1idsr 5187  ltasr 5189  recexsrlem 5192  mulgt0sr 5194  sqgt0sr 5195  recexsr 5196  map2psrpr 5200  suppsrlem 5201  suppsr 5202  suppsr2 5203  suppsr3 5204  supsrlem2 5206  supsrlem3 5207  supsrlem6 5210  ltresr 5238  supre 5240  ltsor 5241  axmulrcl 5254  axaddcom 5255  axmulcom 5256  axaddass 5257  axmulass 5258  axdistr 5259  axrrecex 5264  axcnre 5266  pre-axltadd 5269  pre-axmulgt0 5270  csbnegg 5344  ssxr 5521  peano2nn 5891  lbinfm 6003  dfinfmr 6022  infmsup 6023  infmxrcl 6041  dfuz 6158  ser1ft 6273  uzind4s 6392  dfseq0 6503  sumex 6927  dffsum 6944  fsum1f 6953  fsum1slem 6954  fsump1f 6957  csbfsum 6973  climfnn 7038  climeu 7045  climreu 7046  climmulc2 7073  iserzext 7079  caucvg3lem 7110  isumclimtf 7139  isumclim2tf 7141  isumshft 7147  isumshft2 7148  isumclt 7152  isumreclt 7153  isummulc1ALT 7156  infcvglem1 7164  fsum0diaglem2 7200  fsum0diag2 7202  efseq0ex 7261  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  xpnnen 7449  infxpidmlem1 7503  infxpidmlem4 7506  infxpidmlem5 7507  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem9 7511  infxpidmlem10 7512  infxpidmlem11 7513  infxpidmlem12 7514  unictb 7526  unctb 7527  infmap2lem1 7529  infmap2lem2 7530  infmap2 7531  tgval2t 7567  tgval3t 7575  eltg3t 7576  tgss3t 7588  basgent 7590  subbas 7594  subbas2 7595  subtop 7596  sn0top 7597  indistop 7598  distop 7599  fctop 7600  cctop 7602  ntrfval 7617  clsfval 7618  ntrval 7626  clsval 7627  clsval2 7635  neifval 7664  neif 7665  neival 7667  lpfval 7692  lpval 7693  islp2 7697  cncnplem2 7725  dfms2 7749  lmfval 7877  iscau 7888  metcld 7917  bopcnlem1 7931  bopcnlem3 7933  iscms2lem4 7942  cmsss 7947  cncms 7948  bcthlem13 7961  bcthlem32 7980  issubg 8068  nvvcop 8165  0vfval 8177  vsfval 8206  sqcn 8283  ipfval 8299  nmoubi 8380  ubthlem3 8475  ubthlem4 8476  minveclem10 8498  minveclem14 8502  psdmrn 8591  spwval2 8595  circgrp 8679  axgroth2 8717  axgroth3 8718  grothprim 8722  axhcompl 8807  hhcmpl 9008  hhcms 9011  hlimreu 9049  hlimeu 9050  chcmh 9052  helch 9055  hsn0elch 9059  hhsscms 9089  occl 9120  projlem25 9149  projlem 9156  chintcl 9233  dfchj3 9263  spanun 9405  spansn 9419  osumlem4 9521  osumlem6 9523  osumlem7 9524  pjrn 9587  nmopubt 9772  nmfnleubt 9788  nmopunt 9877  nmcopexlem1 9889  nmcfnexlem1 9918  nlelch 9932  cnlnssadj 9951  adjbd1o 9956  branmfnt 9976  bra11 9979  pjnmop 10013  hmopidmch 10017  pjhmopidm 10048  ghomgrplem 10323  symggrp 10342  cayleythlem 10347  ntunte 10376  uninqs 10378  elo 10381  infi1 10383  fine 10384  abfi 10385  stcat 10389  ficli 10404  fiv 10410  mapudiscn 10435  hmphsyma 10451  hmpher 10459  hmeogrp 10461  homcard 10462  subsp 10465  qusp 10466  oefil2 10477  fgsb 10480  infi 10484  fgsb2 10485  cnfilca 10487  dtopcl 10495  dtt2 10498  eloi 10539  ishomd 10598  blkssatm 10639

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain