Theorem visset 1816

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

Assertion

Ref	Expression
visset	|- x e. V

Proof of Theorem visset

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

Syntax hints:   = wceq 958   e. wcel 960  Vcvv 1814

This theorem is referenced by:  isset 1817  ralv 1823  rexv 1824  rabab 1825  eqvinc 1886  ceqex 1889  cbvab 1911  moeq3 1924  mo2icl 1926  moi2 1927  moi 1928  reu8 1939  sbhypf 1942  sbhyp 1943  sbc2or 1962  sbccomg 1993  sbcralt 1994  sbcralgf 1996  sbcel12g 2015  sbceqdig 2016  csbvarg 2025  csbiegft 2033  csbnestg 2040  csbabg 2047  uniiunlem 2136  ddif 2173  dfun2 2247  dfin2 2248  difab 2273  vne0 2291  eqv 2300  elpwg 2410  hbpw 2412  hbpr 2431  ralpr 2433  dftp2 2445  snssg 2468  difprsn 2470  prss 2476  prssg 2477  tpss 2481  prsspw 2485  pwv 2507  unipr 2520  uniprg 2521  unisng 2523  elintg 2546  elinti 2547  hbint 2548  elintrabg 2551  intss1 2553  ssint 2554  intmin 2558  intss 2559  intssuni 2560  intmin4 2564  intab 2565  intun 2567  intpr 2568  iuniin 2578  dfiun2g 2591  dfiin2 2593  ssiin 2604  iinss 2605  0iin 2611  iinun2 2615  iundif2 2616  iindif2 2617  iinuni 2621  iinpw 2623  iunpwss 2624  brab1 2666  sbcbrg 2668  dftr4 2691  nalset 2718  nvelv 2719  inex1g 2724  ssexg 2727  intex 2735  pwexg 2753  abssexg 2754  snex 2757  el 2758  rext 2761  sspwb 2762  unipw 2763  pwuni 2764  ssextss 2769  nnullss 2775  exss 2776  axpr 2785  zfpair2 2787  opthg 2795  opthgg 2796  eqvinop 2798  copsexg 2799  copsex4g 2801  opprc1b 2803  opth2 2807  moop2 2808  opabid 2817  pwin 2832  pwunss 2833  pwssun 2834  pwundif 2835  epel 2841  dfid3 2843  uniexg 2878  unexb 2880  opeluu 2886  uniuni 2887  euuni 2888  reucl 2892  reuunisn 2902  iunpw 2921  dffr2 2926  frirr 2931  fr2nr 2932  fr3nr 2933  wefrc 2950  onfr 2993  ordon 2994  ssorduni 3000  onint 3013  onminex 3027  hbsuc 3047  sucel 3049  sucidg 3059  ordpwsuc 3073  unon 3095  ordunisuc 3096  onuninsuc 3115  orduninsuc 3121  onzsl 3124  limsssuc 3128  limuni3 3130  dfom2 3140  elomg 3142  omsson 3143  limomss 3144  ordom 3148  peano5 3160  finds 3163  findsg 3164  finds2 3165  findes 3167  tfinds 3168  tfindsg 3169  tfindsg2 3170  tfindes 3171  tfinds2 3172  opelxp1 3212  opelxp 3221  opelxpg 3223  ralxp 3225  ralxpf 3227  elxp3 3231  elvv 3235  optocl 3242  onxpdisj 3248  ssxp 3263  xpsspw 3264  relopab 3273  opabid2 3274  inxp 3276  relop 3282  ididg 3285  opelcog 3297  cnvco 3307  dfrn2 3310  dfdm4 3312  eldm2g 3316  dmss 3317  breldmg 3323  dmun 3324  dmin 3325  dmuni 3326  dmsnsn0 3332  dmi 3333  dmsnop 3335  reldm0 3338  elreldm 3345  hbrn 3358  dmrnssfld 3364  dmcoss 3370  dmcosseq 3372  opelresg 3381  resieq 3383  dmres 3387  relssres 3399  resopab 3402  resiexg 3403  iss 3404  dfima2 3412  hbima 3418  csbima12g 3420  imadmrn 3421  imai 3424  elimasng 3434  args 3435  eliniseg 3436  iniseg 3437  dffr3 3438  intasym 3445  asymref 3446  asymref2 3447  intirr 3448  cnvopab 3452  cnv0 3453  cnvi 3454  cnvsn 3456  elxp4 3460  elxp5 3461  cnvun 3462  cnvin 3463  rnuni 3466  dminss 3469  imainss 3470  cnvxp 3471  xpnz 3473  ssrnres 3488  rninxp 3489  dminxp 3490  dfrel2 3492  cores 3506  resco 3507  imaco 3508  rnco 3509  co02 3515  coi1 3517  coass 3519  relssdr 3520  cnvpo 3529  cnvso 3530  dffun2 3533  dffun6 3546  dffun7 3547  dffun8 3548  funsn 3550  funopg 3554  funco 3557  funssres 3559  funun 3561  funcnv2 3563  funcnv 3564  funcnv3 3565  fun2cnv 3566  fncnv 3568  funcnvuni 3571  imadif 3581  isarep1 3584  fneu 3599  2elresin 3605  fn0 3612  zfrep6 3621  fcoi1 3652  fcoi2 3653  feu 3654  fcnvres 3655  fabexg 3660  fconst 3665  fconstg 3666  f11 3671  fvprc 3728  fvex 3739  fv3 3740  tz6.12f 3745  tz6.12-2 3746  csbfv12g 3749  ndmfv 3752  funbrfv 3757  funopfvg 3759  fnbrfvb 3760  funbrfvbg 3764  fnopabfv 3765  fnrnfv 3766  dfimafn 3768  funimass4 3770  fvelima 3771  fnsnfv 3774  ssimaexg 3776  dmfco 3780  fvco 3781  fvopab4gf 3788  fvopabg 3792  fvopabn 3793  fvopabgf 3794  fvopabnf 3795  fvopab2 3798  eqfnfv 3804  funfvop 3810  fvelrn 3819  dff2 3824  dff3 3825  dffo4 3827  exfo 3829  fopabcos 3840  fsn 3841  fnressn 3844  fressnfv 3845  fvi 3849  funfvima3 3861  fvclss 3862  fvresex 3864  abrexexlem2 3866  abrexex 3867  abrexexg 3868  imaiun 3871  funiunfv 3873  abexssex 3879  f1fv 3881  f1ofveu 3889  cbvfo 3892  isomin 3906  isoini 3907  isofrlem 3908  f1oweALT 3913  tfrlem2 3919  tfrlem3 3920  tfrlem8 3925  tfrlem9 3926  tfrlem10 3927  tfrlem11 3928  tz7.44lem1 3934  rdg0t 3951  rdglim2 3956  tz7.48-1 3963  abianfplem 3968  csboprg 3993  eloprabg 4014  resoprab 4016  oprabval2gf 4033  oprabval5 4036  oprssdm 4049  caoprmo 4077  op1stg 4094  op2ndg 4095  1stval2 4096  2ndval2 4097  fo1st 4098  fo2nd 4099  f1stres 4100  f2ndres 4101  1st2val 4102  2nd2val 4103  2ndconst 4104  curry1 4105  sbcopeq1a 4118  csbopeq1a 4119  dfopab2 4120  dfoprab3 4121  dfoprab5 4122  dfoprab4 4123  df1st2 4133  df2nd2 4134  oacl 4177  omcl 4178  oecl 4179  oa0r 4180  om0r 4181  om1r 4184  oe1m 4186  oaordi 4187  oawordri 4191  oawordeulem 4195  oalimcl 4201  oaass 4202  oarec 4203  omordi 4204  omwordri 4210  omlimcl 4216  odi 4217  omass 4218  oen0 4220  oeordi 4221  oewordri 4226  oeworde 4227  oaabs 4259  omsmolem 4263  ider 4276  eqerlem 4277  erref 4282  erdmrn 4283  ecdmn0 4287  erthi 4288  erth 4289  erdisj 4293  elqsi 4298  0nelqs 4305  ecid 4307  qsid 4308  brecop 4313  ecopoprdm 4316  ecopoprsym 4317  ecopoprtrn 4318  ecopoprer 4319  th3qlem1 4321  mapprc 4333  fnmap 4336  mapvalg 4337  pmvalg 4338  mapval2 4342  map0 4351  mapsn 4352  ixpconst 4359  ss2ixp 4361  ixp0 4368  mapixp 4369  breng 4382  brdomg 4383  domen 4386  domeng 4387  idssen 4413  ener 4417  ensymg 4418  entrt 4421  domtr 4422  ensn1g 4432  en1 4433  fundmen 4435  mapsnen 4436  unen 4441  xpsnen 4442  xpsneng 4443  xpcomen 4446  xpcomeng 4447  xpassen 4448  xpdom2 4449  xpdom1g 4451  xpdom3 4452  pw2en 4453  sbth 4464  sbthcl 4466  fodomr 4490  canth2 4491  canth2g 4492  mapenlem1 4496  mapenlem2 4497  mapdom1 4499  mapdom2lem 4500  mapdom2 4501  mapunen 4509  pwen 4510  ssenen 4511  nneneq 4519  php 4520  php2 4521  php3 4522  php3OLD 4523  0sdom1dom 4532  ominf 4538  ominfOLD 4539  pssnn 4546  ssfi 4549  ssfiOLD 4550  domfi 4551  domfiOLD 4552  unbnn2 4558  isfinite2 4559  isfinite2OLD 4560  infcntss 4569  unifi 4572  unifiOLD 4574  fiint 4576  fiintOLD 4577  abfii2 4580  abfii3 4581  fodomfi 4582  fodomfiOLD 4583  pwfilem 4584  pwfilemOLD 4585  pwfi 4586  pwfiOLD 4587  pm54.43 4588  suppr 4606  elirrv 4614  zfregfr 4617  en2lp 4618  inf0 4622  inf3lema 4625  inf3lemd 4628  inf3lem1 4629  inf3lem2 4630  inf3lem3 4631  inf3lem5 4633  inf3lem6 4634  inf3lem7 4635  inf3 4636  infeq5 4637  omex 4643  dfom3 4646  infensuc 4655  unbnnt 4656  zfregs 4664  setind2 4666  r1tr 4671  r1ord 4672  r1val1 4675  tz9.12lem1 4676  tz9.12lem3 4678  tz9.13 4680  tz9.13g 4681  rankwflem 4682  jech9.3 4683  rankvalg 4686  rankr1 4691  rankr1g 4692  r1val2 4695  rankval3 4698  bndrank 4699  ranklim 4702  r1pw 4703  r1pwcl 4704  rankuni2 4707  rankun 4708  rankonid 4712  rankr1id 4714  rankuni 4715  rankval4 4719  rankxplim 4729  rankxplim3 4731  rankxpsuc 4732  cp 4739  bnd2 4741  kardex 4742  karden 4743  aceq3lem 4749  aceq3 4750  aceq4 4751  aceq5lem1 4752  aceq5lem2 4753  aceq5lem3 4754  aceq5lem4 4755  aceq5lem5 4756  aceq5 4757  aceq6a 4758  aceq6b 4759  ac6lem 4771  ac6s 4773  ac9s 4781  kmlem1 4782  kmlem2 4783  kmlem4 4785  kmlem9 4790  kmlem10 4791  kmlem11 4792  kmlem12 4793  kmlem13 4794  numthlem 4800  numth2 4802  numthcor 4803  zorn2lem1 4805  zorn2lem7 4811  zornlem 4812  fodom 4815  fodomg 4816  brdom3 4818  brdom5 4819  brdom4 4820  brdom7disj 4821  brdom6disj 4822  unidomg 4826  cardval 4843  unxpdomlem 4861  unxpdom 4862  sucxpdom 4864  cardlim 4869  iscard2 4872  ondomon 4874  ondomcard 4875  carduni 4876  cardiun 4877  cardmin 4878  alephon 4883  alephcard 4885  alephordi 4892  cardaleph 4903  alephval2 4920  alephval3 4921  dominf 4922  dominfOLD 4923  cffnon 4926  cflim 4928  cardcf 4930  cfeq0 4933  cfsuc 4934  cfom 4935  cdavalt 4938  ltpiord 5034  indpi 5053  dmenq 5064  enqer 5065  addcmpblnq 5071  mulcmpblnq 5072  addpipq 5073  mulpipq 5074  ordpipq 5075  addcompq 5081  addasspq 5082  mulcompq 5083  mulasspq 5084  distrpqlem 5085  distrpq 5086  mulidpq 5088  recmulpq 5089  ltsopq 5094  ltapq 5095  ltmpq 5096  ltexpq 5099  ltexpq2 5100  halfpq 5101  nsmallpq 5102  ltbtwnpq 5103  ltrpq 5104  prnmadd 5119  genpv 5121  genpdm 5124  genpnnp 5127  genpcd 5128  genpnmax 5129  genpcl 5130  genpass 5131  1pr 5136  addclprlem1 5137  addclprlem2 5138  addclpr 5139  mulclprlem 5140  mulclpr 5141  addcompr 5142  addasspr 5143  mulcompr 5144  mulasspr 5145  distrlem1pr 5146  distrlem2pr 5147  distrlem4pr 5149  distrlem5pr 5150  1idpr 5152  prlem934a 5156  prlem934b 5157  prlem934 5158  ltaddpr 5159  ltexprlem1 5161  ltexprlem2 5162  ltexprlem3 5163  ltexprlem4 5164  ltexprlem6 5166  ltexprlem7 5167  ltexpri 5168  ltaprlem 5169  prlem936a 5172  prlem936 5174  reclem1pr 5175  reclem2pr 5176  reclem3pr 5177  reclem4pr 5178  recexpr 5179  suplem1pr 5180  suplem2pr 5181  dmenr 5194  enrer 5195  addcmpblnr 5200  mulcmpblnrlem 5201  addsrpr 5203  mulsrpr 5204  ltsrpr 5205  addcomsr 5215  addasssr 5216  mulcomsr 5217  mulasssr 5218  distrsr 5219  ltsosr 5222  0idsr 5225  1idsr 5226  ltasr 5228  recexsrlem 5231  mulgt0sr 5233  sqgt0sr 5234  recexsr 5235  map2psrpr 5239  suppsrlem 5240  suppsr 5241  suppsr2 5242  suppsr3 5243  supsrlem2 5245  supsrlem3 5246  supsrlem6 5249  ltresr 5277  supre 5279  ltsor 5280  axmulrcl 5293  axaddcom 5294  axmulcom 5295  axaddass 5296  axmulass 5297  axdistr 5298  axrrecex 5303  axcnre 5305  pre-axltadd 5308  pre-axmulgt0 5309  csbnegg 5383  ssxr 5559  peano2nn 5944  lbinfm 6057  dfinfmr 6076  infmsup 6077  infmxrcl 6095  dfuz 6211  ser1ft 6336  uzind4s 6460  dfseq0 6571  sumex 6988  dffsum 7005  fsum1f 7014  fsum1slem 7015  fsump1f 7018  csbfsum 7034  climfnn 7099  climeu 7107  climreu 7108  climmulc2 7136  iserzext 7142  caucvg3lem 7173  isumclimtf 7202  isumclim2tf 7205  isumshft 7211  isumshft2 7212  isumclt 7216  isumreclt 7217  isummulc1ALT 7220  infcvglem1 7228  fsum0diaglem2 7264  fsum0diag2 7266  efseq0ex 7318  acdc3lem 7494  acdc2lem2 7497  acdc5lem2 7500  acdclem 7502  xpnnen 7507  infxpidmlem1 7560  infxpidmlem4 7563  infxpidmlem5 7564  infxpidmlem7 7566  infxpidmlem8 7567  infxpidmlem9 7568  infxpidmlem10 7569  infxpidmlem11 7570  infxpidmlem12 7571  infpss 7582  unictb 7584  unctb 7585  unctbOLD 7586  infmap2lem1 7588  infmap2lem2 7589  infmap2 7590  tgval2t 7623  tgval3t 7631  eltg3t 7632  tgss3t 7644  basgent 7646  subtop 7650  sn0top 7651  indistop 7652  distop 7653  fctopOLD 7654  cctop 7656  ntrfval 7671  clsfval 7672  ntrval 7680  clsval 7681  clsval2 7689  neifval 7718  neif 7719  neival 7721  lpfval 7746  lpval 7747  islp2 7751  cncnplem2 7779  dfms2 7803  lmfval 7929  iscau 7940  iscaunns 7948  metcls 7970  metcld 7971  bopcnlem1 7985  bopcnlem3 7987  iscms2lem4 7996  cmsss 8001  cncms 8002  bcthlem13 8015  bcthlem32 8034  issubg 8119  nvvcop 8216  0vfval 8228  vsfval 8257  sqcn 8338  ipfval 8355  nmoubi 8438  ubthlem3 8534  ubthlem4 8535  minveclem10 8557  minveclem14 8561  psdmrn 8651  spwval2 8656  spwpr2 8661  circgrp 8742  axgroth2 8780  axgroth3 8781  grothprim 8785  axhcompl 8870  hhcmpl 9071  hhcms 9074  hlimreu 9112  hlimeu 9113  chcmh 9115  helch 9118  hsn0elch 9122  hhsscms 9152  occl 9183  projlem25 9212  projlem 9219  chintcl 9297  dfchj3 9327  spanun 9469  spansn 9482  osumlem4 9583  osumlem6 9585  osumlem7 9586  pjrn 9649  nmopubt 9834  nmfnleubt 9851  nmopunt 9941  nmcopexlem1 9953  nmcfnexlem1 9982  nlelch 9996  cnlnssadj 10015  adjbd1o 10020  branmfnt 10040  bra11 10043  pjnmop 10077  hmopidmch 10081  pjhmopidm 10112  ghomgrplem 10392  symggrp 10411  cayleythlem 10416  ntunte 10442  uninqs 10444  elo 10447  infi1 10449  fine 10450  abfi 10451  stcat 10455  ficli 10470  fiv 10478  inpc 10484  inposet 10485  mapudiscn 10506  hmphsyma 10522  hmpher 10530  hmeogrp 10532  homcard 10533  eqindhome 10535  subsp 10548  qusp 10549  oefil2 10560  fgsb 10563  infi 10567  fgsb2 10568  cnfilca 10570  rcfpfillem4 10574  rcfpfillem6 10576  rcfpfil 10577  sfvlim 10584  dtt2 10597  eloi 10638  ishomd 10697  blkssatm 10746

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815

Copyright terms: Public domain