MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vex Unicode version

Theorem vex 2919
Description: All set variables are sets (see isset 2920). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
vex  |-  x  e. 
_V

Proof of Theorem vex
StepHypRef Expression
1 equid 1684 . 2  |-  x  =  x
2 df-v 2918 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2511 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 201 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916
This theorem is referenced by:  isset  2920  ralv  2929  rexv  2930  reuv  2931  rmov  2932  rabab  2933  sbhypf  2961  ceqex  3026  ralab  3055  rexab  3057  moeq3  3071  mo2icl  3073  reu8  3090  sbc2or  3129  csbvarg  3238  csbiebg  3250  sbcnestgf  3258  sbnfc2  3269  ddif  3439  csbing  3508  dfun2  3536  dfin2  3537  vn0  3595  eqv  3603  abvor0  3605  sbss  3697  csbifg  3727  ifexg  3758  elpwg  3766  exsnrex  3808  dftp2  3814  prnzg  3884  snssg  3892  difprsnss  3894  sneqrg  3928  preq12bg  3937  pwpr  3971  pwtp  3972  pwv  3974  unipr  3989  uniprg  3990  unisng  3992  elintg  4018  elintrabg  4023  intss1  4025  ssint  4026  intmin  4030  intss  4031  intssuni  4032  intmin4  4039  intab  4040  intun  4042  intpr  4043  intprg  4044  uniintsn  4047  iinconst  4062  iuniin  4063  iinss1  4065  dfiin2g  4084  dfiunv2  4087  ssiinf  4100  iinss  4102  iinss2  4103  0iin  4109  iinab  4112  iinun2  4117  iundif2  4118  iindif2  4120  iinin2  4121  iinuni  4134  sspwuni  4136  iinpw  4139  iunpwss  4140  brab1  4217  csbopabg  4243  mptv  4261  trint  4277  trintss  4278  vprc  4301  inex1g  4306  ssexg  4309  intex  4316  inuni  4322  axpweq  4336  pwexg  4343  pwuni  4355  axpr  4362  zfpair2  4364  elALT  4367  rext  4372  sspwb  4373  unipw  4374  ssextss  4377  nnullss  4385  exss  4386  opth  4395  opthg  4396  copsexg  4402  copsex4g  4405  moop2  4411  euotd  4417  opelopabsbOLD  4423  opelopabsb  4425  pwin  4447  pwunss  4448  pwssun  4449  epelg  4455  epel  4457  dfid3  4459  pofun  4479  epse  4525  wefrc  4536  tron  4564  onfr  4580  sucel  4614  suctr  4624  uniexg  4665  unexb  4668  snnex  4672  uniuni  4675  eusvnf  4677  eusvnfb  4678  reusv6OLD  4693  iunpw  4718  onint  4734  ordpwsuc  4754  unon  4770  ordunisuc  4771  onuninsuci  4779  orduninsuc  4782  limsssuc  4789  limuni3  4791  tfinds  4798  tfindsg  4799  tfindsg2  4800  tfinds2  4802  dfom2  4806  peano5  4827  finds  4830  findsg  4831  finds2  4832  0nelxp  4865  opelxp  4867  opeliunxp  4888  elvv  4895  elvvv  4896  elvvuni  4897  xpsspw  4945  xpsspwOLD  4946  relopabi  4959  opabid2  4963  difopab  4965  xpiindi  4969  ralxpf  4978  relop  4982  cnvco  5015  dfrn2  5018  dfdm4  5022  dmss  5028  dmin  5036  dmiun  5037  dmuni  5038  dm0  5042  dmi  5043  reldm0  5046  elreldm  5053  elrnmpt1  5078  dmrnssfld  5088  dmcoss  5094  dmcosseq  5096  opelresg  5112  resieq  5115  dmres  5126  elres  5140  relssres  5142  resopab  5146  resiexg  5147  iss  5148  dfres2  5152  dfima2  5164  csbima12g  5172  imadmrn  5174  imai  5177  elimasng  5189  args  5191  epini  5193  iniseg  5194  dffr3  5195  dfse2  5196  exse2  5197  cotr  5205  issref  5206  cnvsym  5207  intasym  5208  asymref  5209  asymref2  5210  intirr  5211  brcodir  5212  codir  5213  qfto  5214  poirr2  5217  cnvopab  5233  cnv0  5234  cnvi  5235  cnvdif  5237  rniun  5241  dminss  5245  imainss  5246  inimasn  5248  ssrnres  5268  rninxp  5269  dminxp  5270  cnvcnv3  5279  dfrel2  5280  dmsnn0  5294  dmsnopg  5300  cnvcnvsn  5306  dmsnsnsn  5307  cnvsng  5314  elxp4  5316  elxp5  5317  cnvresima  5318  dfco2  5328  dfco2a  5329  cores  5332  resco  5333  imaco  5334  rnco  5335  coiun  5338  co02  5342  coi1  5344  coass  5347  relssdmrn  5349  unielrel  5353  unixp0  5362  ressn  5367  cnviin  5368  cnvpo  5369  cnvso  5370  uniabio  5387  iotaval  5388  sniota  5404  csbiotag  5406  dffun2  5423  dffun7  5438  dffun8  5439  dffun9  5440  funopg  5444  funssres  5452  funun  5454  funcnvsn  5455  funcnv2  5469  funcnv  5470  funcnv3  5471  fun2cnv  5472  funcnvuni  5477  imadif  5487  isarep1  5491  2elresin  5515  fnres  5520  fcnvres  5579  fabexg  5583  fconstg  5589  fun11iun  5654  f1osng  5675  dffv3  5683  fv3  5703  fvres  5704  nfunsn  5720  funimass4  5736  ssimaexg  5748  dffv2  5755  dmfco  5756  fvopab6  5785  fndmdif  5793  iinpreima  5819  fvelrn  5825  dff3  5841  dffo4  5844  exfo  5846  f1ompt  5850  fmptco  5860  fsng  5866  dfmpt  5870  fnressn  5877  fressnfv  5879  fvsng  5886  fnpr  5909  fnprOLD  5910  zfrep6  5927  funfvima3  5934  idref  5938  fvclss  5939  fvresex  5941  abrexco  5945  opabex3d  5948  opabex3  5949  imaiun  5951  dff13  5963  foeqcnvco  5986  f1eqcocnv  5987  fliftcnv  5992  isocnv2  6010  isomin  6016  isoini  6017  isofr  6021  isose  6022  f1oweALT  6033  wemoiso  6037  wemoiso2  6038  knatar  6039  oprabid  6064  csbovg  6071  0neqopab  6078  eloprabga  6119  mpt2v  6122  caovmo  6243  f1opw  6258  ofmres  6302  op1stg  6318  op2ndg  6319  1stval2  6323  2ndval2  6324  fo1st  6325  fo2nd  6326  f1stres  6327  f2ndres  6328  fo1stres  6329  fo2ndres  6330  1st2val  6331  2nd2val  6332  xp1st  6335  xp2nd  6336  sbcopeq1a  6358  csbopeq1a  6359  eloprabi  6372  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fmpt2co  6389  df1st2  6392  df2nd2  6393  1stconst  6394  2ndconst  6395  curry1  6397  curry2  6400  fparlem1  6405  fparlem2  6406  fpar  6409  fsplit  6410  fo2ndf  6412  f1o2ndf1  6413  frxp  6415  xporderlem  6416  soxp  6418  fnwelem  6420  fnse  6422  reldmtpos  6446  dmtpos  6450  rntpos  6451  ovtpos  6453  dftpos3  6456  dftpos4  6457  tpostpos  6458  porpss  6485  sorpss  6486  sorpsscmpl  6492  opiota  6494  opabiotafun  6495  opabiota  6497  riotav  6513  csbriotag  6521  onovuni  6563  smogt  6588  tfrlem3  6597  tfrlem8  6604  tfrlem9a  6606  tfrlem16  6613  tz7.44lem1  6622  rdg0g  6644  rdglim2  6649  tz7.48-1  6659  seqomlem1  6666  seqomlem2  6667  abianfplem  6674  oacl  6738  omcl  6739  oecl  6740  oa0r  6741  om0r  6742  om1r  6745  oe1m  6747  oaordi  6748  oawordri  6752  oawordeulem  6756  oalimcl  6762  oaass  6763  oarec  6764  omordi  6768  omwordri  6774  omlimcl  6780  odi  6781  omass  6782  omeulem1  6784  oen0  6788  oeordi  6789  oewordri  6794  oeworde  6795  oeoalem  6798  oeoelem  6800  nnawordex  6839  omabs  6849  omsmolem  6855  ercnv  6885  iserd  6890  eqerlem  6896  eqer  6897  ecdmn0  6906  erth  6908  erdisj  6911  qsss  6924  ecid  6928  qsid  6929  iiner  6935  qsel  6942  erovlem  6959  ecopovsym  6965  ecopovtrn  6966  ecopover  6967  mapprc  6981  fnmap  6984  fnpm  6985  mapval2  7002  pmsspw  7007  mapsn  7014  mapsncnv  7019  ixpconstg  7030  ixpprc  7042  uniixp  7044  ixpin  7046  ixpiin  7047  resixpfo  7059  elixpsn  7060  ixpsnf1o  7061  boxriin  7063  boxcutc  7064  bren  7076  brdomg  7077  domen  7080  domeng  7081  idssen  7111  ener  7113  domtr  7119  ensn1g  7131  en1  7133  en1b  7134  fundmen  7139  fundmeng  7140  mapsnen  7143  unen  7148  domdifsn  7150  xpsnen  7151  xpsneng  7152  xpcomeng  7159  xpassen  7161  xpdom2  7162  xpdom2g  7163  domunsncan  7167  omxpenlem  7168  pw2f1o  7172  sbthlem10  7185  sbth  7186  sbthcl  7188  domunsn  7216  fodomr  7217  pwdom  7218  canth2  7219  canth2g  7220  domssex  7227  xpf1o  7228  mapen  7230  mapunen  7235  map2xp  7236  mapdom2  7237  mapdom3  7238  ssenen  7240  infensuc  7244  nneneq  7249  php  7250  php2  7251  php3  7252  sucdom2  7262  1sdom  7270  unxpdomlem2  7273  unxpdomlem3  7274  isinf  7281  fineqvlem  7282  fineqv  7283  pssnn  7286  ssfi  7288  dif1enOLD  7299  dif1en  7300  findcard  7306  findcard2  7307  findcard2s  7308  ac6sfi  7310  frfi  7311  fimax2g  7312  unbnn2  7323  isfinite2  7324  xpfi  7337  domunfican  7338  fiint  7342  fodomfi  7344  fodomfib  7345  iunfi  7353  pwfilem  7359  ixpfi2  7363  fissuni  7369  fipreima  7370  finsschain  7371  fival  7375  ssfii  7382  fi0  7383  fiin  7385  dffi2  7386  fipwuni  7389  fisn  7390  elfiun  7393  dffi3  7394  fifo  7395  marypha1lem  7396  dfsup2  7405  dfsup2OLD  7406  ordiso2  7440  oismo  7465  hartogslem1  7467  hartogs  7469  wofib  7470  wemappo  7474  wemapso2lem  7475  card2on  7478  brwdom  7491  brwdomn0  7493  brwdom2  7497  wdomtr  7499  wdompwdom  7502  canthwdom  7503  xpwdomg  7509  unxpwdom2  7512  ixpiunwdom  7515  elirrv  7521  zfregfr  7526  inf0  7532  inf3lema  7535  inf3lemd  7538  inf3lem1  7539  inf3lem2  7540  inf3lem3  7541  inf3lem5  7543  inf3lem6  7544  inf3lem7  7545  inf3  7546  infeq5  7548  omex  7554  dfom3  7558  dfom5  7561  infdifsn  7567  cantnfdm  7575  cantnfval  7579  cantnfval2  7580  cantnflt  7583  cantnff  7585  oemapso  7594  cantnflem1  7601  wemapwe  7610  cnfcom  7613  cnfcom3clem  7618  epfrs  7623  tcvalg  7633  tctr  7635  tcmin  7636  r1sdom  7656  r1val1  7668  tz9.12lem1  7669  tz9.12lem3  7671  tz9.13  7673  tz9.13g  7674  rankf  7676  unir1  7695  rankvalg  7699  rankonidlem  7710  r1val2  7719  bndrank  7723  ranklim  7726  r1pwOLD  7728  rankunb  7732  rankuni2b  7735  rankuni  7745  rankval4  7749  rankxplim  7759  rankxplim3  7761  rankxpsuc  7762  tcrank  7764  cp  7771  bnd2  7773  kardex  7774  karden  7775  cardf2  7786  tskwe  7793  cardlim  7815  harcard  7821  cardiun  7825  pm54.43  7843  r0weon  7850  infxpenlem  7851  infxpenc2lem2  7857  fseqenlem1  7861  fseqenlem2  7862  fseqen  7864  dfac8alem  7866  dfac8clem  7869  ac10ct  7871  ween  7872  acnlem  7885  finacn  7887  acndom  7888  acndom2  7891  wdomfil  7898  infpwfien  7899  alephon  7906  alephcard  7907  alephordi  7911  cardaleph  7926  alephval3  7947  iunfictbso  7951  aceq3lem  7957  dfac3  7958  dfac4  7959  dfac5lem1  7960  dfac5lem2  7961  dfac5lem3  7962  dfac5lem4  7963  dfac5lem5  7964  dfac5  7965  dfac2a  7966  dfac2  7967  dfac8  7971  dfac9  7972  dfac10b  7975  acacni  7976  dfacacn  7977  dfac13  7978  kmlem1  7986  kmlem2  7987  kmlem9  7994  kmlem10  7995  kmlem11  7996  kmlem12  7997  kmlem13  7998  cdafn  8005  pwsdompw  8040  infmap2  8054  ackbij1lem5  8060  ackbij1lem8  8063  ackbij2  8079  cflm  8086  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cfflb  8095  cfval2  8096  cflim2  8099  cfss  8101  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  sornom  8113  infpssr  8144  fin4en1  8145  enfin2i  8157  fin23lem26  8161  fin23lem14  8169  fin23lem16  8171  fin23lem17  8174  fin23lem21  8175  fin23lem32  8180  fin23lem34  8182  fin23lem39  8186  compsscnvlem  8206  compssiso  8210  isf34lem4  8213  enfin1ai  8220  isfin1-3  8222  fin67  8231  dffin7-2  8234  fin1a2lem7  8242  fin1a2lem10  8245  fin1a2lem12  8247  fin1a2lem13  8248  fin12  8249  itunitc1  8256  itunitc  8257  ituniiun  8258  hsmexlem2  8263  hsmexlem4  8265  hsmex  8268  axcc2lem  8272  axcc3  8274  acncc  8276  fin41  8280  dominf  8281  dcomex  8283  axdc2lem  8284  axdc3lem  8286  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ac9  8319  ac6s  8320  ac6sg  8324  ac9s  8329  numthcor  8330  zorn2lem1  8332  zorn2lem4  8335  zorn2lem7  8338  zorng  8340  zornn0g  8341  ttukeylem5  8349  ttukeylem6  8350  ttukeylem7  8351  axdclem  8355  axdclem2  8356  fodomg  8359  fodomb  8360  brdom3  8362  brdom5  8363  brdom4  8364  brdom7disj  8365  brdom6disj  8366  iunfo  8370  ondomon  8394  cardmin  8395  alephval2  8403  dominfac  8404  fpwwe2lem1  8462  fpwwe2lem8  8468  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  fpwwe  8477  canthwe  8482  canthp1lem1  8483  pwfseqlem1  8489  pwfseqlem2  8490  pwfseqlem3  8491  pwfseqlem4a  8492  pwfseqlem5  8494  pwxpndom2  8496  gchac  8504  gch2  8510  inawinalem  8520  winainflem  8524  winalim2  8527  winafp  8528  gchina  8530  wunfi  8552  intwun  8566  wunex2  8569  uniwun  8571  eltsk2g  8582  inttsk  8605  inar1  8606  rankcf  8608  tskcard  8612  tskuni  8614  gruun  8637  intgru  8645  ingru  8646  wfgru  8647  grudomon  8648  gruina  8649  grur1a  8650  grur1  8651  grutsk  8653  axgroth5  8655  axgroth2  8656  grothpw  8657  grothpwex  8658  axgroth6  8659  grothomex  8660  grothac  8661  axgroth3  8662  grothprim  8665  grothtsk  8666  inaprc  8667  nqereu  8762  nqerf  8763  dmrecnq  8801  ltaddnq  8807  genpnnp  8838  genpnmax  8840  genpcl  8841  nqpr  8847  addclprlem1  8849  mulclprlem  8852  distrlem4pr  8859  1idpr  8862  prlem934  8866  ltaddpr  8867  ltexprlem3  8871  ltexprlem4  8872  ltexprlem6  8874  ltexprlem7  8875  prlem936  8880  reclem2pr  8881  reclem3pr  8882  mulasssr  8921  ltsosr  8925  0idsr  8928  1idsr  8929  ltasr  8931  recexsrlem  8934  mulgt0sr  8936  supsrlem  8942  ltresr  8971  axmulass  8988  axrrecex  8994  axpre-lttri  8996  wuncn  9001  renfdisj  9094  wloglei  9515  lbinfm  9917  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  dfinfmr  9941  infmsup  9942  infmrgelb  9944  infmrlb  9945  dfnn2  9969  dflt2  10697  xrinfmss2  10845  infmxrgelb  10869  xrinfm0  10871  fzpr  11057  uzrdgfni  11253  axdc4uzlem  11276  axdc4uz  11277  seqval  11289  seqfeq4  11327  serle  11333  seqof  11335  hash1snb  11636  hash2prde  11643  hash2prb  11644  hashxplem  11651  hashmap  11653  hashpw  11654  hashfun  11655  hashbclem  11656  hashfacen  11658  hashf1lem1  11659  hashf1lem2  11660  hashf1  11661  fz1isolem  11665  brfi1uzind  11670  ccatfn  11696  wrdexb  11718  wrdind  11746  shftfval  11840  shftfib  11842  shftfn  11843  2shfti  11850  sqrlem6  12008  rexfiuz  12106  rlimdm  12300  fclim  12302  climshft  12325  fsum2dlem  12509  fsumcom2  12513  fsum0diag2  12521  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  incexclem  12571  isumltss  12583  supcvg  12590  xpnnenOLD  12764  rpnnen2lem11  12779  algrf  13019  isprm2lem  13041  isprm2  13042  prmind2  13045  iserodd  13164  4sqlem12  13279  vdwmc  13301  vdwlem10  13313  vdwlem13  13316  ramtlecl  13323  hashbc0  13328  ramval  13331  ramcl2lem  13332  ramub2  13337  0ram  13343  ram0  13345  ramub1lem1  13349  ramub1lem2  13350  ramub1  13351  restfn  13607  elrest  13610  restsspw  13614  prdsval  13633  prdsle  13639  prdsless  13640  prdsleval  13654  pwsle  13669  imasaddfnlem  13708  imasvscafn  13717  imasleval  13721  xpsc0  13740  xpsc1  13741  xpsfrnel2  13745  ismre  13770  fnmre  13771  ismred  13782  mremre  13784  fnmrc  13787  mrcfval  13788  mrisval  13810  mreexexlem4d  13827  isacs2  13833  mreacs  13838  acsfn  13839  acsfn1  13841  acsfn2  13843  cidffn  13858  comfeq  13887  invsym2  13943  oppcsect2  13955  brssc  13969  sscpwex  13970  isssc  13975  issubc  13990  isfuncd  14017  cofucl  14040  funcres2b  14049  funcpropd  14052  setcmon  14197  catcval  14206  fnxpc  14228  xpcval  14229  xpccatid  14240  curf2ndf  14299  drsdirfi  14350  isdrs2  14351  clatl  14498  odupos  14517  oduposb  14518  oduglb  14521  odulub  14523  posglbd  14531  ipoval  14535  ipolerval  14537  fpwipodrs  14545  ipodrsima  14546  isacs5lem  14550  psdmrn  14594  psssdm2  14602  submacs  14720  pwsdiagmhm  14723  gsumwspan  14746  mulgpropd  14878  subgacs  14930  nsgacs  14931  eqgfval  14943  eqgval  14944  gicsubgen  15020  gaid  15031  gaorb  15039  orbsta  15045  symgval  15049  symgbas  15050  symgplusg  15054  sylow1lem2  15188  sylow2alem1  15206  sylow2alem2  15207  sylow2a  15208  sylow2blem1  15209  sylow2blem2  15210  sylow2blem3  15211  sylow3lem1  15216  sylow3lem3  15218  sylow3lem6  15221  efgval  15304  efgval2  15311  efgrelexlemb  15337  efgcpbllema  15341  efgcpbllemb  15342  vrgpfval  15353  frgpuplem  15359  divsabl  15435  frgpnabllem1  15439  gsumval3  15469  gsumzaddlem  15481  gsumzadd  15482  gsum2d  15501  gsum2d2  15503  gsumcom2  15504  gsumxp  15505  dprdfadd  15533  dprdres  15541  subgdmdprd  15547  dprd2dlem1  15554  dprd2d2  15557  ablfac1eulem  15585  pgpfac1lem5  15592  opprsubg  15696  subrgmre  15847  subsubrg2  15850  subrgpropd  15857  lss1d  15994  lssintcl  15995  lssmre  15997  lssacs  15998  pwsdiaglmhm  16088  lbsextlem4  16188  drngnidl  16255  lidldvgen  16281  psrbaglefi  16392  mplcoe1  16483  mplcoe2  16485  ltbval  16487  ltbwe  16488  opsrle  16491  opsrtoslem1  16499  opsrtoslem2  16500  evlslem4  16519  coe1mul2  16617  coe1tm  16620  znleval  16790  cssmre  16875  thlle  16879  pjfval2  16891  istopon  16945  tgval2  16976  bastg  16986  tgdom  16998  distop  17015  indistopon  17020  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  fncld  17041  cldss2  17049  ntreq0  17096  discld  17108  mretopd  17111  toponmre  17112  neisspw  17126  opnnei  17139  tgrest  17177  resttopon  17179  restco  17182  restdis  17196  neitr  17198  ordtbas2  17209  ordtcnv  17219  ordtrest2  17222  pnfnei  17238  mnfnei  17239  iscnp2  17257  subbascn  17272  cnntr  17293  cnrest2  17304  cnpresti  17306  cnprest  17307  cnprest2  17308  ist1-3  17367  hausnei2  17371  isnrm2  17376  dishaus  17400  cmpcovf  17408  fincmp  17410  cmpsublem  17416  cmpsub  17417  cmpcld  17419  uncmp  17420  fiuncmp  17421  hauscmplem  17423  cmpfi  17425  dfcon2  17435  consuba  17436  cnconn  17438  uncon  17445  t1conperf  17452  is1stc2  17458  1stcfb  17461  2ndcsb  17465  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  2ndcdisj  17472  2ndcomap  17474  2ndcsep  17475  dis2ndc  17476  llyi  17490  nllyi  17491  nlly2i  17492  llynlly  17493  subislly  17497  restnlly  17498  restlly  17499  islly2  17500  llyrest  17501  llyidm  17504  nllyidm  17505  hausllycmp  17510  cldllycmp  17511  lly1stc  17512  dislly  17513  hausmapdom  17516  kgenf  17526  iskgen3  17534  llycmpkgen2  17535  1stckgenlem  17538  1stckgen  17539  kgencn2  17542  txuni2  17550  txbas  17552  eltx  17553  ptpjpre1  17556  ptuni2  17561  ptpjcn  17596  ptpjopn  17597  ptclsg  17600  dfac14  17603  xkoccn  17604  txcnp  17605  txcnmpt  17609  prdstopn  17613  txrest  17616  txdis  17617  txindis  17619  txdis1cn  17620  txlly  17621  txnlly  17622  pthaus  17623  txcmplem1  17626  txcmplem2  17627  hausdiag  17630  txlm  17633  tx1stc  17635  tx2ndc  17636  txkgen  17637  xkopt  17640  xkococnlem  17644  xkococn  17645  cnmpt1st  17653  cnmpt2nd  17654  xkofvcn  17669  xkoinjcn  17672  txcon  17674  imasnopn  17675  imasncld  17676  imasncls  17677  qtoptop2  17684  qtopuni  17687  basqtop  17696  tgqtop  17697  hmphdis  17781  indishmph  17783  txhmeo  17788  pt1hmeo  17791  ptuncnv  17792  ptunhmeo  17793  xpstopnlem1  17794  ptcmpfi  17798  xkohmeo  17800  isfbas  17814  isfbas2  17820  fbssfi  17822  trfbas2  17828  isfild  17843  snfil  17849  elfg  17856  fgcl  17863  filcon  17868  fbasrn  17869  filuni  17870  trfil2  17872  cfinfil  17878  csdfil  17879  supfil  17880  zfbas  17881  isufil2  17893  filssufilg  17896  acufl  17902  filufint  17905  uffix  17906  ufildr  17916  fin1aufil  17917  rnelfmlem  17937  rnelfm  17938  fmfnfmlem3  17941  fmfnfmlem4  17942  fmfnfm  17943  ufldom  17947  flimrest  17968  hauspwpwf1  17972  txflf  17991  fclsrest  18009  fclscmp  18015  alexsubb  18030  alexsubALTlem1  18031  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  ptcmplem4  18039  ptcmplem5  18040  cnextf  18050  cnextcn  18051  tmdgsum  18078  symgtgp  18084  cldsubg  18093  tgpconcomp  18095  divstgplem  18103  divstgphaus  18105  prdstmdd  18106  tsmsval2  18112  tsmssubm  18125  ustfn  18184  ustfilxp  18195  ustn0  18203  restutopopn  18221  ustuqtop0  18223  ustuqtop1  18224  ustuqtop2  18225  ustuqtop3  18226  ustuqtop4  18227  utopsnneiplem  18230  utopreg  18235  ucnimalem  18263  ucnima  18264  fmucndlem  18274  neipcfilu  18279  imasdsf1olem  18356  xpsdsval  18364  xmetec  18417  prdsbl  18474  stdbdxmet  18498  met1stc  18504  prdsxmslem2  18512  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  blval2  18558  metuel2  18562  metustblOLD  18563  metustbl  18564  restmetu  18570  dscopn  18574  xrtgioo  18790  xrsblre  18795  icccmplem1  18806  icccmplem2  18807  fsumcn  18853  fsum2cn  18854  cnllycmp  18934  isphtpc  18972  pi1blem  19017  iscmet3  19199  metcld2  19212  bcthlem4  19233  minveclem3b  19282  ovolfiniun  19350  ovoliunlem1  19351  ovoliunlem2  19352  finiunmbl  19391  volfiniun  19394  iundisj2  19396  uniioombllem3  19430  vitalilem2  19454  vitalilem3  19455  vitali  19458  mbfimaopnlem  19500  itg1addlem4  19544  mbfi1fseqlem4  19563  mbfi1fseqlem6  19565  itgfsum  19671  ellimc2  19717  limcflf  19721  perfdvf  19743  dvres  19751  dvres2  19752  dvnff  19762  dvcj  19789  dvrec  19794  dvmptfsum  19812  dvef  19817  rolle  19827  dvivthlem1  19845  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem3  19865  ftc1cn  19880  mpfind  19918  pf1ind  19928  vieta1lem2  20181  elqaalem2  20190  ulmdv  20272  logfac  20448  xrlimcnp  20760  jensenlem1  20778  jensenlem2  20779  jensen  20780  wilthlem2  20805  prmorcht  20914  lgsquadlem1  21091  lgsquadlem2  21092  dchrisumlema  21135  dchrisumlem3  21138  umgraex  21311  isusgra0  21329  usgra2edg  21355  usgrarnedg  21357  usgraedg4  21359  usgraedgreu  21360  usgraexmpl  21373  usgrafis  21382  nbgraf1olem5  21408  nb3graprlem1  21413  cusgrarn  21421  cusgrares  21434  cusgrasize  21440  cusgrafilem1  21441  cusgrafilem2  21442  isuvtx  21450  uvtx01vtx  21454  trls  21489  wlkntrllem2  21513  wlkntrl  21515  constr1trl  21541  2pthon  21555  dfconngra1  21611  eupath  21656  ex-natded9.26  21680  nvss  22025  vsfval  22067  h2hlm  22436  axhcompl-zf  22454  hlim2  22647  hhcmpl  22655  hhcms  22658  shex  22667  isch2  22679  helch  22699  hhsscms  22732  occl  22759  chintcli  22786  dfch2  22862  spanuni  22999  spansni  23012  elnlfn  23384  nmopun  23470  nlelchi  23517  cnlnssadj  23536  adjbd1o  23541  branmfn  23561  pjnmopi  23604  hmopidmchi  23607  abrexss  23946  iuninc  23964  disjabrex  23977  disjabrexf  23978  disjpreima  23979  disjxpin  23981  iundisj2f  23983  suppss2f  24002  fmptdF  24022  fmptcof2  24029  ofpreima  24034  funcnvmptOLD  24035  funcnvmpt  24036  disjdsct  24043  1stpreima  24048  2ndpreima  24049  ctex  24053  iundisj2fi  24106  ishashinf  24112  tosglb  24145  pstmxmet  24245  tpr2rico  24263  esum0  24397  esumc  24399  gsumesum  24404  esumcst  24408  esumfsup  24413  esumpfinvalf  24419  hasheuni  24428  sigaex  24445  sigaval  24446  isrnsigaOLD  24448  pwsiga  24466  sigainb  24472  insiga  24473  dmsigagen  24480  measbase  24504  ismeas  24506  isrnmeas  24507  measiuns  24524  measdivcstOLD  24531  measdivcst  24532  cntmeas  24533  mbfmco2  24568  mbfmcnt  24571  br2base  24572  dya2iocrfn  24582  dya2iocct  24583  dya2iocnrect  24584  dya2iocucvr  24587  sxbrsigalem2  24589  ballotlem2  24699  ballotlemsf1o  24724  ballotlemirc  24742  derangenlem  24810  subfacp1lem1  24818  subfacp1lem3  24821  subfacp1lem4  24822  subfacp1lem5  24823  erdszelem7  24836  erdszelem8  24837  erdsze2lem2  24843  kur14lem9  24853  ptpcon  24873  indispcon  24874  conpcon  24875  cnllyscon  24885  rellyscon  24891  cvmsss2  24914  cvmcov2  24915  cvmliftlem15  24938  cvmlift2lem1  24942  cvmlift2lem12  24954  ghomgrplem  25053  relexpindlem  25092  rtrclreclem.trans  25099  dfrtrcl2  25101  untsucf  25112  dfid4  25136  shftvalg  25161  ntrivcvg  25178  fprodfac  25249  fprod2dlem  25257  fprodcom2  25261  dftr6  25321  coepr  25323  dffr5  25324  dfso2  25325  dfpo2  25326  br8  25327  br6  25328  br4  25329  dfres3  25330  cnvco1  25331  cnvco2  25332  eldm3  25333  fundmpss  25336  fprb  25343  dfdm5  25346  dfrn5  25347  setinds  25348  dfon2lem1  25353  dfon2lem3  25355  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  dfon2  25362  rdgprc  25365  dfrdg2  25366  predreseq  25393  predpo  25398  predbrg  25400  setlikespec  25401  predep  25406  preddowncl  25410  preduz  25414  predfz  25417  tz6.26  25419  trpredrec  25455  poseq  25467  soseq  25468  wfrlem5  25474  wfrlem10  25479  wfrlem12  25481  wfrlem13  25482  wfrlem14  25483  wfrlem16  25485  tfrALTlem  25490  frrlem5  25499  frrlem11  25507  sltsolem1  25536  nofulllem5  25574  txpss3v  25632  brtxp  25634  brtxp2  25635  pprodss4v  25638  brpprod  25639  brpprod3a  25640  brpprod3b  25641  brsset  25643  idsset  25644  dfon3  25646  brtxpsd  25648  brbigcup  25652  dfbigcup2  25653  fobigcup  25654  elfix  25657  elfix2  25658  dffix2  25659  fixcnv  25662  limitssson  25665  dfom5b  25666  dffun10  25667  elfuns  25668  elfunsg  25669  elsingles  25671  fnsingle  25672  fvsingle  25673  dfiota3  25676  brimage  25679  brimageg  25680  funimage  25681  fnimage  25682  imageval  25683  brcart  25685  brdomaing  25688  brrangeg  25689  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  funpartlem  25695  funpartfun  25696  funpartfv  25698  fullfunfv  25700  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  altopelaltxp  25725  altxpsspw  25726  brsegle  25946  fvline  25982  liness  25983  ellines  25990  bpoly2  26007  bpoly3  26008  rankung  26011  ranksng  26012  rankelg  26013  rankpwg  26014  rankeq1o  26016  elhf2g  26021  hfext  26028  onsucconi  26091  supaddc  26137  supadd  26138  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  ftc1cnnc  26178  areacirclem6  26186  trer  26209  finminlem  26211  gtinf  26212  fneer  26258  fnessref  26263  refssfne  26264  islocfin  26266  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  topmeet  26283  topjoin  26284  neifg  26290  tailfb  26296  filnetlem2  26298  filnetlem3  26299  filnetlem4  26300  cover2g  26306  f1opr  26316  inixp  26320  indexdom  26326  frinfm  26327  sdclem2  26336  sdclem1  26337  fdc  26339  isbndx  26381  prdstotbnd  26393  heibor1lem  26408  heiborlem1  26410  heiborlem3  26412  heiborlem4  26413  heiborlem5  26414  heiborlem6  26415  heiborlem8  26417  heiborlem10  26419  ismrer1  26437  riscer  26494  divrngidl  26528  intidl  26529  isfldidl  26568  ispridlc  26570  prtlem10  26604  prtlem13  26607  prtlem16  26608  prtlem19  26617  prter2  26620  prter3  26621  ralxpmap  26632  elrfi  26638  ismrcd1  26642  ismrcd2  26643  istopclsd  26644  ismrc  26645  mrefg2  26651  isnacs3  26654  mzpclall  26674  mzpincl  26681  mzpsubst  26695  mzpcompact2lem  26698  mzpcompact2  26699  eldioph2lem1  26708  eldioph2lem2  26709  eldiophss  26723  diophrex  26724  rexrabdioph  26744  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  rabren3dioph  26766  fphpd  26767  rencldnfilem  26771  pellexlem5  26786  pellex  26788  rmxypairf1o  26864  monotuz  26894  monotoddzzfi  26895  oddcomabszz  26897  2nn0ind  26898  zindbi  26899  mzpcong  26927  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  setindtr  26985  setindtrs  26986  dford3lem2  26988  ttac  26997  pw2f1ocnv  26998  wepwsolem  27006  inisegn0  27008  dnnumch1  27009  fnwe2val  27014  fnwe2lem2  27016  aomclem1  27019  aomclem2  27020  aomclem6  27024  dfac11  27028  kelac2lem  27030  dfac21  27032  islssfg2  27037  lmhmlnmsplit  27053  pwssplit3  27058  filnm  27060  pwslnmlem1  27062  pwslnm  27064  dsmmval  27068  frlmlbs  27117  unxpwdom3  27124  enfixsn  27125  dfacbasgrp  27141  islindf4  27176  lmisfree  27180  lnr2i  27188  lnrfg  27191  hbtlem6  27201  rngunsnply  27246  pmtrfval  27261  symggen  27279  gsumcom3  27322  acsfn1p  27375  sdrgacs  27377  idomsubgmo  27382  fgraphxp  27398  expgrowth  27420  2sbc6g  27483  iotain  27485  compel  27508  ipo0  27519  ifr0  27520  fnchoice  27567  infrglb  27589  stoweidlem31  27647  stoweidlem57  27673  stirlinglem13  27702  funressnfv  27859  dfdfat2  27862  csbafv12g  27868  tz6.12-afv  27904  rlimdmafv  27908  csbaovg  27911  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  usg2wlkonot  28080  usg2wotspth  28081  2wot2wont  28083  2spontn0vne  28084  2spot2iun2spont  28088  frisusgranb  28101  frgra3vlem1  28104  frgra3vlem2  28105  3vfriswmgralem  28108  2pthfrgra  28115  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrawopreg1  28153  frgrawopreg2  28154  frg2woteq  28163  2spotiundisj  28165  usg2spot2nb  28168  onfrALTlem5  28339  onfrALTlem4  28340  onfrALTlem3  28341  opelopab4  28349  a9e2nd  28356  trsspwALT  28640  trsspwALT2  28641  trsspwALT3  28642  pwtrVD  28646  unipwrVD  28653  unipwr  28654  onfrALTlem5VD  28706  onfrALTlem4VD  28707  onfrALTlem3VD  28708  relopabVD  28722  a9e2ndVD  28729  sspwimp  28739  sspwimpVD  28740  sspwimpcf  28741  sspwimpcfVD  28742  sspwimpALT  28746  sspwimpALT2  28750  a9e2ndALT  28752  bnj23  28789  bnj62  28791  bnj156  28801  bnj219  28806  bnj610  28821  bnj918  28841  bnj927  28845  bnj976  28854  bnj1098  28860  bnj1379  28908  bnj110  28935  bnj98  28944  bnj154  28955  bnj155  28956  bnj535  28967  bnj556  28977  bnj557  28978  bnj581  28985  bnj591  28988  bnj594  28989  bnj580  28990  bnj607  28993  bnj609  28994  bnj600  28996  bnj849  29002  bnj893  29005  bnj908  29008  bnj934  29012  bnj944  29015  bnj964  29020  bnj966  29021  bnj969  29023  bnj970  29024  bnj910  29025  bnj986  29031  bnj999  29034  bnj1018  29039  bnj907  29042  bnj1039  29046  bnj1040  29047  bnj1052  29050  bnj1123  29061  bnj1030  29062  bnj1133  29064  bnj1128  29065  bnj1145  29068  bnj1204  29087  bnj1373  29105  bnj1417  29116  bnj1421  29117  bnj1498  29136  eqlkr2  29583  glbconxN  29860  pmapglbx  30251  pmapglb  30252  pclclN  30373  pclfinN  30382  polval2N  30388  pclfinclN  30432  osumcllem10N  30447  pexmidlem7N  30458  cdleme31sdnN  30869  cdlemefr44  30907  cdleme48fv  30981  cdleme46fvaw  30983  cdleme48bw  30984  cdleme46fsvlpq  30987  cdlemeg46fvcl  30988  cdlemeg49le  30993  cdlemeg46fjgN  31003  cdlemeg46fjv  31005  cdleme48d  31017  cdlemeg49lebilem  31021  cdleme50eq  31023  cdleme50f  31024  cdlemg2jlemOLDN  31075  cdlemg2klem  31077  cdlemk40  31399  cdlemk56  31453  diaglbN  31538  dvhlveclem  31591  dib1dim  31648  dibglbN  31649  diblss  31653  diblsmopel  31654  dicelvalN  31661  diclspsn  31677  cdlemn7  31686  dihordlem7  31697  dihopelvalcpre  31731  xihopellsmN  31737  dihopellsm  31738  dih1  31769  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetlem4preN  31789  dihmeetlem13N  31802  dih1dimatlem  31812  dihatlat  31817  dihjatcclem4  31904  lcdlss  32102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator