Theorem visset 1810

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

Assertion

Ref	Expression
visset	|- x e. V

Proof of Theorem visset

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

Syntax hints:   = wceq 955   e. wcel 957  Vcvv 1808

This theorem is referenced by:  isset 1811  ralv 1817  rexv 1818  rabab 1819  eqvinc 1880  ceqex 1883  cbvab 1905  moeq3 1918  mo2icl 1920  moi2 1921  moi 1922  reu8 1933  sbhypf 1936  sbhyp 1937  sbc2or 1955  sbccomg 1986  sbcralt 1987  sbcralgf 1989  sbcel12g 2008  sbceqdig 2009  csbvarg 2018  csbiegft 2026  csbnestg 2033  csbabg 2040  uniiunlem 2129  ddif 2166  dfun2 2240  dfin2 2241  difab 2266  eqv 2292  elpwg 2402  hbpw 2404  hbpr 2423  ralpr 2425  dftp2 2437  snssg 2460  difprsn 2462  prss 2468  prssg 2469  tpss 2473  prsspw 2477  pwv 2498  unipr 2511  uniprg 2512  unisng 2514  elintg 2537  elinti 2538  hbint 2539  elintrabg 2542  intss1 2544  ssint 2545  intmin 2549  intss 2550  intssuni 2551  intmin4 2555  intab 2556  intun 2558  intpr 2559  iuniin 2569  dfiun2g 2582  dfiin2 2584  ssiin 2595  iinss 2596  0iin 2602  iinun2 2605  iundif2 2606  iindif2 2607  iinuni 2611  iinpw 2613  iunpwss 2614  brab1 2656  sbcbrg 2658  dftr4 2681  nalset 2708  nvelv 2709  inex1g 2714  ssexg 2717  intex 2725  pwexg 2742  abssexg 2743  snex 2746  el 2747  rext 2750  sspwb 2751  unipw 2752  pwuni 2753  ssextss 2758  nnullss 2764  exss 2765  axpr 2774  zfpair2 2776  opthg 2784  opthgg 2785  eqvinop 2787  copsexg 2788  copsex4g 2790  opprc1b 2792  opth2 2796  moop2 2797  opabid 2806  pwin 2821  pwunss 2822  pwssun 2823  pwundif 2824  epel 2830  dfid3 2832  uniexg 2867  unexb 2869  opeluu 2875  uniuni 2876  euuni 2877  reucl 2881  reuunisn 2891  iunpw 2910  dffr2 2915  frirr 2920  fr2nr 2921  fr3nr 2922  wefrc 2939  onfr 2982  ordon 2983  ssorduni 2989  onint 3002  onminex 3016  hbsuc 3036  sucel 3038  sucidg 3048  ordpwsuc 3062  unon 3084  ordunisuc 3085  onuninsuc 3104  orduninsuc 3110  onzsl 3113  limsssuc 3117  limuni3 3119  dfom2 3129  elomg 3131  omsson 3132  limomss 3133  ordom 3137  peano5 3149  finds 3152  findsg 3153  finds2 3154  findes 3156  tfinds 3157  tfindsg 3158  tfindsg2 3159  tfindes 3160  tfinds2 3161  opelxp1 3201  opelxp 3210  opelxpg 3212  ralxp 3214  ralxpf 3216  elxp3 3220  elvv 3224  optocl 3231  onxpdisj 3237  ssxp 3252  xpsspw 3253  relopab 3262  opabid2 3263  inxp 3265  relop 3271  ididg 3274  opelcog 3286  cnvco 3296  dfrn2 3299  dfdm4 3301  eldm2g 3305  dmss 3306  breldmg 3312  dmun 3313  dmin 3314  dmuni 3315  dmsnsn0 3321  dmi 3322  dmsnop 3324  reldm0 3327  elreldm 3334  hbrn 3347  dmrnssfld 3353  dmcoss 3359  dmcosseq 3361  opelresg 3370  resieq 3372  dmres 3376  relssres 3388  resopab 3391  resiexg 3392  iss 3393  dfima2 3401  hbima 3407  csbima12g 3409  imadmrn 3410  imai 3413  elimasng 3423  args 3424  eliniseg 3425  iniseg 3426  dffr3 3427  intasym 3434  asymref 3435  asymref2 3436  intirr 3437  cnvopab 3441  cnv0 3442  cnvi 3443  cnvsn 3445  elxp4 3449  elxp5 3450  cnvun 3451  cnvin 3452  rnuni 3455  dminss 3458  imainss 3459  cnvxp 3460  xpnz 3462  ssrnres 3477  rninxp 3478  dminxp 3479  dfrel2 3481  cores 3495  resco 3496  imaco 3497  rnco 3498  co02 3504  coi1 3506  coass 3508  relssdr 3509  cnvpo 3518  cnvso 3519  dffun2 3522  dffun6 3535  dffun7 3536  dffun8 3537  funsn 3539  funopg 3543  funco 3546  funssres 3548  funun 3550  funcnv2 3552  funcnv 3553  funcnv3 3554  fun2cnv 3555  fncnv 3557  funcnvuni 3560  imadif 3570  isarep1 3573  fneu 3588  2elresin 3594  fn0 3601  zfrep6 3610  fcoi1 3640  fcoi2 3641  feu 3642  fcnvres 3643  fabexg 3648  fconst 3653  fconstg 3654  f11 3659  fvprc 3716  fvex 3727  fv3 3728  tz6.12f 3733  tz6.12-2 3734  csbfv12g 3737  ndmfv 3740  funbrfv 3745  funopfvg 3747  fnbrfvb 3748  funbrfvbg 3752  fnopabfv 3753  fnrnfv 3754  dfimafn 3756  funimass4 3758  fvelima 3759  fnsnfv 3762  ssimaexg 3764  dmfco 3768  fvco 3769  fvopab4gf 3776  fvopabg 3780  fvopabn 3781  fvopabgf 3782  fvopabnf 3783  fvopab2 3786  eqfnfv 3792  funfvop 3798  fvelrn 3807  dff2 3812  dff3 3813  dffo4 3815  exfo 3817  fopabcos 3828  fsn 3829  fnressn 3832  fressnfv 3833  fvi 3837  funfvima3 3849  fvclss 3850  fvresex 3852  abrexexlem2 3854  abrexex 3855  abrexexg 3856  imaiun 3859  funiunfv 3861  abexssex 3867  f1fv 3869  f1ofveu 3877  cbvfo 3880  isomin 3894  isoini 3895  isofrlem 3896  f1oweALT 3901  tfrlem2 3907  tfrlem3 3908  tfrlem8 3913  tfrlem9 3914  tfrlem10 3915  tfrlem11 3916  tz7.44lem1 3922  rdg0t 3939  rdglim2 3944  tz7.48-1 3951  abianfplem 3956  csboprg 3981  eloprabg 4002  resoprab 4004  oprabval2gf 4021  oprabval5 4024  oprssdm 4037  caoprmo 4065  op1stg 4080  op2ndg 4081  1stval2 4082  2ndval2 4083  fo1st 4084  fo2nd 4085  f1stres 4086  f2ndres 4087  1st2val 4088  2nd2val 4089  2ndconst 4090  curry1 4091  sbcopeq1a 4104  csbopeq1a 4105  dfopab2 4106  dfoprab3 4107  dfoprab5 4108  dfoprab4 4109  df1st2 4119  df2nd2 4120  oacl 4163  omcl 4164  oecl 4165  oa0r 4166  om0r 4167  om1r 4170  oe1m 4172  oaordi 4173  oawordri 4177  oawordeulem 4181  oalimcl 4187  oaass 4188  oarec 4189  omordi 4190  omwordri 4196  omlimcl 4202  odi 4203  omass 4204  oen0 4206  oeordi 4207  oewordri 4212  oeworde 4213  oaabs 4245  omsmolem 4249  ider 4262  eqerlem 4263  erref 4268  erdmrn 4269  ecdmn0 4273  erthi 4274  erth 4275  erdisj 4279  elqsi 4284  0nelqs 4291  ecid 4293  qsid 4294  brecop 4299  ecopoprdm 4302  ecopoprsym 4303  ecopoprtrn 4304  ecopoprer 4305  th3qlem1 4307  mapprc 4319  fnmap 4322  mapvalg 4323  pmvalg 4324  mapval2 4328  map0 4337  mapsn 4338  ixpconst 4345  ss2ixp 4347  ixp0 4354  mapixp 4355  breng 4366  brdomg 4367  domen 4370  domeng 4371  idssen 4396  ener 4400  ensymg 4401  entrt 4404  domtr 4405  ensn1g 4415  en1 4416  fundmen 4418  mapsnen 4419  unen 4423  xpsnen 4424  xpsneng 4425  xpcomen 4428  xpcomeng 4429  xpassen 4430  xpdom2 4431  xpdom1g 4433  xpdom3 4434  pw2en 4435  sbth 4446  sbthcl 4448  fodomr 4472  canth2 4473  canth2g 4474  mapenlem1 4478  mapenlem2 4479  mapdom1 4481  mapdom2lem 4482  mapdom2 4483  mapunen 4491  pwen 4492  ssenen 4493  nneneq 4501  php 4502  php2 4503  php3 4504  0sdom1dom 4513  ominf 4517  pssnn 4522  ssfi 4524  domfi 4525  unbnn2 4531  isfinite2 4532  infcntss 4539  unifi 4541  fiint 4543  abfii2 4545  abfii3 4546  abfii4 4547  fodomfi 4549  pwfilem 4553  pwfi 4554  pm54.43 4555  suppr 4573  elirrv 4581  zfregfr 4584  en2lp 4585  inf0 4589  inf3lema 4592  inf3lemd 4595  inf3lem1 4596  inf3lem2 4597  inf3lem3 4598  inf3lem5 4600  inf3lem6 4601  inf3lem7 4602  inf3 4603  infeq5 4604  omex 4610  dfom3 4613  infensuc 4621  unbnnt 4622  zfregs 4630  setind2 4632  r1tr 4637  r1ord 4638  r1val1 4641  tz9.12lem1 4642  tz9.12lem3 4644  tz9.13 4646  tz9.13g 4647  rankwflem 4648  jech9.3 4649  rankvalg 4652  rankr1 4657  rankr1g 4658  r1val2 4661  rankval3 4664  bndrank 4665  ranklim 4668  r1pw 4669  r1pwcl 4670  rankuni2 4673  rankun 4674  rankonid 4678  rankr1id 4680  rankuni 4681  rankval4 4685  rankxplim 4695  rankxplim3 4697  rankxpsuc 4698  cp 4705  bnd2 4707  kardex 4708  karden 4709  aceq3lem 4715  aceq3 4716  aceq4 4717  aceq5lem1 4718  aceq5lem2 4719  aceq5lem3 4720  aceq5lem4 4721  aceq5lem5 4722  aceq5 4723  aceq6a 4724  aceq6b 4725  ac6lem 4737  ac6s 4739  ac9s 4747  kmlem1 4748  kmlem2 4749  kmlem4 4751  kmlem9 4756  kmlem10 4757  kmlem11 4758  kmlem12 4759  kmlem13 4760  numthlem 4766  numth2 4768  numthcor 4769  zorn2lem1 4771  zorn2lem7 4777  zornlem 4778  fodom 4781  fodomg 4782  brdom3 4784  brdom5 4785  brdom4 4786  brdom7disj 4787  brdom6disj 4788  unidomg 4792  cardval 4809  unxpdomlem 4826  unxpdom 4827  sucxpdom 4829  cardlim 4834  iscard2 4837  ondomon 4839  ondomcard 4840  carduni 4841  cardiun 4842  cardmin 4843  alephon 4848  alephcard 4850  alephordi 4857  cardaleph 4868  alephval2 4885  alephval3 4886  dominf 4887  cffnon 4890  cflim 4892  cardcf 4894  cfeq0 4897  cfsuc 4898  cfom 4899  cdavalt 4902  ltpiord 4998  indpi 5017  dmenq 5028  enqer 5029  addcmpblnq 5035  mulcmpblnq 5036  addpipq 5037  mulpipq 5038  ordpipq 5039  addcompq 5045  addasspq 5046  mulcompq 5047  mulasspq 5048  distrpqlem 5049  distrpq 5050  mulidpq 5052  recmulpq 5053  ltsopq 5058  ltapq 5059  ltmpq 5060  ltexpq 5063  ltexpq2 5064  halfpq 5065  nsmallpq 5066  ltbtwnpq 5067  ltrpq 5068  prnmadd 5083  genpv 5085  genpdm 5088  genpnnp 5091  genpcd 5092  genpnmax 5093  genpcl 5094  genpass 5095  1pr 5100  addclprlem1 5101  addclprlem2 5102  addclpr 5103  mulclprlem 5104  mulclpr 5105  addcompr 5106  addasspr 5107  mulcompr 5108  mulasspr 5109  distrlem1pr 5110  distrlem2pr 5111  distrlem4pr 5113  distrlem5pr 5114  1idpr 5116  prlem934a 5120  prlem934b 5121  prlem934 5122  ltaddpr 5123  ltexprlem1 5125  ltexprlem2 5126  ltexprlem3 5127  ltexprlem4 5128  ltexprlem6 5130  ltexprlem7 5131  ltexpri 5132  ltaprlem 5133  prlem936a 5136  prlem936 5138  reclem1pr 5139  reclem2pr 5140  reclem3pr 5141  reclem4pr 5142  recexpr 5143  suplem1pr 5144  suplem2pr 5145  dmenr 5158  enrer 5159  addcmpblnr 5164  mulcmpblnrlem 5165  addsrpr 5167  mulsrpr 5168  ltsrpr 5169  addcomsr 5179  addasssr 5180  mulcomsr 5181  mulasssr 5182  distrsr 5183  ltsosr 5186  0idsr 5189  1idsr 5190  ltasr 5192  recexsrlem 5195  mulgt0sr 5197  sqgt0sr 5198  recexsr 5199  map2psrpr 5203  suppsrlem 5204  suppsr 5205  suppsr2 5206  suppsr3 5207  supsrlem2 5209  supsrlem3 5210  supsrlem6 5213  ltresr 5241  supre 5243  ltsor 5244  axmulrcl 5257  axaddcom 5258  axmulcom 5259  axaddass 5260  axmulass 5261  axdistr 5262  axrrecex 5267  axcnre 5269  pre-axltadd 5272  pre-axmulgt0 5273  csbnegg 5347  ssxr 5523  peano2nn 5893  lbinfm 6005  dfinfmr 6024  infmsup 6025  infmxrcl 6043  dfuz 6160  ser1ft 6278  uzind4s 6397  dfseq0 6508  sumex 6934  dffsum 6951  fsum1f 6960  fsum1slem 6961  fsump1f 6964  csbfsum 6980  climfnn 7045  climeu 7053  climreu 7054  climmulc2 7082  iserzext 7088  caucvg3lem 7119  isumclimtf 7148  isumclim2tf 7150  isumshft 7156  isumshft2 7157  isumclt 7161  isumreclt 7162  isummulc1ALT 7165  infcvglem1 7173  fsum0diaglem2 7209  fsum0diag2 7211  efseq0ex 7270  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  xpnnen 7458  infxpidmlem1 7512  infxpidmlem4 7515  infxpidmlem5 7516  infxpidmlem7 7518  infxpidmlem8 7519  infxpidmlem9 7520  infxpidmlem10 7521  infxpidmlem11 7522  infxpidmlem12 7523  infpss 7534  unictb 7536  unctb 7537  infmap2lem1 7539  infmap2lem2 7540  infmap2 7541  tgval2t 7577  tgval3t 7585  eltg3t 7586  tgss3t 7598  basgent 7600  subbas 7604  subbas2 7605  subtop 7606  sn0top 7607  indistop 7608  distop 7609  fctop 7610  cctop 7612  ntrfval 7627  clsfval 7628  ntrval 7636  clsval 7637  clsval2 7645  neifval 7674  neif 7675  neival 7677  lpfval 7702  lpval 7703  islp2 7707  cncnplem2 7735  dfms2 7759  lmfval 7887  iscau 7898  iscaunns 7906  metcls 7928  metcld 7929  bopcnlem1 7943  bopcnlem3 7945  iscms2lem4 7954  cmsss 7959  cncms 7960  bcthlem13 7973  bcthlem32 7992  issubg 8080  nvvcop 8177  0vfval 8189  vsfval 8218  sqcn 8298  ipfval 8314  nmoubi 8395  ubthlem3 8490  ubthlem4 8491  minveclem10 8513  minveclem14 8517  psdmrn 8606  spwval2 8610  spwpr2 8615  circgrp 8695  axgroth2 8733  axgroth3 8734  grothprim 8738  axhcompl 8823  hhcmpl 9024  hhcms 9027  hlimreu 9065  hlimeu 9066  chcmh 9068  helch 9071  hsn0elch 9075  hhsscms 9105  occl 9136  projlem25 9165  projlem 9172  chintcl 9250  dfchj3 9280  spanun 9422  spansn 9436  osumlem4 9538  osumlem6 9540  osumlem7 9541  pjrn 9604  nmopubt 9789  nmfnleubt 9806  nmopunt 9895  nmcopexlem1 9907  nmcfnexlem1 9936  nlelch 9950  cnlnssadj 9969  adjbd1o 9974  branmfnt 9994  bra11 9997  pjnmop 10031  hmopidmch 10035  pjhmopidm 10066  ghomgrplem 10345  symggrp 10364  cayleythlem 10369  ntunte 10398  uninqs 10400  elo 10403  infi1 10405  fine 10406  abfi 10407  stcat 10411  ficli 10426  fiv 10433  mapudiscn 10458  hmphsyma 10474  hmpher 10482  hmeogrp 10484  homcard 10485  subsp 10488  qusp 10489  oefil2 10500  fgsb 10503  infi 10507  fgsb2 10508  cnfilca 10510  rcfpfillem4 10514  rcfpfillem6 10516  rcfpfil 10517  dtopcl 10531  dtt2 10534  eloi 10575  ishomd 10634  blkssatm 10676

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain