Theorem visset 2295

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

Assertion

Ref	Expression
visset	|- x e. _V

Proof of Theorem visset

Step	Hyp	Ref	Expression
1		eqid 1884	. 2 |- x = x
2		df-v 2294	. . 3 |- _V = {x | x = x}
3	2	abeq2i 2001	. 2 |- (x e. _V <-> x = x)
4	1, 3	mpbir 207	1 |- x e. _V

Syntax hints:   = wceq 1298   e. wcel 1300  _Vcvv 2292

This theorem is referenced by:  isset 2296  ralv 2305  rexv 2306  reuv 2307  rabab 2308  rababOLD 2309  eqvincOLD 2388  ceqex 2391  ralab 2417  moeq3 2432  mo2icl 2434  moi2 2435  moi 2436  reu8 2448  sbhypf 2452  sbc2or 2481  sbccomg 2526  sbcralt 2527  sbcralgf 2529  sbcel12gOLD 2553  sbceqdigOLD 2555  csbvarg 2564  csbhypf 2572  csbiegft 2573  csbnestg 2581  csbabg 2588  csbabgOLD 2589  uniiunlem 2693  ddif 2737  dfun2 2829  dfin2 2830  difabOLD 2864  vn0 2882  eqv 2890  elpwg 3038  hbpw 3041  dftp2 3075  hbpr 3076  ralprg 3078  ralprOLD 3080  ralprOLDOLD 3081  raltp 3083  snssg 3124  difprsn 3127  difprsnOLD 3128  prssOLD 3139  prssgOLD 3141  tpssOLD 3146  prsspwOLD 3151  pwpr 3174  pwv 3176  unipr 3191  uniprg 3192  unisng 3194  reucl 3213  elintg 3222  elintiOLD 3224  hbint 3225  hbintOLD 3226  elintrabg 3229  intss1 3231  ssint 3232  intmin 3237  intminOLD 3238  intss 3239  intssuni 3240  intmin4 3246  intab 3247  intun 3249  intpr 3250  intprg 3251  uniintsn 3253  iuniin 3264  iuniinOLD 3265  iinss1 3268  dfiun2gOLD 3284  dfiin2g 3286  dfiin2 3287  dfiin2OLD 3288  ssiin 3302  ssiinOLD 3303  iinss 3304  iinssOLD 3305  0iin 3313  iinun2 3321  iundif2 3322  iindif2 3324  iinxsng 3325  iinxprg 3326  iinuni 3330  sspwuni 3333  iinpw 3336  iunpwss 3337  brab1OLD 3385  sbcbrg 3390  sbcbrgOLD 3391  trint 3426  trintss 3427  nalset 3448  vprc 3449  inex1g 3454  ssexg 3457  intex 3465  inuni 3470  axpweq 3480  pwexg 3489  abssexgOLD 3491  snexOLD 3493  elALT 3494  rext 3502  sspwb 3503  unipw 3504  pwuni 3505  ssextss 3507  nnullss 3515  exss 3516  axpr 3523  zfpair2 3525  opthg 3533  opthgg 3534  eqvinop 3536  copsexg 3537  copsexgOLD 3538  copsex4g 3540  opprc1b 3542  opth2 3546  moop2 3548  opabidOLD 3558  opelopabsb 3564  pwin 3576  pwunss 3577  pwssun 3578  pwundif 3579  epel 3585  dfid3 3587  posn 3603  dffr2OLD 3628  frirr 3634  fr2nr 3635  wefrc 3652  tron 3681  onfr 3702  hbsuc 3736  sucel 3738  sucidgOLD 3748  suctr 3751  uniexg 3795  unexb 3797  snnex 3801  opeluu 3805  uniuni 3806  euuni 3807  reuunisn 3822  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq2 3829  eufromeq4 3831  eufromeq6 3833  iunpw 3858  fr3nr 3859  ssorduniOLD 3871  onint 3876  onminex 3888  ordpwsuc 3896  unon 3910  ordunisuc 3911  ordunisucOLD 3912  onuninsuci 3921  orduninsuc 3925  onzslOLD 3929  limsssuc 3934  limuni3 3936  tfinds 3942  tfindsOLD 3943  tfindsg 3944  tfindsg2 3945  tfindes 3946  tfinds2 3947  dfom2 3951  elomg 3953  omssonOLD 3955  limomss 3956  ordom 3960  ordomOLD 3961  peano5 3975  finds 3979  findsg 3980  finds2 3981  findes 3983  opelxp1 4026  opelxpOLD 4037  opelxpg 4039  ralxp 4041  ralxpf 4043  elxp3 4049  elvv 4053  elvvv 4054  optocl 4061  0nelelxp 4067  onxpdisjOLD 4069  xpss12 4089  xpss12OLD 4090  xpsspw 4093  relopab 4104  opabid2 4107  inxpOLD 4110  relop 4113  ididgOLD 4118  opelco2g 4133  cnvco 4145  cnvcoOLD 4146  dfrn2 4149  dfdm4 4151  eldm2g 4155  dmss 4156  breldmg 4162  dmunOLD 4164  dmin 4165  dmuni 4166  dm0 4170  dmi 4172  dmiOLD 4173  reldm0 4176  elreldm 4185  hbrn 4198  hbrnOLD 4199  dmrnssfld 4205  dmcoss 4211  dmcossOLD 4212  dmcosseq 4214  dmcosseqOLD 4215  opelresg 4224  resieq 4227  dmres 4234  relssres 4248  resopab 4252  resiexg 4253  iss 4254  issOLD 4255  dfima2 4265  dfima2OLD 4266  hbimaOLD 4274  csbima12g 4276  imadmrn 4277  imai 4280  elimasng 4291  args 4293  elinisegOLD 4295  iniseg 4296  dffr3 4297  cotr 4302  cnvsym 4304  intasym 4306  intasymOLD 4307  asymref 4308  asymrefOLD 4309  asymref2OLD 4311  intirr 4312  intirrOLD 4313  cnvopab 4317  cnvopabOLD 4318  cnv0 4319  cnvi 4320  cnviOLD 4321  cnvunOLD 4323  cnvin 4324  rnuni 4327  dminss 4330  imainss 4331  cnvxpOLD 4333  xpnz 4335  ssrnres 4354  rninxp 4355  rninxpOLD 4356  dminxp 4357  dfrel2 4358  dmsnn0 4362  dmsnop 4367  dmsnopOLD 4368  cnvsn 4373  elxp4 4379  elxp5 4380  dfco2 4393  dfco2a 4394  dfco2aOLD 4395  coundiOLD 4397  coundirOLD 4399  cores 4400  coresOLD 4401  resco 4402  imaco 4403  rnco 4404  coiun 4407  co02 4411  coi1 4413  coass 4415  relssdmrn 4416  cnvpo 4427  cnvso 4428  dffun2 4431  dffun7 4447  dffun8 4448  dffun8OLD 4449  dffun9 4450  funopg 4454  funcoOLD 4458  funssres 4460  funun 4462  funsn 4463  funsnOLD 4464  funsng 4465  funcnv2 4474  funcnv 4475  funcnv3 4476  fun2cnv 4477  fncnv 4479  funcnvuni 4482  imadif 4493  isarep1 4497  isarep1OLD 4498  fneu 4517  fneuOLD 4518  2elresin 4524  fn0OLD 4533  iunfopabOLD 4543  zfrep6 4545  fcoi1OLD 4585  fcoi2OLD 4587  feu 4588  fcnvres 4589  fabexg 4596  fconstOLD 4603  fconstg 4604  dff12 4609  fv2 4676  fvprc 4678  fvex 4689  fv3 4690  tz6.12f 4695  tz6.12-2 4696  csbfv12g 4699  ndmfv 4702  nfunsn 4706  funbrfv 4709  funopfvg 4711  fnbrfvb 4712  funbrfvbg 4716  dffn5 4717  fnrnfv 4718  dfimafn 4720  funimass4 4722  fvelimaOLD 4724  fnsnfv 4728  ssimaexg 4730  dffv2 4734  dmfco 4735  fvco 4736  fvopab4gf 4744  fvopabg 4748  fvopabn 4749  fvopabgf 4750  fvopabnf 4751  fvopab2 4754  eqfnfv 4766  funfvop 4776  fvelrn 4785  dff3 4790  dff4 4791  dffo4 4793  exfo 4795  fopabcos 4806  fsn 4807  fnressn 4812  fressnfv 4813  fvi 4818  funfvima3 4830  fvclss 4831  fvresex 4833  abrexexlem2 4835  abrexex 4836  abrexexg 4837  imaiun 4840  funiunfv 4842  abexssex 4848  dff13 4850  f1ofveu 4858  cbvfo 4861  isomin 4876  isoini 4877  isofrlem 4878  f1oweALT 4883  csboprg 4910  csboprgOLD 4911  eloprabg 4936  resoprab 4938  oprabval2gf 4955  oprabval5 4958  oprabval4gALT 4961  oprssdm 4975  caoprmo 5003  op1stg 5028  op2ndg 5029  1stval2 5030  2ndval2 5031  fo1st 5032  fo2nd 5033  f1stres 5034  f2ndres 5035  fo1stres 5036  fo2ndres 5037  1st2val 5038  2nd2val 5039  sbcopeq1a 5051  csbopeq1a 5052  dfopab2 5053  dfoprab3 5054  dfoprab4s 5056  dfoprab5s 5057  dfoprab5sf 5058  df1st2 5068  df2nd2 5069  1stconst 5070  2ndconst 5071  curry1 5075  curry2 5078  fparlem1 5081  fparlem2 5082  fparlem3 5083  fparlem4 5084  fpar 5085  fsplit 5086  uniabio 5095  iotaval 5096  onopruni 5117  onopriun 5118  tfrlem2 5120  tfrlem3 5121  tfrlem8 5126  tfrlem9 5127  tfrlem10 5128  tfrlem11 5129  tz7.44lem1 5135  rdg0g 5152  rdglim2 5157  frsucmpt 5163  tz7.48-1 5165  abianfplem 5170  oacl 5215  omcl 5216  omclOLD 5217  oecl 5218  oeclOLD 5219  oa0r 5220  om0r 5221  om1r 5224  oe1m 5226  oaordi 5227  oawordri 5232  oawordeulem 5236  oalimcl 5242  oaass 5243  oarec 5244  omordi 5245  omwordri 5251  omlimcl 5257  odi 5258  omass 5259  oen0 5261  oeordi 5262  oewordri 5267  oeworde 5268  oeoalem 5271  oeoelem 5273  oaabs 5309  omsmolem 5313  iderOLD 5327  eqerlem 5328  erref 5333  erdmrn 5334  ecdmn0 5338  erthi 5339  erth 5340  erdisj 5344  elqsi 5349  uniqs 5354  0nelqs 5357  ecid 5359  qsid 5360  brecop 5365  ecopoprdm 5368  ecopoprsym 5369  ecopoprtrn 5370  ecopoprer 5371  th3qlem1 5373  mapprc 5385  fnmap 5388  mapvalg 5389  pmvalg 5390  mapval2 5394  map0 5403  mapsn 5404  ixpconst 5411  ss2ixp 5413  ixp0 5420  mapixp 5421  breng 5434  brdomg 5435  domen 5438  domeng 5439  idssen 5465  ener 5469  ensymg 5470  entr 5473  domtr 5474  ensn1g 5484  en1 5485  fundmen 5487  mapsnen 5488  unen 5493  xpsnen 5494  xpsneng 5495  xpcomen 5498  xpcomeng 5499  xpassen 5500  xpdom2 5501  xpdom1g 5503  xpdom3 5504  pw2en 5505  ac6sfilem3 5508  ac6sfi 5509  sbth 5520  sbthcl 5522  fodomr 5547  canth2 5548  canth2g 5549  riotav 5565  mapenlem1 5583  mapenlem2 5584  mapdom1 5586  mapdom2lem 5587  mapdom2 5588  mapunen 5596  pwen 5597  ssenen 5598  nneneq 5606  php 5607  php2 5608  php3 5609  0sdom1dom 5618  ominf 5622  pssnn 5628  ssfi 5630  domfi 5631  xpfi 5632  unbnn2 5638  isfinite2 5639  infcntss 5646  unifi 5648  fiint 5650  abfii2 5652  abfii3 5653  abfii4 5654  fodomfi 5656  pwfilem 5660  pwfi 5661  pm54.43 5662  suppr 5680  ordtypelem1 5684  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  hartog 5693  onsdom 5694  elirrv 5700  zfregfr 5706  en2lp 5707  inf0 5712  inf3lema 5715  inf3lemd 5718  inf3lem1 5719  inf3lem2 5720  inf3lem3 5721  inf3lem5 5723  inf3lem6 5724  inf3lem7 5725  inf3 5726  infeq5 5727  omex 5733  dfom3 5737  infensuc 5745  unbnn3 5746  zfregs 5754  setind2 5760  r1tr 5765  r1ord 5766  r1val1 5769  tz9.12lem1 5770  tz9.12lem3 5772  tz9.13 5774  tz9.13g 5775  rankwflem 5776  jech9.3 5777  rankvalg 5780  rankr1 5785  rankr1g 5786  r1val2 5789  rankval3 5792  bndrank 5793  ranklim 5796  r1pw 5797  r1pwcl 5798  rankuni2 5801  rankun 5802  rankonid 5806  rankr1id 5808  rankuni 5809  rankval4 5813  rankxplim 5823  rankxplim3 5825  rankxpsuc 5826  cp 5852  bnd2 5854  kardex 5855  karden 5856  alephon 5876  omsubsuc2 5878  omsubsdomlem2 5880  elomsubsd 5885  omsublim 5887  infenomsub 5889  aceq3lem 5894  aceq3 5895  aceq4 5896  aceq5lem1 5897  aceq5lem2 5898  aceq5lem3 5899  aceq5lem4 5900  aceq5lem5 5901  aceq5 5902  aceq6a 5903  aceq6b 5904  ac6lem 5916  ac6s 5918  ac9s 5926  kmlem1 5927  kmlem2 5928  kmlem4 5930  kmlem9 5935  kmlem10 5936  kmlem11 5937  kmlem12 5938  kmlem13 5939  numthlem 5945  numth2 5947  numthcor 5948  zorn2lem1 5950  zorn2lem7 5956  zornlem 5957  fodom 5960  fodomg 5961  brdom3 5963  brdom5 5964  brdom4 5965  brdom7disj 5966  brdom6disj 5967  unidomg 5971  cardval 5975  unxpdomlem 5995  unxpdom 5996  sucxpdom 5998  cardlim 6003  iscard2 6006  ondomon 6008  ondomcard 6009  carduni 6010  cardiun 6011  cardmin 6012  alephcard 6015  alephordi 6022  cardaleph 6033  alephval2 6050  alephval3 6051  dominf 6052  cffnon 6055  cflim 6057  cardcf 6059  cfeq0 6062  cfsuc 6063  cfom 6064  cdaval 6067  cdaung 6071  cdaeng 6074  nnacda 6088  ltpiord 6167  indpi 6186  dmenq 6197  enqer 6198  addcmpblnq 6204  mulcmpblnq 6205  addpipq 6206  mulpipq 6207  ordpipq 6208  addcompq 6214  addasspq 6215  mulcompq 6216  mulasspq 6217  distrpqlem 6218  distrpq 6219  mulidpq 6221  recmulpq 6222  ltsopq 6227  ltapq 6228  ltmpq 6229  ltexpq 6232  ltexpq2 6233  halfpq 6234  nsmallpq 6235  ltbtwnpq 6236  ltrpq 6237  prnmadd 6252  genpv 6254  genpdm 6257  genpnnp 6260  genpcd 6261  genpnmax 6262  genpcl 6263  genpass 6264  1pr 6269  addclprlem1 6270  addclprlem2 6271  addclpr 6272  mulclprlem 6273  mulclpr 6274  addcompr 6275  addasspr 6276  mulcompr 6277  mulasspr 6278  distrlem1pr 6279  distrlem2pr 6280  distrlem4pr 6282  distrlem5pr 6283  1idpr 6285  prlem934a 6289  prlem934b 6290  prlem934 6291  ltaddpr 6292  ltexprlem1 6294  ltexprlem2 6295  ltexprlem3 6296  ltexprlem4 6297  ltexprlem6 6299  ltexprlem7 6300  ltexpri 6301  ltaprlem 6302  prlem936a 6305  prlem936 6307  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  reclem4pr 6311  recexpr 6312  suplem1pr 6313  suplem2pr 6314  dmenr 6327  enrer 6328  addcmpblnr 6333  mulcmpblnrlem 6334  addsrpr 6336  mulsrpr 6337  ltsrpr 6338  addcomsr 6348  addasssr 6349  mulcomsr 6350  mulasssr 6351  distrsr 6352  ltsosr 6355  0idsr 6358  1idsr 6359  ltasr 6361  recexsrlem 6364  mulgt0sr 6366  sqgt0sr 6367  recexsr 6368  map2psrpr 6372  suppsrlem 6373  suppsr 6374  suppsr2 6375  suppsr3 6376  supsrlem2 6378  supsrlem3 6379  supsrlem6 6382  ltresr 6410  supre 6412  ltsor 6413  axmulrcl 6427  axaddcom 6428  axmulcom 6429  axaddass 6430  axmulass 6431  axdistr 6432  axrrecex 6437  axcnre 6439  pre-axltadd 6442  pre-axmulgt0 6443  csbneggOLD 6521  renfdisj 6712  ssxrOLD 6715  peano2nn 7118  lbinfm 7257  dfinfmr 7276  infmsup 7277  infmxrcl 7295  dfuzi 7414  uzind4s 7621  fzpr 7685  seq1lem1 7722  ser1f 7741  dfseq0 7806  hashgval 8230  sumex 8241  dffsum 8258  fsum1fi 8267  fsum1slem 8268  fsump1fi 8271  csbfsum 8287  climfnn 8352  climeu 8360  climreu 8361  climmulc2 8389  iserzex 8395  caucvg3lem 8426  isumclimtfi 8456  isumclim2f 8459  isumshfti 8465  isumshft2i 8466  isumcl 8470  isumrecl 8471  isummulc1iALT 8474  infcvglem1 8482  fsum0diaglem2 8519  fsum0diag2 8521  efseq0ex 8573  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  xpnnen 8768  infxpidmlem1 8821  infxpidmlem4 8824  infxpidmlem5 8825  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem9 8829  infxpidmlem10 8830  infxpidmlem11 8831  infxpidmlem12 8832  infpss 8843  unictb 8845  unctb 8846  infmap2lem1 8848  infmap2lem2 8849  infmap2 8850  tgval2 8887  tgval3 8895  eltg3 8896  tgss3 8908  basgen 8910  subbas 8914  subbas2 8915  subtop 8916  sn0top 8917  indistop 8918  distop 8919  fctop 8920  cctop 8922  txbas 8933  txuni 8935  ntrfval 8943  clsfval 8944  ntrval 8952  clsval 8953  clsval2 8961  neifval 8990  neif 8991  neival 8993  lpfval 9018  lpval 9019  islp2 9023  cncnplem2 9052  dfms2 9076  lmfval 9203  iscau 9214  iscaunns 9222  metcls 9244  metcld 9245  bopcnlem1 9259  bopcnlem3 9261  iscms2lem4 9270  cmsss 9275  cncms 9276  bcthlem13 9289  bcthlem32 9308  gx1 9385  gxnn0suc 9387  issubg 9425  gaid 9454  ssga 9455  gapmlem 9461  gapm 9462  nvvcop 9545  vsfval 9586  vacnlem5 9671  vacnlem6 9672  sqcn 9674  ipfval 9691  nmoubi 9774  ubthlem3 9874  ubthlem4 9875  minveclem10 9899  minveclem14 9903  psdmrn 9991  spwval2 9996  spwpr2 10001  circgrp 10094  axgroth5 10132  axgroth2 10133  grothpw 10134  grothpwex 10135  axgroth6 10137  axgroth3 10138  grothprim 10141  xp1st 10155  xp2nd 10156  oprabopabf 10157  dif1en 10172  dif1enOLD 10173  indexfi 10174  findcard 10178  findcardOLD 10179  fixp 10180  fiv 10212  fine 10213  abfi 10215  fiuni 10219  fibas 10221  hausnei2 10222  uptx 10226  txcn 10227  subsp 10244  subspid 10249  subtopmet 10256  isfbas2 10263  oefil2 10275  fbssint 10279  infi 10280  fsubbas 10281  fbunfip 10282  elfg 10284  filrn 10293  sfvlim 10296  hausfillim 10303  filmapf 10307  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  cncomp 10331  comptoppr 10332  fintopcomp 10333  usinuniop 10341  tosdir 10358  on1el3 10412  on1el4 10413  axhcompl 10500  hhcmpl 10702  hhcms 10705  hlimreui 10743  hlimeui 10744  chcmhi 10746  helch 10749  hsn0elch 10753  hhsscms 10783  occli 10814  projlem25 10843  projlem 10850  chintcli 10928  dfchj3 10958  spanuni 11100  spansni 11113  osumlem4 11216  osumlem6 11218  osumlem7 11219  pjrni 11282  nmopub 11469  nmfnleub 11486  nmopun 11576  nmcopexlem1 11588  nmcfnexlem1 11617  nlelchi 11631  cnlnssadj 11650  adjbd1o 11655  branmfn 11675  branmfnOLD 11676  bra11 11679  pjnmopi 11719  hmopidmchi 11723  pjhmopidm 11754  bnj33 12401  bnj33OLD 12402  bnj112 12457  bnj136 12468  bnj210 12502  bnj214 12508  bnj219 12510  bnj220 12511  bnj610 12564  bnj879 12806  bnj880 12807  bnj918 12826  bnj922 12834  bnj927 12835  bnj963 12857  bnj971 12860  bnj1098 12917  bnj1379 13100  bnj64 13201  bnj82 13210  bnj98 13221  bnj149 13241  bnj522 13261  bnj535 13265  bnj556 13280  bnj557 13281  bnj606 13293  bnj591 13299  bnj594 13300  bnj580 13301  bnj607 13304  bnj609 13306  bnj600 13308  bnj891 13321  bnj889 13323  bnj908 13329  bnj934 13334  bnj944 13340  bnj950 13342  bnj964 13347  bnj910 13353  bnj986 13360  bnj999 13365  bnj1018 13378  bnj907 13381  bnj1040 13388  bnj1041 13389  bnj1042 13390  bnj1043 13391  bnj1045 13392  bnj1052 13395  bnj1069 13400  bnj1073 13403  bnj1081 13407  bnj1084 13409  bnj1099 13413  bnj1133 13426  bnj1134 13427  bnj1145 13431  bnj1421 13532  bnj1498 13562  ifexg 13599  fseq1cl 13619  ghomgrplem 13632  symggrp 13640  cayleythlem 13645  gcdcllem2 13719  gcdcllem3 13720  eucalgf 13751  eucalglt 13753  isprm2lem 13774  isprm2 13775  trintOLD 13794  trintssOLD 13795  untsucf 13798  sneqrg 13822  elres 13824  epelg 13827  dffr5 13831  dftr6 13834  fundmpss 13836  setinds 13844  dfon2lem1 13849  dfon2lem3 13851  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2 13858  predreseq 13890  predso 13895  predbrg 13897  predep 13903  preddowncl 13907  tz6.26 13913  trclss 13935  xporderlem 13948  soxp 13950  frxp 13951  poseq 13954  soseq 13955  wfrlem5 13961  wfrlem10 13966  wfrlem12 13968  wfrlem13 13969  wfrlem14 13970  wfrlem16 13972  tfrALTlem 13976  elno 13987  axsltsolem1 14006  axfelem15 14045  axfelem16 14046  txpss3v 14065  brtxp 14067  brsset 14069  idsset 14070  dfon3 14072  brbigcup 14074  fnbigcup 14075  elfix 14077  elfix2 14078  limitssson 14080  dfom5 14081  altopelaltxp 14099  altxpsspw 14100  fatesg 14293  twsvbdop 14332  uninqs 14340  elo 14342  infi1 14343  stcat 14347  ficli 14353  domfldrefc 14361  ranfldrefc 14362  domrngref 14364  domintrefb 14367  ref4w 14370  cpref 14379  restidsing 14391  prj1 14395  eloi 14400  elintabg 14414  omslim 14420  omslim2 14421  surjsec2 14467  inpreima2 14468  inpreima5 14469  mapmapmap 14486  injsurinj 14487  elixp2a 14493  elixp2b 14494  hbcp 14500  npincppr 14501  repcpwti 14503  cbcpcp 14504  prjmapcp 14507  cbicplem 14508  prjmapcp2 14515  dstr 14516  iscst2 14520  iscst4 14522  nZdef 14527  islatalg 14531  domrancur1b 14548  domrancur1c 14550  mnlmxl2 14611  defse3 14614  inpc 14619  inposet 14620  tolat 14631  pospos 14635  tostos 14637  toplat 14638  dfdir2 14639  dffprod 14670  fprod1fi 14675  fprod1slem 14676  fprodp1fi 14680  fprod1ib 14686  clfsebs 14707  fincmpzer 14711  isppm 14715  fprodneg 14741  fprodsub 14742  svs2 14829  inttop2 14863  mapdiscn 14871  mapudiscn 14872  sallnei 14873  nsn 14874  hmphsyma 14882  hmpher 14890  hmeogrp 14892  homcard 14893  eqindhome 14895  sbtpsines 14905  subtopsin2 14907  qusp 14908  ttcn 14913  fgsb 14921  fgsb2 14925  cnfilca 14927  rcfpfillem4 14931  rcfpfillem6 14933  rcfpfil 14934  dtt2 14951  bwt2 14960  altretop 14997  domleqt 15020  lteqtpos 15024  dmrngcmp 15098  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualded 15132  dualcat2 15133  ishomd 15139  issubcat 15193  taralt 15211  tarvalg 15213  tarval1g 15215  tclinf 15241  cptarc 15242  settrcon 15247  tarval2 15249  tarval2g 15250  bpmp 15251  btmp 15252  intartar 15255  intrtael 15256  tmpts 15257  vtarsuelt 15272  cartarlim 15282  fnctartar 15284  fnctartar2 15285  subtr 15352  subtr2 15353  cbvcsb 15354  cbvsbcOLD 15355  dfiin2gOLD 15356  cnvresima 15359  trer 15361  finminlem 15367  elfiun 15369  fictblem 15370  fictb 15371  inficlALT 15372  finsschain 15373  ordtypelem1OLD 15375  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  onsdomOLD 15385  omsubsuc2OLD 15387  omsubsdomlem2OLD 15389  elomsubsdOLD 15394  omsublimOLD 15396  infenomsubOLD 15398  fibasOLD 15400  opncldf1 15402  opnnei 15417  subsubtop 15423  cnsubsp2 15427  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem1 15437  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  connsub 15443  cnconn 15444  conntoppr 15445  is1stc3 15469  2ndcsb 15476  2ndc1stc 15477  2ndcctbss 15478  isfne2 15481  isfne3 15482  fneer 15496  fneerdm 15498  topfneec 15501  fnessref 15503  refssfne 15504  lfinpfin 15513  locfincomp 15514  locfindsc 15515  locfincf 15516  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topmtcl 15525  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  ist1-2 15542  ist1-3 15543  neifg 15559  supfil 15560  filfinnfr 15561  isufil2 15565  filssufillem 15570  filssufil 15571  ufileulem 15572  ufileu 15573  filufint 15574  uffixfr 15575  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  ufcondr 15581  limfilcf 15587  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  sfcls 15604  filclus 15605  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  fclusff 15623  tailf 15633  istail 15634  tailmap 15636  tailuni 15638  tailfb 15639  filnetlem1 15640  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  ralabOLD 15669  cover2g 15674  prfunOLD 15677  prfOLD 15680  xpeng 15691  opabex3 15701  fvopabf4g 15703  oprabvalg 15706  fnopabco 15711  f1opr 15714  inixp 15722  hbixp1 15725  ecelqsg 15731  eropreu 15733  eroprf 15735  findcard2 15745  fimax 15746  ac6gf 15749  acdcg 15750  acdc3g 15751  acdc5g 15752  indexdom 15754  indexfiOLD 15755  inficl 15757  frinfm 15758  zornn0 15764  infmrlb 15765  infmrgelb 15766  wofi 15770  frfi 15771  pofun 15772  seq11g 15804  seq1p1g 15805  seqz1g 15806  seqzp1g 15807  seq1seqzg 15808  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  incld 15836  subspabs 15840  mettrifi2 15848  oprpiece1res1 15880  oprpiece1res2 15881  cnimass 15888  cnresima 15891  cnss 15892  cncfres 15895  tlmval 15903  haustlmu 15906  txsubsp 15912  cnresoprab 15915  cnoprab1 15921  cnoprab2 15922  txmet 15925  sstotbnd 15936  totbndbnd 15944  heiborlem1 15955  heiborlem10 15964  heiborlem23 15977  heiborlem28 15982  heiborlem38 15992  heiborlem41 15995  bfplem8 16005  bfp 16009  rrntotbnd 16022  ismrer1 16024  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpcdm 16061  phtpcer 16062  pcorevlem 16086  pi1bvalqs 16091  pi1f 16093  pi1val 16094  pi1gp 16095  riscer 16142  divrngidl 16176  intidl 16177  inidl 16178  isfldidl 16216  ispridlc 16218  erreft 16259  erdmrn2 16260  prtlem10 16265  erdisj3 16266  0nelqs2 16269  prtlem16 16272  prtlem19 16280  prter2 16285  prter3 16286  blkssatm 16289  iotain 16381  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  compel 16415  ipo0 16426  ifr0 16427  smoge 16454  trsspwALT 16640  trsspwALT2 16641  trsspwALT3 16642  pwtrVD 16646  pwtr 16647  unipwrVD 16656  unipwr 16657  strcval 16732  stb2xpl 16742  stb3xpl 16743  stb2str 16744  stb2v1 16745  stb2v2 16746  stb3str 16750  stb3v1 16751  stb3v2 16752  stb3v3 16753  glbvalle 16811  glbprople 16812  clatlat 16893  glbconx 17029  grpstr 17097  cnaddablNEW 17139  csubspset 17208  pmapglbx 17251  pmapglb 17252  polval2 17319  osumcllem10 17373  pexmidlem7 17384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain