HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem visset 1804
Description: All set variables are sets (see isset 1805). Theorem 6.8 of [Quine] p. 43.
Assertion
Ref Expression
visset |- x e. V
Proof of Theorem visset
StepHypRef Expression
1 eqid 1468 . 2 |- x = x
2 df-v 1803 . . 3 |- V = {x | x = x}
32abeq2i 1562 . 2 |- (x e. V <-> x = x)
41, 3mpbir 190 1 |- x e. V
Colors of variables: wff set class
Syntax hints:   = wceq 953   e. wcel 955  Vcvv 1802
This theorem is referenced by:  isset 1805  ralv 1811  rexv 1812  rabab 1813  eqvinc 1874  ceqex 1877  cbvab 1899  moeq3 1912  mo2icl 1914  moi 1915  reu8 1926  sbhypf 1929  sbhyp 1930  sbc2or 1948  sbccomg 1979  sbcralt 1980  sbcralgf 1982  sbcel12g 2001  sbceqdig 2002  csbvarg 2011  csbiegft 2019  csbnestg 2026  csbabg 2033  uniiunlem 2122  ddif 2159  dfun2 2233  dfin2 2234  difab 2259  eqv 2285  elpwg 2395  hbpw 2397  hbpr 2416  ralpr 2418  dftp2 2430  snssg 2454  difprsn 2456  prss 2462  prssg 2463  tpss 2467  prsspw 2471  pwv 2492  unipr 2505  uniprg 2506  unisng 2508  elintg 2531  elinti 2532  hbint 2533  elintrabg 2536  intss1 2538  ssint 2539  intmin 2543  intss 2544  intssuni 2545  intmin4 2549  intab 2550  intun 2552  intpr 2553  iuniin 2563  dfiun2g 2576  dfiin2 2578  ssiin 2589  iinss 2590  0iin 2596  iinun2 2599  iundif2 2600  iindif2 2601  iinuni 2605  iinpw 2607  iunpwss 2608  brab1 2650  sbcbrg 2652  dftr4 2675  nalset 2702  nvelv 2703  inex1g 2708  ssexg 2711  intex 2719  pwexg 2736  abssexg 2737  snex 2740  el 2741  rext 2744  sspwb 2745  unipw 2746  pwuni 2747  ssextss 2752  nnullss 2758  exss 2759  axpr 2768  zfpair2 2770  opthg 2778  opthgg 2779  eqvinop 2781  copsexg 2782  copsex4g 2784  opprc1b 2786  opth2 2789  moop2 2790  opabid 2799  pwin 2814  pwunss 2815  pwssun 2816  pwundif 2817  epel 2823  dfid3 2826  uniexg 2862  unexb 2864  opeluu 2869  uniuni 2870  euuni 2871  reucl 2875  reuunisn 2885  iunpw 2904  dffr2 2909  frirr 2914  fr2nr 2915  fr3nr 2916  wefrc 2933  onfr 2976  ordon 2977  ssorduni 2983  onint 2996  onminex 3010  hbsuc 3030  sucel 3032  sucidg 3042  ordpwsuc 3056  unon 3078  ordunisuc 3079  onuninsuc 3098  orduninsuc 3104  onzsl 3107  limsssuc 3111  limuni3 3113  dfom2 3123  elomg 3125  omsson 3126  limomss 3127  ordom 3131  peano5 3143  finds 3146  findsg 3147  finds2 3148  findes 3150  tfinds 3151  tfindsg 3152  tfindsg2 3153  tfindes 3154  tfinds2 3155  opelxp1 3195  opelxp 3204  opelxpg 3206  ralxp 3208  ralxpf 3210  elxp3 3214  elvv 3218  optocl 3225  onxpdisj 3231  ssxp 3246  xpsspw 3247  relopab 3256  opabid2 3257  inxp 3259  relop 3265  ididg 3268  opelcog 3279  cnvco 3289  dfrn2 3292  dfdm4 3294  eldm2g 3298  dmss 3299  breldmg 3305  dmun 3306  dmin 3307  dmuni 3308  dmsnsn0 3314  dmi 3315  dmsnop 3317  reldm0 3320  elreldm 3327  hbrn 3337  dmrnssfld 3343  dmcoss 3347  dmcosseq 3349  opelresg 3358  resieq 3360  dmres 3364  relssres 3376  resopab 3379  resiexg 3380  iss 3381  dfima2 3389  hbima 3395  csbima12g 3397  imadmrn 3398  imai 3401  elimasng 3411  args 3412  eliniseg 3413  iniseg 3414  dffr3 3415  intasym 3422  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  intirr 3427  cnvopab 3431  cnv0 3432  cnvi 3433  cnvsn 3435  elxp4 3439  elxp5 3440  cnvun 3441  cnvin 3442  rnuni 3445  dminss 3448  imainss 3449  cnvxp 3450  xpnz 3452  ssrnres 3467  rninxp 3468  dminxp 3469  dfrel2 3471  cores 3485  resco 3486  imaco 3487  rnco 3488  co02 3494  coi1 3496  coass 3498  relssdr 3499  cnvpo 3508  cnvso 3509  dffun2 3512  dffun6 3525  dffun7 3526  dffun8 3527  funsn 3529  funopg 3533  funco 3536  funssres 3538  funun 3540  funcnv2 3542  funcnv 3543  funcnv3 3544  fun2cnv 3545  fncnv 3547  funcnvuni 3550  imadif 3560  isarep1 3563  fneu 3578  2elresin 3584  fn0 3591  zfrep6 3600  fcoi1 3630  fcoi2 3631  feu 3632  fcnvres 3633  fabexg 3638  fconst 3643  fconstg 3644  f11 3649  fvprc 3706  fvex 3717  fv3 3718  tz6.12f 3723  tz6.12-2 3724  csbfv12g 3727  ndmfv 3730  funbrfv 3735  funopfvg 3737  fnbrfvb 3738  funbrfvbg 3742  fnopabfv 3743  fnrnfv 3744  dfimafn 3746  funimass4 3748  fvelima 3749  fnsnfv 3752  ssimaexg 3754  dmfco 3758  fvco 3759  fvopab4gf 3766  fvopabg 3770  fvopabn 3771  fvopabgf 3772  fvopabnf 3773  fvopab2 3776  eqfnfv 3782  funfvop 3788  fvelrn 3797  dff2 3802  dff3 3803  dffo4 3805  exfo 3807  fopabcos 3818  fsn 3819  fnressn 3822  fressnfv 3823  fvi 3827  funfvima3 3839  fvclss 3840  fvresex 3842  abrexexlem2 3844  abrexex 3845  abrexexg 3846  imaiun 3849  funiunfv 3851  abexssex 3857  f1fv 3859  f1ofveu 3867  cbvfo 3870  isomin 3884  isoini 3885  isofrlem 3886  f1oweALT 3891  tfrlem2 3897  tfrlem3 3898  tfrlem8 3903  tfrlem9 3904  tfrlem10 3905  tfrlem11 3906  tz7.44lem1 3912  rdg0t 3929  rdglim2 3934  tz7.48-1 3941  abianfplem 3946  csboprg 3971  eloprabg 3992  resoprab 3994  oprabval2gf 4011  oprabval5 4014  oprssdm 4027  caoprmo 4056  op1stg 4071  op2ndg 4072  1stval2 4073  2ndval2 4074  fo1st 4075  fo2nd 4076  f1stres 4077  f2ndres 4078  1st2val 4079  2nd2val 4080  2ndconst 4081  curry1 4082  sbcopeq1a 4095  csbopeq1a 4096  dfopab2 4097  dfoprab3 4098  dfoprab5 4099  dfoprab4 4100  df1st2 4110  df2nd2 4111  oacl 4154  omcl 4155  oecl 4156  oa0r 4157  om0r 4158  om1r 4161  oe1m 4163  oaordi 4164  oawordri 4168  oawordeulem 4172  oalimcl 4178  oaass 4179  oarec 4180  omordi 4181  omwordri 4187  omlimcl 4193  odi 4194  omass 4195  oen0 4197  oeordi 4198  oewordri 4203  oeworde 4204  oaabs 4236  omsmolem 4240  ider 4253  eqerlem 4254  erref 4259  erdmrn 4260  ecdmn0 4264  erthi 4265  erth 4266  erdisj 4270  elqsi 4275  0nelqs 4282  ecid 4284  qsid 4285  brecop 4290  ecopoprdm 4293  ecopoprsym 4294  ecopoprtrn 4295  ecopoprer 4296  th3qlem1 4298  mapprc 4310  fnmap 4313  mapvalg 4314  pmvalg 4315  mapval2 4319  map0 4328  mapsn 4329  ixpconst 4336  ss2ixp 4338  ixp0 4345  mapixp 4346  breng 4357  brdomg 4358  domen 4361  domeng 4362  idssen 4387  ener 4391  ensymg 4392  entrt 4395  domtr 4396  ensn1g 4406  en1 4407  fundmen 4409  mapsnen 4410  unen 4414  xpsnen 4415  xpsneng 4416  xpcomen 4419  xpcomeng 4420  xpassen 4421  xpdom2 4422  xpdom1g 4424  xpdom3 4425  pw2en 4426  sbth 4437  sbthcl 4439  fodomr 4463  canth2 4464  canth2g 4466  mapenlem1 4469  mapenlem2 4470  mapdom1 4472  mapdom2lem 4473  mapdom2 4474  mapunen 4482  pwen 4483  ssenen 4484  nneneq 4492  php 4493  php2 4494  php3 4495  0sdom1dom 4504  ominf 4508  pssnn 4513  ssfi 4515  domfi 4516  unbnn2 4522  isfinite2 4523  infcntss 4530  unifi 4532  fiint 4534  abfii2 4536  abfii3 4537  abfii4 4538  fodomfi 4540  pwfilem 4544  pwfi 4545  pm54.43 4546  suppr 4562  elirrv 4570  zfregfr 4573  en2lp 4574  inf0 4578  inf3lema 4581  inf3lemd 4584  inf3lem1 4585  inf3lem2 4586  inf3lem3 4587  inf3lem5 4589  inf3lem6 4590  inf3lem7 4591  inf3 4592  infeq5 4593  omex 4599  dfom3 4602  infensuc 4610  unbnnt 4611  zfregs 4619  setind2 4621  r1tr 4626  r1ord 4627  r1val1 4630  tz9.12lem1 4631  tz9.12lem3 4633  tz9.13 4635  tz9.13g 4636  rankwflem 4637  jech9.3 4638  rankvalg 4641  rankr1 4646  rankr1g 4647  r1val2 4650  rankval3 4653  bndrank 4654  ranklim 4657  r1pw 4658  r1pwcl 4659  rankuni2 4662  rankun 4663  rankonid 4667  rankr1id 4669  rankuni 4670  rankval4 4674  rankxplim 4684  rankxplim3 4686  rankxpsuc 4687  cp 4694  bnd2 4696  kardex 4697  karden 4698  aceq3lem 4704  aceq3 4705  aceq4 4706  aceq5lem1 4707  aceq5lem2 4708  aceq5lem3 4709  aceq5lem4 4710  aceq5lem5 4711  aceq5 4712  aceq6a 4713  aceq6b 4714  ac6lem 4726  ac6s 4728  ac9s 4736  kmlem1 4737  kmlem2 4738  kmlem4 4740  kmlem9 4745  kmlem10 4746  kmlem11 4747  kmlem12 4748  kmlem13 4749  numthlem 4755  numth2 4757  numthcor 4758  zorn2lem1 4760  zorn2lem7 4766  zornlem 4767  fodom 4770  fodomg 4771  brdom3 4773  brdom5 4774  brdom4 4775  brdom7disj 4776  brdom6disj 4777  unidomg 4781  cardval 4798  unxpdomlem 4815  unxpdom 4816  sucxpdom 4818  cardlim 4823  iscard2 4826  ondomon 4828  ondomcard 4829  carduni 4830  cardiun 4831  cardmin 4832  alephon 4837  alephcard 4839  alephordi 4846  cardaleph 4857  alephval2 4874  alephval3 4875  dominf 4876  cffnon 4879  cflim 4881  cardcf 4883  cfeq0 4886  cfsuc 4887  cfom 4888  cdavalt 4891  ltpiord 4987  indpi 5006  dmenq 5017  enqer 5018  addcmpblnq 5024  mulcmpblnq 5025  addpipq 5026  mulpipq 5027  ordpipq 5028  addcompq 5034  addasspq 5035  mulcompq 5036  mulasspq 5037  distrpqlem 5038  distrpq 5039  mulidpq 5041  recmulpq 5042  ltsopq 5047  ltapq 5048  ltmpq 5049  ltexpq 5052  ltexpq2 5053  halfpq 5054  nsmallpq 5055  ltbtwnpq 5056  ltrpq 5057  prnmadd 5072  genpv 5074  genpdm 5077  genpnnp 5080  genpcd 5081  genpnmax 5082  genpcl 5083  genpass 5084  1pr 5089  addclprlem1 5090  addclprlem2 5091  addclpr 5092  mulclprlem 5093  mulclpr 5094  addcompr 5095  addasspr 5096  mulcompr 5097  mulasspr 5098  distrlem1pr 5099  distrlem2pr 5100  distrlem4pr 5102  distrlem5pr 5103  1idpr 5105  prlem934a 5109  prlem934b 5110  prlem934 5111  ltaddpr 5112  ltexprlem1 5114  ltexprlem2 5115  ltexprlem3 5116  ltexprlem4 5117  ltexprlem6 5119  ltexprlem7 5120  ltexpri 5121  ltaprlem 5122  prlem936a 5125  prlem936 5127  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  reclem4pr 5131  recexpr 5132  suplem1pr 5133  suplem2pr 5134  dmenr 5147  enrer 5148  addcmpblnr 5153  mulcmpblnrlem 5154  addsrpr 5156  mulsrpr 5157  ltsrpr 5158  addcomsr 5168  addasssr 5169  mulcomsr 5170  mulasssr 5171  distrsr 5172  ltsosr 5175  0idsr 5178  1idsr 5179  ltasr 5181  recexsrlem 5184  mulgt0sr 5186  sqgt0sr 5187  recexsr 5188  map2psrpr 5192  suppsrlem 5193  suppsr 5194  suppsr2 5195  suppsr3 5196  supsrlem2 5198  supsrlem3 5199  supsrlem6 5202  ltresr 5230  supre 5232  ltsor 5233  axmulrcl 5246  axaddcom 5247  axmulcom 5248  axaddass 5249  axmulass 5250  axdistr 5251  axrrecex 5256  axcnre 5258  pre-axltadd 5261  pre-axmulgt0 5262  csbnegg 5336  ssxr 5513  peano2nn 5883  lbinfm 5995  dfinfmr 6014  infmsup 6015  infmxrcl 6033  dfuz 6150  ser1ft 6265  uzind4s 6384  dfseq0 6495  sumex 6919  dffsum 6936  fsum1f 6945  fsum1slem 6946  fsump1f 6949  csbfsum 6965  climfnn 7030  climeu 7037  climreu 7038  climmulc2 7065  iserzext 7071  caucvg3lem 7102  isumclimtf 7131  isumclim2tf 7133  isumshft 7139  isumshft2 7140  isumclt 7144  isumreclt 7145  isummulc1ALT 7148  infcvglem1 7156  fsum0diaglem2 7192  fsum0diag2 7194  efseq0ex 7253  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  xpnnen 7441  infxpidmlem1 7495  infxpidmlem4 7498  infxpidmlem5 7499  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem9 7503  infxpidmlem10 7504  infxpidmlem11 7505  infxpidmlem12 7506  unictb 7518  unctb 7519  infmap2lem1 7521  infmap2lem2 7522  infmap2 7523  tgval2t 7559  tgval3t 7567  eltg3t 7568  tgss3t 7580  basgent 7582  subbas 7586  subbas2 7587  subtop 7588  sn0top 7589  indistop 7590  distop 7591  fctop 7592  cctop 7594  ntrfval 7609  clsfval 7610  ntrval 7618  clsval 7619  clsval2 7627  neifval 7655  neif 7656  neival 7658  lpfval 7683  lpval 7684  islp2 7688  cncnplem2 7714  dfms2 7738  lmfval 7863  iscau 7874  metcld 7901  bopcnlem1 7915  bopcnlem3 7917  iscms2lem4 7926  cmsss 7931  cncms 7932  bcthlem13 7945  bcthlem32 7964  issubg 8053  nvvcop 8151  0vfval 8163  vsfval 8194  sqcn 8270  ipfval 8286  nmoubi 8367  ubthlem3 8462  ubthlem4 8463  minveclem10 8485  minveclem14 8489  psdmrn 8574  spwval2 8577  circgrp 8660  axgroth2 8717  axgroth3 8718  grothprim 8722  hhcmpl 8990  hhcms 8993  hlimreu 9031  hlimeu 9032  chcmh 9034  helch 9037  hsn0elch 9041  hhsscms 9067  occl 9097  projlem25 9126  projlem 9133  chintcl 9210  dfchj3 9240  spanun 9382  spansn 9396  osumlem4 9498  osumlem6 9500  osumlem7 9501  pjrn 9564  nmopubt 9749  nmfnleubt 9765  nmopunt 9854  nmcopexlem1 9866  nmcfnexlem1 9895  nlelch 9909  cnlnssadj 9928  adjbd1o 9933  branmfnt 9951  bra11 9954  pjnmop 9986  hmopidmch 9990  pjhmopidm 10020  ghomgrplem 10294  symggrp 10315  cayleythlem 10320  ntunte 10340  uninqs 10342  elo 10345  infi1 10347  fine 10348  abfi 10349  stcat 10353  ficli 10368  fiv 10374  mapudiscn 10399  hmphsyma 10415  hmpher 10423  hmeogrp 10425  homcard 10426  subsp 10429  qusp 10430  oefil2 10441  fgsb 10444  infi 10448  fgsb2 10449  cnfilca 10451  dtopcl 10459  dtt2 10462  eloi 10503  ishomd 10562  blkssatm 10603
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803
Copyright terms: Public domain