Theorem visset 1350

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

Assertion

Ref	Expression
visset	⊢ x ∈ V

Proof of Theorem visset

Step	Hyp	Ref	Expression
1		cleqid 1102	. 2 ⊢ x = x
2		df-v 1349	. . 3 ⊢ V = {x∣x = x}
3	2	cleqabi 1176	. 2 ⊢ (x ∈ V ↔ x = x)
4	1, 3	mpbir 165	1 ⊢ x ∈ V

Syntax hints:   = weq 797   ∈ wcel 1092  Vcvv 1348

This theorem is referenced by:  isset 1351  ralv 1357  rexv 1358  rabab 1359  eqvinc 1407  ceqex 1410  cbvab 1423  moeq3 1432  mo2icl 1434  vsbcint 1438  sbc2or 1454  elabs2 1457  axrep 1473  axrep2 1474  zfaus 1480  bm1.3ii 1481  nalset 1482  nvelv 1483  ddif 1597  dfun2 1668  dfin2 1669  difab 1693  inex1g 1699  ssexg 1702  disj2 1735  0ex 1745  zfnul 1746  elpwg 1802  hbpw 1804  pwexg 1807  hbpr 1824  dftp2 1835  snssg 1850  prss 1854  tpss 1855  prsspw 1858  snex 1859  el 1860  rext 1862  sspwb 1863  ssextss 1864  nnullss 1880  exss 1881  pwv 1884  opthg 1899  eqvinop 1901  copsexg 1902  copsex4g 1904  opprc1b 1906  opth2 1909  moop2 1910  pwin 1915  pwunss 1916  pwssun 1917  unpr 1930  unisng 1933  uniexg 1948  unexb 1950  opeluu 1953  euuni 1954  reucl 1957  unipw 1960  pwuni 1961  elintg 1973  elinti 1974  hbint 1975  intss1 1979  ssint 1980  intmin 1982  intss 1983  intmin2 1984  intex 1986  intun 1989  intpr 1990  iuniin 2001  dfiun2 2014  dfiin2 2015  ssiin 2024  iinss 2025  iinun2 2031  iundif2 2032  iindif2 2033  iinuni 2036  iinpw 2038  iunpwss 2039  iunpw 2040  dftr4 2046  brab1 2096  opabid 2099  epel 2124  dffr2 2171  frirr 2176  fr2nr 2177  fr3nr 2178  wefrc 2195  onfr 2237  ordon 2238  ssorduni 2249  onint 2261  onminex 2275  hbsuc 2294  sucel 2296  sucidg 2305  onpwsuc 2315  unon 2338  ordunisuc 2339  onuninsuc 2356  limsssuc 2362  orduninsuc 2365  onzsl 2367  dfom2 2374  elomg 2376  omsson 2377  limomss 2378  ordom 2382  peano5 2394  finds 2397  findsg 2398  finds2 2399  findes 2400  tfinds 2401  tfindsg 2402  tfindsg2 2403  tfindes 2404  tfinds2 2405  opelxpex 2445  opelxp 2452  opelxpg 2454  ralxp 2456  elxp3 2460  elvv 2464  optocl 2469  cbvop 2473  onxpdisj 2476  ssxp 2487  xpex 2488  xpexg 2489  relopab 2494  inxp 2496  opelcog 2511  cnvco 2520  dfrn2 2523  dfdm4 2525  eldmg 2529  dmss 2530  dmun 2536  dmin 2537  dmuni 2538  dmsnsn0 2544  dmi 2545  dmsnop 2547  reldm0 2550  elreldm 2554  hbrn 2564  dmco 2570  dmcosseq 2572  resieq 2581  dmres 2584  relssres 2596  resopab 2598  iss 2599  dfima2 2604  hbima 2609  imadmrn 2610  imai 2613  eliniseg 2618  iniseg 2619  dffr3 2620  intasym 2627  intirr 2628  cnvopab 2632  cnv0 2633  cnvi 2634  cnvsn 2636  elxp4 2640  elxp5 2641  cnvun 2642  cnvin 2643  rnuni 2646  dminss 2648  imainss 2649  imaiun 2650  cnvxp 2651  cores 2659  dfrel2 2660  co02 2663  coi1 2665  coass 2667  relssdr 2668  dmco2 2673  dffun2 2674  dffun6 2687  dffun7 2688  funsn 2690  funco 2696  funssres 2698  funun 2700  funcnv2 2702  funcnv 2703  fun2cnv 2704  funcnvuni 2706  imadif 2714  fneu 2728  2elresin 2733  fn0 2739  zfrep6 2744  fcoi1 2765  fcoi2 2766  feu 2767  fcnvres 2768  fconst 2774  fconstg 2775  f11 2780  fvprc 2829  fvex 2838  fv3 2839  tz6.12f 2844  tz6.12-2 2845  ndmfv 2848  funbrfv 2852  funopfvg 2854  fnfvbr 2855  fnopabfv 2858  fvelima 2859  fniunfv 2860  fnsnfv 2861  dmfco 2864  fvco 2865  fvopabg 2872  fvopabn 2873  fvopabgf 2874  fvopabnf 2875  fvopab2 2878  cleqfv 2880  fvelrn 2883  funopfv 2886  fvrn 2888  fsn 2895  fnressn 2897  fressnfv 2898  fvi 2900  funfvima3 2906  fvclss 2907  fvresex 2909  abrexexlem2 2911  abrexex 2912  abrexexg 2913  f1fv 2916  cbvfo 2923  isoid 2933  isomin 2937  isoini 2938  isofrlem 2939  f1oweOLD 2944  tfrlem2 2950  tfrlem3 2951  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  tz7.44lem1 2965  rdgzert 2982  rdglim2 2987  tz7.48-1 2994  abianfplem 2999  eloprabg 3035  oprssdm 3056  caoprmo 3084  fo1st 3094  fo2nd 3095  f1stres 3096  1st2val 3097  df1st2 3098  oacl 3138  omcl 3139  oecl 3140  oa0r 3141  om0r 3142  om1r 3145  oe1m 3147  oaordi 3148  oawordri 3152  oawordeulem 3156  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  omsmolem 3195  ider 3208  erref 3212  erdmrn 3213  ecdmn0 3217  erthi 3218  erth 3219  erdisj 3223  elqsi 3228  0nelqs 3234  ecid 3236  qsid 3237  brecop 3242  ecopoprdm 3245  ecopoprsym 3246  ecopoprtrn 3247  ecopoprer 3248  th3qlem1 3250  mapprc 3260  fnmap 3262  mapvalg 3263  map0 3268  mapsn 3269  breng 3280  brdomg 3281  domen 3284  domeng 3285  idssen 3309  ener 3313  ensymg 3316  entrt 3319  domtr 3320  ensn1g 3330  en1 3331  fundmen 3333  mapsnen 3334  en2sn 3336  snfi 3337  unen 3338  xpsnen 3339  xpsneng 3340  xpcomen 3343  xpassen 3344  xpdom2 3345  xpdom3 3347  pw2en 3348  sbth 3359  sbthcl 3361  canth2 3381  canth2g 3382  mapenlem1 3384  mapenlem2 3385  mapdom1 3387  mapdom2lem 3388  mapdom2 3389  mapunen 3397  ssenen 3399  limenpsi 3400  nneneq 3408  php 3409  php2 3410  php3 3411  0sdom1dom 3420  ominf 3423  pssnn 3428  ssfi 3430  unbnn2 3436  isfinite2 3437  infcntss 3443  fiint 3445  eirrv 3449  zfregfr 3452  en2lp 3453  inf0 3457  inf3lema 3460  inf3lemd 3463  inf3lem1 3464  inf3lem2 3465  inf3lem3 3466  inf3lem5 3468  inf3lem6 3469  inf3lem7 3470  inf3 3471  inf5 3472  omex 3475  dfom3 3477  infensuc 3484  zfregs 3491  setind2 3493  r1tr 3498  r1ord 3499  r1val1 3502  tz9.12lem1 3503  tz9.12lem3 3505  tz9.13 3507  tz9.13g 3508  rankwflem 3509  jech9.3 3510  rankvalg 3513  rankr1 3518  rankr1g 3519  r1val2 3522  rankval3 3525  bndrank 3526  r1pw 3529  r1pwcl 3530  rankuni 3533  rankun 3535  rankonid 3538  rankr1id 3539  ranklon 3540  cp 3547  bnd2 3549  kardex 3550  karden 3551  aceq3lem 3555  aceq3 3556  aceq4 3557  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  aceq5lem4 3561  aceq5lem5 3562  aceq5 3563  aceq6a 3564  aceq6b 3565  ac6lem 3575  ac6s 3577  kmlem1 3580  kmlem2 3581  kmlem4 3583  kmlem8 3587  kmlem9 3588  kmlem10 3589  kmlem11 3590  kmlem12 3591  numthlem 3598  numth2 3600  numthcor 3601  zornlem1 3603  zornlem7 3609  zorn2lem 3610  fodom 3613  fodomg 3614  fodomb 3615  cardval 3633  unxpdomlem 3649  unxpdom 3650  sucxpdom 3652  cardlim 3657  iscard2 3660  ondomon 3662  ondomcard 3663  carduni 3664  cardiun 3665  cardmin 3666  alephon 3671  alephcard 3673  alephordi 3679  cardaleph 3690  cffnon 3702  cflim 3704  cardcf 3706  cfsuc 3709  cfom 3710  cdavalt 3716  zfcndrep 3760  ltpiord 3809  indpi 3828  dmenq 3839  enqer 3840  addcmpblnq 3846  mulcmpblnq 3847  addpipq 3848  mulpipq 3849  ordpipq 3850  addcompq 3856  addasspq 3857  mulcompq 3858  mulasspq 3859  distrpqlem 3860  distrpq 3861  mulidpq 3863  recmulpq 3864  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  ltexpq2 3875  halfpq 3876  nsmallpq 3877  ltbtwnpq 3878  ltrpq 3879  prnmadd 3894  genpv 3896  genpdm 3899  genpnnp 3902  genpcd 3903  genpnmax 3904  genpcl 3905  genpass 3906  1pr 3911  addclprlem1 3912  addclprlem2 3913  addclpr 3914  mulclprlem 3915  mulclpr 3916  addcompr 3917  addasspr 3918  mulcompr 3919  mulasspr 3920  distrlem1pr 3921  distrlem2pr 3922  distrlem4pr 3924  distrlem5pr 3925  1idpr 3927  prlem934a 3931  prlem934b 3932  prlem934 3933  ltaddpr 3934  ltexprlem1 3936  ltexprlem2 3937  ltexprlem3 3938  ltexprlem4 3939  ltexprlem6 3941  ltexprlem7 3942  ltexpri 3943  ltaprlem 3944  prlem936a 3947  prlem936 3949  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  recexpr 3954  suplem1pr 3955  suplem2pr 3956  dmenr 3969  enrer 3970  addcmpblnr 3975  mulcmpblnrlem 3976  addsrpr 3978  mulsrpr 3979  ltsrpr 3980  addcomsr 3990  addasssr 3991  mulcomsr 3992  mulasssr 3993  distrsr 3994  ltsosr 3997  0idsr 4000  1idsr 4001  ltasr 4003  recexsrlem 4006  mulgt0sr 4008  sqgt0sr 4009  recexsr 4010  map2psrpr 4014  suppsrlem 4015  suppsr 4016  suppsr2 4017  suppsr3 4018  supsrlem2 4020  supsrlem3 4021  supsrlem6 4024  ltresr 4052  supre 4054  ltsor 4055  axmulrcl 4069  axaddcom 4070  axmulcom 4071  axaddass 4072  axmulass 4073  axdistr 4074  axrecex 4079  axrrecex 4081  axltadd 4085  axmulgt0 4086  axcnre 4087  peano2nn 4433  nnind 4434  seqval 4665  xpnnen 4927  infxpidmlem1 4933  infxpidmlem4 4936  infxpidmlem5 4937  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem9 4941  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infmap2lem1 4951  infmap2lem2 4952  infmap2 4953  hlimreu 5145  hlimeu 5146  chcmh 5148  helch 5151  hsn0elch 5155  ocvalt 5161  occl 5188  projlem25 5217  projlem 5224  chintcl 5296  spanvalt 5300  hsupval2t 5301  sshjvalt 5321  dfchj3 5326  sshjval3t 5327  spanun 5450  spansn 5462  hosmvalt 5487  hodmvalt 5488  osumlem4 5533  osumlem6 5535  osumlem7 5536  pjrn 5587

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org