Theorem visset 1859

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

Assertion

Ref	Expression
visset	|- x e. V

Proof of Theorem visset

Step	Hyp	Ref	Expression
1		eqid 1518	. 2 |- x = x
2		df-v 1858	. . 3 |- V = {x | x = x}
3	2	abeq2i 1613	. 2 |- (x e. V <-> x = x)
4	1, 3	mpbir 188	1 |- x e. V

Syntax hints:   = wceq 992   e. wcel 994  Vcvv 1857

This theorem is referenced by:  isset 1860  ralv 1866  rexv 1867  rabab 1868  eqvinc 1929  ceqex 1932  cbvab 1954  moeq3 1967  mo2icl 1969  moi2 1970  moi 1971  reu8 1982  sbhypf 1985  sbc2or 2006  sbccomg 2039  sbcralt 2040  sbcralgf 2042  sbcel12g 2062  sbceqdig 2063  csbvarg 2072  csbhypf 2080  csbiegft 2081  csbnestg 2088  csbabg 2095  uniiunlem 2184  ddif 2221  dfun2 2295  dfin2 2296  difab 2321  vn0 2339  eqv 2348  elpwg 2462  hbpw 2464  hbpr 2484  ralpr 2486  dftp2 2501  snssg 2527  difprsn 2529  prss 2536  prssg 2537  tpss 2541  prsspw 2545  pwpr 2567  pwv 2568  unipr 2581  uniprg 2582  reucl 2584  unisng 2585  elintg 2608  elinti 2609  hbint 2610  elintrabg 2613  intss1 2615  ssint 2616  intmin 2620  intss 2621  intssuni 2622  intmin4 2626  intab 2627  intun 2629  intpr 2630  iuniin 2641  dfiun2g 2654  dfiin2 2656  ssiin 2667  iinss 2668  0iin 2674  iinun2 2678  iundif2 2679  iindif2 2681  iinuni 2685  sspwuni 2687  iinpw 2690  iunpwss 2691  brab1 2733  sbcbrg 2736  nalset 2786  vprc 2787  inex1g 2792  ssexg 2795  intex 2803  axpweq 2817  pwexg 2824  abssexg 2825  snex 2826  elALT 2827  rext 2834  sspwb 2835  unipw 2836  pwuni 2837  ssextss 2839  nnullss 2846  exss 2847  axpr 2854  zfpair2 2856  opthg 2864  opthgg 2865  eqvinop 2867  copsexg 2868  copsex4g 2870  opprc1b 2872  opth2 2876  moop2 2878  opabid 2887  pwin 2903  pwunss 2904  pwssun 2905  pwundif 2906  epel 2912  dfid3 2914  posn 2928  dffr2 2949  frirr 2954  fr2nr 2955  wefrc 2970  tron 2998  onfr 3014  hbsuc 3044  sucel 3046  sucidg 3052  suctr 3055  uniexg 3094  unexb 3096  snnex 3100  opeluu 3103  uniuni 3104  euuni 3105  reuunisn 3118  iunpw 3137  fr3nr 3138  ssorduni 3147  onint 3152  onminex 3164  ordpwsuc 3172  unon 3185  ordunisuc 3186  onuninsuci 3194  orduninsuc 3197  onzsl 3200  limsssuc 3204  limuni3 3206  tfinds 3212  tfindsg 3213  tfindsg2 3214  tfindes 3215  tfinds2 3216  dfom2 3220  elomg 3222  omsson 3223  limomss 3224  ordom 3228  peano5 3241  finds 3244  findsg 3245  finds2 3246  findes 3248  opelxp1 3288  opelxp 3297  opelxpg 3299  ralxp 3301  ralxpf 3303  elxp3 3309  elvv 3313  elvvv 3314  optocl 3321  0nelelxp 3327  onxpdisj 3328  ssxp 3345  xpsspw 3346  relopab 3357  opabid2 3360  inxp 3362  relop 3365  ididg 3368  opelco2g 3380  cnvco 3391  dfrn2 3394  dfdm4 3396  eldm2g 3400  dmss 3401  breldmg 3407  dmun 3408  dmin 3409  dmuni 3410  dmi 3415  reldm0 3418  elreldm 3425  hbrn 3438  dmrnssfld 3444  dmcoss 3450  dmcosseq 3452  opelresg 3461  resieq 3463  dmres 3470  relssres 3482  resopab 3485  resiexg 3486  iss 3487  dfima2 3497  hbima 3503  csbima12g 3505  imadmrn 3506  imai 3509  elimasng 3519  args 3520  eliniseg 3521  iniseg 3522  dffr3 3523  intasym 3530  asymref 3531  asymref2 3532  intirr 3533  cnvopab 3537  cnv0 3538  cnvi 3539  cnvun 3540  cnvin 3541  rnuni 3544  dminss 3547  imainss 3548  cnvxp 3549  xpnz 3551  ssrnres 3566  rninxp 3567  dminxp 3568  dfrel2 3569  dmsnop 3577  cnvsn 3580  elxp4 3585  elxp5 3586  dfco2 3598  dfco2a 3599  coundi 3600  coundir 3601  cores 3602  resco 3603  imaco 3604  rnco 3605  coiun 3608  co02 3612  coi1 3614  coass 3616  relssdmrn 3617  cnvpo 3627  cnvso 3628  dffun2 3631  dffun7 3644  dffun8 3645  dffun9 3646  funsn 3648  funopg 3652  funco 3655  funssres 3657  funun 3659  funcnv2 3661  funcnv 3662  funcnv3 3663  fun2cnv 3664  fncnv 3666  funcnvuni 3669  imadif 3679  isarep1 3683  fneu 3698  2elresin 3704  fn0 3711  iunfopab 3719  zfrep6 3721  fcoi1 3752  fcoi2 3753  feu 3754  fcnvres 3755  fabexg 3760  fconst 3765  fconstg 3766  dff12 3771  fvprc 3832  fvex 3843  fv3 3844  tz6.12f 3849  tz6.12-2 3850  csbfv12g 3853  ndmfv 3856  funbrfv 3861  funopfvg 3863  fnbrfvb 3864  funbrfvbg 3868  dffn5 3869  fnrnfv 3870  dfimafn 3872  funimass4 3874  fvelima 3875  fnsnfv 3878  ssimaexg 3880  dmfco 3884  fvco 3885  fvopab4gf 3892  fvopabg 3896  fvopabn 3897  fvopabgf 3898  fvopabnf 3899  fvopab2 3902  eqfnfv 3909  eqfnfv2 3911  funfvop 3917  fvelrn 3926  dff3 3931  dff4 3932  dffo4 3934  exfo 3936  fopabcos 3947  fsn 3948  fnressn 3951  fressnfv 3952  fvi 3956  funfvima3 3968  fvclss 3969  fvresex 3971  abrexexlem2 3973  abrexex 3974  abrexexg 3975  imaiun 3978  funiunfv 3980  abexssex 3986  dff13 3988  f1ofveu 3996  cbvfo 3999  isomin 4013  isoini 4014  isofrlem 4015  f1oweALT 4020  csboprg 4044  eloprabg 4067  resoprab 4069  oprabval2gf 4086  oprabval5 4089  oprabval4gALT 4092  oprssdm 4103  caoprmo 4131  op1stg 4148  op2ndg 4149  1stval2 4150  2ndval2 4151  fo1st 4152  fo2nd 4153  f1stres 4154  f2ndres 4155  fo1stres 4156  fo2ndres 4157  1st2val 4158  2nd2val 4159  sbcopeq1a 4171  csbopeq1a 4172  dfopab2 4173  dfoprab3 4174  dfoprab4s 4176  dfoprab5s 4177  dfoprab5sf 4178  df1st2 4188  df2nd2 4189  1stconst 4190  2ndconst 4191  curry1 4193  curry2 4196  fparlem1 4199  fparlem2 4200  fparlem3 4201  fparlem4 4202  fpar 4203  fsplit 4204  onopruni 4210  onopriun 4211  tfrlem2 4213  tfrlem3 4214  tfrlem8 4219  tfrlem9 4220  tfrlem10 4221  tfrlem11 4222  tz7.44lem1 4228  rdg0g 4245  rdglim2 4250  tz7.48-1 4257  abianfplem 4262  oacl 4306  omcl 4307  oecl 4308  oa0r 4309  om0r 4310  om1r 4313  oe1m 4315  oaordi 4316  oawordri 4320  oawordeulem 4324  oalimcl 4330  oaass 4331  oarec 4332  omordi 4333  omwordri 4339  omlimcl 4345  odi 4346  omass 4347  oen0 4349  oeordi 4350  oewordri 4355  oeworde 4356  oeoalem 4359  oeoelem 4361  oaabs 4392  omsmolem 4396  ider 4409  eqerlem 4410  erref 4415  erdmrn 4416  ecdmn0 4420  erthi 4421  erth 4422  erdisj 4426  elqsi 4431  uniqs 4436  0nelqs 4439  ecid 4441  qsid 4442  brecop 4447  ecopoprdm 4450  ecopoprsym 4451  ecopoprtrn 4452  ecopoprer 4453  th3qlem1 4455  mapprc 4467  fnmap 4470  mapvalg 4471  pmvalg 4472  mapval2 4476  map0 4485  mapsn 4486  ixpconst 4493  ss2ixp 4495  ixp0 4502  mapixp 4503  breng 4516  brdomg 4517  domen 4520  domeng 4521  idssen 4547  ener 4551  ensymg 4552  entr 4555  domtr 4556  ensn1g 4566  en1 4567  fundmen 4569  mapsnen 4570  unen 4575  xpsnen 4576  xpsneng 4577  xpcomen 4580  xpcomeng 4581  xpassen 4582  xpdom2 4583  xpdom1g 4585  xpdom3 4586  pw2en 4587  ac6sfilem3 4590  ac6sfi 4591  sbth 4602  sbthcl 4604  fodomr 4628  canth2 4629  canth2g 4630  mapenlem1 4636  mapenlem2 4637  mapdom1 4639  mapdom2lem 4640  mapdom2 4641  mapunen 4649  pwen 4650  ssenen 4651  nneneq 4659  php 4660  php2 4661  php3 4662  0sdom1dom 4671  ominf 4675  pssnn 4681  ssfi 4683  domfi 4684  xpfi 4685  unbnn2 4691  isfinite2 4692  infcntss 4699  unifi 4701  fiint 4703  abfii2 4705  abfii3 4706  abfii4 4707  fodomfi 4709  pwfilem 4713  pwfi 4714  pm54.43 4715  suppr 4733  elirrv 4741  zfregfr 4746  en2lp 4747  inf0 4751  inf3lema 4754  inf3lemd 4757  inf3lem1 4758  inf3lem2 4759  inf3lem3 4760  inf3lem5 4762  inf3lem6 4763  inf3lem7 4764  inf3 4765  infeq5 4766  omex 4772  dfom3 4776  infensuc 4784  unbnn3 4785  zfregs 4793  setind2 4795  r1tr 4800  r1ord 4801  r1val1 4804  tz9.12lem1 4805  tz9.12lem3 4807  tz9.13 4809  tz9.13g 4810  rankwflem 4811  jech9.3 4812  rankvalg 4815  rankr1 4820  rankr1g 4821  r1val2 4824  rankval3 4827  bndrank 4828  ranklim 4831  r1pw 4832  r1pwcl 4833  rankuni2 4836  rankun 4837  rankonid 4841  rankr1id 4843  rankuni 4844  rankval4 4848  rankxplim 4858  rankxplim3 4860  rankxpsuc 4861  cp 4868  bnd2 4870  kardex 4871  karden 4872  aceq3lem 4878  aceq3 4879  aceq4 4880  aceq5lem1 4881  aceq5lem2 4882  aceq5lem3 4883  aceq5lem4 4884  aceq5lem5 4885  aceq5 4886  aceq6a 4887  aceq6b 4888  ac6lem 4900  ac6s 4902  ac9s 4910  kmlem1 4911  kmlem2 4912  kmlem4 4914  kmlem9 4919  kmlem10 4920  kmlem11 4921  kmlem12 4922  kmlem13 4923  numthlem 4929  numth2 4931  numthcor 4932  zorn2lem1 4934  zorn2lem7 4940  zornlem 4941  fodom 4944  fodomg 4945  brdom3 4947  brdom5 4948  brdom4 4949  brdom7disj 4950  brdom6disj 4951  unidomg 4955  cardval 4973  unxpdomlem 4993  unxpdom 4994  sucxpdom 4996  cardlim 5001  iscard2 5004  ondomon 5006  ondomcard 5007  carduni 5008  cardiun 5009  cardmin 5010  alephon 5015  alephcard 5017  alephordi 5024  cardaleph 5035  alephval2 5052  alephval3 5053  dominf 5054  cffnon 5057  cflim 5059  cardcf 5061  cfeq0 5064  cfsuc 5065  cfom 5066  cdaval 5069  cdaung 5073  cdaeng 5076  nnacda 5090  ltpiord 5169  indpi 5188  dmenq 5199  enqer 5200  addcmpblnq 5206  mulcmpblnq 5207  addpipq 5208  mulpipq 5209  ordpipq 5210  addcompq 5216  addasspq 5217  mulcompq 5218  mulasspq 5219  distrpqlem 5220  distrpq 5221  mulidpq 5223  recmulpq 5224  ltsopq 5229  ltapq 5230  ltmpq 5231  ltexpq 5234  ltexpq2 5235  halfpq 5236  nsmallpq 5237  ltbtwnpq 5238  ltrpq 5239  prnmadd 5254  genpv 5256  genpdm 5259  genpnnp 5262  genpcd 5263  genpnmax 5264  genpcl 5265  genpass 5266  1pr 5271  addclprlem1 5272  addclprlem2 5273  addclpr 5274  mulclprlem 5275  mulclpr 5276  addcompr 5277  addasspr 5278  mulcompr 5279  mulasspr 5280  distrlem1pr 5281  distrlem2pr 5282  distrlem4pr 5284  distrlem5pr 5285  1idpr 5287  prlem934a 5291  prlem934b 5292  prlem934 5293  ltaddpr 5294  ltexprlem1 5296  ltexprlem2 5297  ltexprlem3 5298  ltexprlem4 5299  ltexprlem6 5301  ltexprlem7 5302  ltexpri 5303  ltaprlem 5304  prlem936a 5307  prlem936 5309  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  reclem4pr 5313  recexpr 5314  suplem1pr 5315  suplem2pr 5316  dmenr 5329  enrer 5330  addcmpblnr 5335  mulcmpblnrlem 5336  addsrpr 5338  mulsrpr 5339  ltsrpr 5340  addcomsr 5350  addasssr 5351  mulcomsr 5352  mulasssr 5353  distrsr 5354  ltsosr 5357  0idsr 5360  1idsr 5361  ltasr 5363  recexsrlem 5366  mulgt0sr 5368  sqgt0sr 5369  recexsr 5370  map2psrpr 5374  suppsrlem 5375  suppsr 5376  suppsr2 5377  suppsr3 5378  supsrlem2 5380  supsrlem3 5381  supsrlem6 5384  ltresr 5412  supre 5414  ltsor 5415  axmulrcl 5428  axaddcom 5429  axmulcom 5430  axaddass 5431  axmulass 5432  axdistr 5433  axrrecex 5438  axcnre 5440  pre-axltadd 5443  pre-axmulgt0 5444  csbnegg 5518  ssxr 5694  peano2nn 6080  lbinfm 6216  dfinfmr 6235  infmsup 6236  infmxrcl 6254  dfuzi 6373  uzind4s 6579  seq1lem1 6674  ser1f 6693  dfseq0 6758  sumex 7184  dffsum 7201  fsum1fi 7210  fsum1slem 7211  fsump1fi 7214  csbfsum 7230  climfnn 7295  climeu 7303  climreu 7304  climmulc2 7332  iserzex 7338  caucvg3lem 7369  isumclimtfi 7399  isumclim2f 7402  isumshfti 7408  isumshft2i 7409  isumcl 7413  isumrecl 7414  isummulc1iALT 7417  infcvglem1 7425  fsum0diaglem2 7462  fsum0diag2 7464  efseq0ex 7516  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  xpnnen 7711  infxpidmlem1 7764  infxpidmlem4 7767  infxpidmlem5 7768  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem9 7772  infxpidmlem10 7773  infxpidmlem11 7774  infxpidmlem12 7775  infpss 7786  unictb 7788  unctb 7789  infmap2lem1 7791  infmap2lem2 7792  infmap2 7793  tgval2 7829  tgval3 7837  eltg3 7838  tgss3 7850  basgen 7852  subbas 7856  subbas2 7857  subtop 7858  sn0top 7859  indistop 7860  distop 7861  cctop 7862  ntrfval 7877  clsfval 7878  ntrval 7886  clsval 7887  clsval2 7895  neifval 7924  neif 7925  neival 7927  lpfval 7952  lpval 7953  islp2 7957  cncnplem2 7985  dfms2 8009  lmfval 8136  iscau 8147  iscaunns 8155  metcls 8177  metcld 8178  bopcnlem1 8192  bopcnlem3 8194  iscms2lem4 8203  cmsss 8208  cncms 8209  bcthlem13 8222  bcthlem32 8241  gx1 8318  gxnn0suc 8320  issubg 8358  nvvcop 8460  vsfval 8501  vacnlem5 8586  vacnlem6 8587  sqcn 8589  ipfval 8606  nmoubi 8689  ubthlem3 8789  ubthlem4 8790  minveclem10 8814  minveclem14 8818  psdmrn 8910  spwval2 8915  spwpr2 8920  circgrp 9012  axgroth2 9050  axgroth3 9051  grothpw 9054  axgroth5 9055  grothprim 9057  axhcompl 9143  hhcmpl 9345  hhcms 9348  hlimreui 9386  hlimeui 9387  chcmhi 9389  helch 9392  hsn0elch 9396  hhsscms 9426  occli 9457  projlem25 9486  projlem 9493  chintcli 9571  dfchj3 9601  spanuni 9743  spansni 9756  osumlem4 9859  osumlem6 9861  osumlem7 9862  pjrni 9925  nmopub 10112  nmfnleub 10129  nmopun 10218  nmcopexlem1 10230  nmcfnexlem1 10259  nlelchi 10273  cnlnssadj 10292  adjbd1o 10297  branmfn 10317  branmfnOLD 10318  bra11 10321  pjnmopi 10355  hmopidmchi 10359  pjhmopidm 10390  ghomgrplem 10674  symggrp 10693  cayleythlem 10698  twsvbdop 10725  ntunte 10728  uninqs 10730  elo 10733  infi1 10735  fine 10736  abfi 10737  stcat 10741  ficli 10756  domrngref 10764  domintref 10767  ref3w 10772  cpref 10782  domleqt 10792  restidsing 10805  prj1 10809  eloi 10817  islatalg 10831  fiv 10849  infi 10854  inpc 10867  inposet 10868  lteqtpos 10880  pospos 10882  tostos 10883  toplat 10884  isppm 10917  on1el3 10962  on1el4 10963  mapudiscn 11015  sallnei 11016  nsn 11017  hmphsyma 11034  hmpher 11042  hmeogrp 11044  homcard 11045  eqindhome 11047  subsp 11056  sbtpsines 11062  subtopsin2 11067  qusp 11068  oefil2 11079  fgsb 11082  fgsb2 11086  cnfilca 11088  rcfpfillem4 11092  rcfpfillem6 11094  rcfpfil 11095  sfvlim 11100  dtt2 11110  fintopcomp 11115  bwt2 11123  usinuniop 11128  altretop 11144  dmrngcmp 11205  ishomd 11245  issubcat 11299  subtr 11395  subtr2 11396  cbvcsb 11397  cbvsbc 11398  dfiin2g 11400  cnvresima 11407  trer 11409  finminlem 11418  fiuni 11420  elfiun 11421  fictblem 11422  fictb 11423  inficlALT 11424  finsschain 11425  ordtypelem1 11427  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  hartog 11436  onsdom 11437  omsubsuc2 11439  omsubsdomlem2 11441  elomsubsd 11446  omsublim 11448  infenomsub 11450  fibas 11452  opncldf1 11454  opnnei 11469  hausnei2 11471  subspid 11478  subsubtop 11479  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  comptoppr 11495  alexsublem1 11496  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  cnconn 11503  conntoppr 11504  subtopmet 11506  is1stc3 11530  2ndcsb 11537  2ndc1stc 11538  2ndcctbss 11539  isfne2 11542  isfne3 11543  fneer 11557  fneerdm 11559  topfneec 11562  fnessref 11564  refssfne 11565  lfinpfin 11574  locfincomp 11575  locfindsc 11576  locfincf 11577  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmtcl 11586  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  ist1-3 11604  isfbas2 11622  fbssint 11626  fsubbas 11630  fbunfip 11631  elfg 11633  filrn 11643  neifg 11644  supfil 11645  filfinnfr 11646  isufil2 11650  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  filufint 11659  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  limfilcf 11683  hausfillim 11685  cnpfillim 11686  filmapf 11688  elfilmap 11690  fmf 11693  fmbas 11694  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  sfcls 11716  filclus 11717  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  fclusff 11735  tosdir 11755  tailf 11756  istail 11757  tailmap 11759  tailuni 11761  tailfb 11762  filnetlem1 11763  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gaid 11776  ssga 11777  gapmlem 11783  gapm 11784  xp1st 11796  xp2nd 11797  opabex3 11806  oprabopabf 11807  fnopabco 11810  inixp 11820  dif1en 11833  findcard 11836  fimax 11837  fixp 11840  ac6gf 11841  acdcg 11842  acdc3g 11843  acdc5g 11844  indexd 11846  indexf 11847  inficl 11849  frinfm 11850  fzpr 11866  sdclem1 11875  sdclem2 11876  sdc 11877  incld 11899  subspabs 11903  metsstop 11909  mettrifi2 11913  cnimass 11949  cnresima 11952  cnss 11953  cncfres 11956  tlmval 11964  haustlmu 11967  txbas 11973  txuni 11975  uptx 11978  txcn 11979  txsubsp 11983  sstotbnd 11992  totbndbnd 12000  heiborlem1 12011  heiborlem10 12020  heiborlem23 12033  heiborlem28 12038  heiborlem38 12048  heiborlem41 12051  bfplem8 12061  bfp 12065  rrntotbnd 12078  ismrer1 12080  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096  phtpcdm 12103  phtpcer 12104  blkssatm 12193  ssunipwALTlem1 12210  ssunipwALT 12211

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858

Copyright terms: Public domain