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

Theorem vex 2959
Description: All set variables are sets (see isset 2960). 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 1688 . 2  |-  x  =  x
2 df-v 2958 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2543 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 201 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2956
This theorem is referenced by:  isset  2960  ralv  2969  rexv  2970  reuv  2971  rmov  2972  rabab  2973  sbhypf  3001  ceqex  3066  ralab  3095  rexab  3097  moeq3  3111  mo2icl  3113  reu8  3130  sbc2or  3169  csbvarg  3278  csbiebg  3290  sbcnestgf  3298  sbnfc2  3309  ddif  3479  csbing  3548  dfun2  3576  dfin2  3577  vn0  3635  eqv  3643  abvor0  3645  sbss  3737  csbifg  3767  ifexg  3798  elpwg  3806  exsnrex  3848  dftp2  3854  prnzg  3924  snssg  3932  difprsnss  3934  sneqrg  3968  preq12bg  3977  pwpr  4011  pwtp  4012  pwv  4014  unipr  4029  uniprg  4030  unisng  4032  elintg  4058  elintrabg  4063  intss1  4065  ssint  4066  intmin  4070  intss  4071  intssuni  4072  intmin4  4079  intab  4080  intun  4082  intpr  4083  intprg  4084  uniintsn  4087  iinconst  4102  iuniin  4103  iinss1  4105  dfiin2g  4124  dfiunv2  4127  ssiinf  4140  iinss  4142  iinss2  4143  0iin  4149  iinab  4152  iinun2  4157  iundif2  4158  iindif2  4160  iinin2  4161  iinuni  4174  sspwuni  4176  iinpw  4179  iunpwss  4180  brab1  4257  csbopabg  4283  mptv  4301  trint  4317  trintss  4318  vprc  4341  inex1g  4346  ssexg  4349  intex  4356  inuni  4362  axpweq  4376  pwexg  4383  pwuni  4395  axpr  4402  zfpair2  4404  elALT  4407  rext  4412  sspwb  4413  unipw  4414  ssextss  4417  nnullss  4425  exss  4426  opth  4435  opthg  4436  copsexg  4442  copsex4g  4445  moop2  4451  euotd  4457  opelopabsbOLD  4463  opelopabsb  4465  pwin  4487  pwunss  4488  pwssun  4489  epelg  4495  epel  4497  dfid3  4499  pofun  4519  epse  4565  wefrc  4576  tron  4604  onfr  4620  sucel  4654  suctrALT  4664  uniexg  4706  unexb  4709  snnex  4713  uniuni  4716  eusvnf  4718  eusvnfb  4719  reusv6OLD  4734  iunpw  4759  onint  4775  ordpwsuc  4795  unon  4811  ordunisuc  4812  onuninsuci  4820  orduninsuc  4823  limsssuc  4830  limuni3  4832  tfinds  4839  tfindsg  4840  tfindsg2  4841  tfinds2  4843  dfom2  4847  peano5  4868  finds  4871  findsg  4872  finds2  4873  0nelxp  4906  opelxp  4908  opeliunxp  4929  elvv  4936  elvvv  4937  elvvuni  4938  xpsspw  4986  xpsspwOLD  4987  relopabi  5000  opabid2  5004  difopab  5006  xpiindi  5010  ralxpf  5019  relop  5023  cnvco  5056  dfrn2  5059  dfdm4  5063  dmss  5069  dmin  5077  dmiun  5078  dmuni  5079  dm0  5083  dmi  5084  reldm0  5087  elreldm  5094  elrnmpt1  5119  dmrnssfld  5129  dmcoss  5135  dmcosseq  5137  opelresg  5153  resieq  5156  dmres  5167  elres  5181  relssres  5183  resopab  5187  resiexg  5188  iss  5189  dfres2  5193  dfima2  5205  csbima12g  5213  imadmrn  5215  imai  5218  elimasng  5230  args  5232  epini  5234  iniseg  5235  dffr3  5236  dfse2  5237  exse2  5238  cotr  5246  issref  5247  cnvsym  5248  intasym  5249  asymref  5250  asymref2  5251  intirr  5252  brcodir  5253  codir  5254  qfto  5255  poirr2  5258  cnvopab  5274  cnv0  5275  cnvi  5276  cnvdif  5278  rniun  5282  dminss  5286  imainss  5287  inimasn  5289  ssrnres  5309  rninxp  5310  dminxp  5311  cnvcnv3  5320  dfrel2  5321  dmsnn0  5335  dmsnopg  5341  cnvcnvsn  5347  dmsnsnsn  5348  cnvsng  5355  elxp4  5357  elxp5  5358  cnvresima  5359  dfco2  5369  dfco2a  5370  cores  5373  resco  5374  imaco  5375  rnco  5376  coiun  5379  co02  5383  coi1  5385  coass  5388  relssdmrn  5390  unielrel  5394  unixp0  5403  ressn  5408  cnviin  5409  cnvpo  5410  cnvso  5411  uniabio  5428  iotaval  5429  sniota  5445  csbiotag  5447  dffun2  5464  dffun7  5479  dffun8  5480  dffun9  5481  funopg  5485  funssres  5493  funun  5495  funcnvsn  5496  funcnv2  5510  funcnv  5511  funcnv3  5512  fun2cnv  5513  funcnvuni  5518  imadif  5528  isarep1  5532  2elresin  5556  fnres  5561  fcnvres  5620  fabexg  5624  fconstg  5630  fun11iun  5695  f1osng  5716  dffv3  5724  fv3  5744  fvres  5745  nfunsn  5761  funimass4  5777  ssimaexg  5789  dffv2  5796  dmfco  5797  fvopab6  5826  fndmdif  5834  iinpreima  5860  fvelrn  5866  dff3  5882  dffo4  5885  exfo  5887  f1ompt  5891  fmptco  5901  fsng  5907  dfmpt  5911  fnressn  5918  fressnfv  5920  fvsng  5927  fnpr  5950  fnprOLD  5951  zfrep6  5968  funfvima3  5975  idref  5979  fvclss  5980  fvresex  5982  abrexco  5986  opabex3d  5989  opabex3  5990  imaiun  5992  dff13  6004  foeqcnvco  6027  f1eqcocnv  6028  fliftcnv  6033  isocnv2  6051  isomin  6057  isoini  6058  isofr  6062  isose  6063  f1oweALT  6074  wemoiso  6078  wemoiso2  6079  knatar  6080  oprabid  6105  csbovg  6112  0neqopab  6119  eloprabga  6160  mpt2v  6163  caovmo  6284  f1opw  6299  ofmres  6343  op1stg  6359  op2ndg  6360  1stval2  6364  2ndval2  6365  fo1st  6366  fo2nd  6367  f1stres  6368  f2ndres  6369  fo1stres  6370  fo2ndres  6371  1st2val  6372  2nd2val  6373  xp1st  6376  xp2nd  6377  sbcopeq1a  6399  csbopeq1a  6400  eloprabi  6413  mpt2mptsx  6414  dmmpt2ssx  6416  fmpt2x  6417  ovmptss  6428  fmpt2co  6430  df1st2  6433  df2nd2  6434  1stconst  6435  2ndconst  6436  curry1  6438  curry2  6441  fparlem1  6446  fparlem2  6447  fpar  6450  fsplit  6451  fo2ndf  6453  f1o2ndf1  6454  frxp  6456  xporderlem  6457  soxp  6459  fnwelem  6461  fnse  6463  reldmtpos  6487  dmtpos  6491  rntpos  6492  ovtpos  6494  dftpos3  6497  dftpos4  6498  tpostpos  6499  porpss  6526  sorpss  6527  sorpsscmpl  6533  opiota  6535  opabiotafun  6536  opabiota  6538  riotav  6554  csbriotag  6562  onovuni  6604  smogt  6629  tfrlem3  6638  tfrlem8  6645  tfrlem9a  6647  tfrlem16  6654  tz7.44lem1  6663  rdg0g  6685  rdglim2  6690  tz7.48-1  6700  seqomlem1  6707  seqomlem2  6708  abianfplem  6715  oacl  6779  omcl  6780  oecl  6781  oa0r  6782  om0r  6783  om1r  6786  oe1m  6788  oaordi  6789  oawordri  6793  oawordeulem  6797  oalimcl  6803  oaass  6804  oarec  6805  omordi  6809  omwordri  6815  omlimcl  6821  odi  6822  omass  6823  omeulem1  6825  oen0  6829  oeordi  6830  oewordri  6835  oeworde  6836  oeoalem  6839  oeoelem  6841  nnawordex  6880  omabs  6890  omsmolem  6896  ercnv  6926  iserd  6931  eqerlem  6937  eqer  6938  ecdmn0  6947  erth  6949  erdisj  6952  qsss  6965  ecid  6969  qsid  6970  iiner  6976  qsel  6983  erovlem  7000  ecopovsym  7006  ecopovtrn  7007  ecopover  7008  mapprc  7022  fnmap  7025  fnpm  7026  mapval2  7043  pmsspw  7048  mapsn  7055  mapsncnv  7060  ixpconstg  7071  ixpprc  7083  uniixp  7085  ixpin  7087  ixpiin  7088  resixpfo  7100  elixpsn  7101  ixpsnf1o  7102  boxriin  7104  boxcutc  7105  bren  7117  brdomg  7118  domen  7121  domeng  7122  idssen  7152  ener  7154  domtr  7160  ensn1g  7172  en1  7174  en1b  7175  fundmen  7180  fundmeng  7181  mapsnen  7184  unen  7189  domdifsn  7191  xpsnen  7192  xpsneng  7193  xpcomeng  7200  xpassen  7202  xpdom2  7203  xpdom2g  7204  domunsncan  7208  omxpenlem  7209  pw2f1o  7213  sbthlem10  7226  sbth  7227  sbthcl  7229  domunsn  7257  fodomr  7258  pwdom  7259  canth2  7260  canth2g  7261  domssex  7268  xpf1o  7269  mapen  7271  mapunen  7276  map2xp  7277  mapdom2  7278  mapdom3  7279  ssenen  7281  infensuc  7285  nneneq  7290  php  7291  php2  7292  php3  7293  sucdom2  7303  1sdom  7311  unxpdomlem2  7314  unxpdomlem3  7315  isinf  7322  fineqvlem  7323  fineqv  7324  pssnn  7327  ssfi  7329  dif1enOLD  7340  dif1en  7341  findcard  7347  findcard2  7348  findcard2s  7349  ac6sfi  7351  frfi  7352  fimax2g  7353  unbnn2  7364  isfinite2  7365  xpfi  7378  domunfican  7379  fiint  7383  fodomfi  7385  fodomfib  7386  iunfi  7394  pwfilem  7401  ixpfi2  7405  fissuni  7411  fipreima  7412  finsschain  7413  fival  7417  ssfii  7424  fi0  7425  fiin  7427  dffi2  7428  fipwuni  7431  fisn  7432  elfiun  7435  dffi3  7436  fifo  7437  marypha1lem  7438  dfsup2  7447  dfsup2OLD  7448  ordiso2  7484  oismo  7509  hartogslem1  7511  hartogs  7513  wofib  7514  wemappo  7518  wemapso2lem  7519  card2on  7522  brwdom  7535  brwdomn0  7537  brwdom2  7541  wdomtr  7543  wdompwdom  7546  canthwdom  7547  xpwdomg  7553  unxpwdom2  7556  ixpiunwdom  7559  elirrv  7565  zfregfr  7570  inf0  7576  inf3lema  7579  inf3lemd  7582  inf3lem1  7583  inf3lem2  7584  inf3lem3  7585  inf3lem5  7587  inf3lem6  7588  inf3lem7  7589  inf3  7590  infeq5  7592  omex  7598  dfom3  7602  dfom5  7605  infdifsn  7611  cantnfdm  7619  cantnfval  7623  cantnfval2  7624  cantnflt  7627  cantnff  7629  oemapso  7638  cantnflem1  7645  wemapwe  7654  cnfcom  7657  cnfcom3clem  7662  epfrs  7667  tcvalg  7677  tctr  7679  tcmin  7680  r1sdom  7700  r1val1  7712  tz9.12lem1  7713  tz9.12lem3  7715  tz9.13  7717  tz9.13g  7718  rankf  7720  unir1  7739  rankvalg  7743  rankonidlem  7754  r1val2  7763  bndrank  7767  ranklim  7770  r1pwOLD  7772  rankunb  7776  rankuni2b  7779  rankuni  7789  rankval4  7793  rankxplim  7803  rankxplim3  7805  rankxpsuc  7806  tcrank  7808  cp  7815  bnd2  7817  kardex  7818  karden  7819  cardf2  7830  tskwe  7837  cardlim  7859  harcard  7865  cardiun  7869  pm54.43  7887  r0weon  7894  infxpenlem  7895  infxpenc2lem2  7901  fseqenlem1  7905  fseqenlem2  7906  fseqen  7908  dfac8alem  7910  dfac8clem  7913  ac10ct  7915  ween  7916  acnlem  7929  finacn  7931  acndom  7932  acndom2  7935  wdomfil  7942  infpwfien  7943  alephon  7950  alephcard  7951  alephordi  7955  cardaleph  7970  alephval3  7991  iunfictbso  7995  aceq3lem  8001  dfac3  8002  dfac4  8003  dfac5lem1  8004  dfac5lem2  8005  dfac5lem3  8006  dfac5lem4  8007  dfac5lem5  8008  dfac5  8009  dfac2a  8010  dfac2  8011  dfac8  8015  dfac9  8016  dfac10b  8019  acacni  8020  dfacacn  8021  dfac13  8022  kmlem1  8030  kmlem2  8031  kmlem9  8038  kmlem10  8039  kmlem11  8040  kmlem12  8041  kmlem13  8042  cdafn  8049  pwsdompw  8084  infmap2  8098  ackbij1lem5  8104  ackbij1lem8  8107  ackbij2  8123  cflm  8130  cardcf  8132  cfeq0  8136  cfsuc  8137  cff1  8138  cfflb  8139  cfval2  8140  cflim2  8143  cfss  8145  cfslb2n  8148  cofsmo  8149  cfsmolem  8150  cfcoflem  8152  coftr  8153  sornom  8157  infpssr  8188  fin4en1  8189  enfin2i  8201  fin23lem26  8205  fin23lem14  8213  fin23lem16  8215  fin23lem17  8218  fin23lem21  8219  fin23lem32  8224  fin23lem34  8226  fin23lem39  8230  compsscnvlem  8250  compssiso  8254  isf34lem4  8257  enfin1ai  8264  isfin1-3  8266  fin67  8275  dffin7-2  8278  fin1a2lem7  8286  fin1a2lem10  8289  fin1a2lem12  8291  fin1a2lem13  8292  fin12  8293  itunitc1  8300  itunitc  8301  ituniiun  8302  hsmexlem2  8307  hsmexlem4  8309  hsmex  8312  axcc2lem  8316  axcc3  8318  acncc  8320  fin41  8324  dominf  8325  dcomex  8327  axdc2lem  8328  axdc3lem  8330  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  axcclem  8337  ac9  8363  ac6s  8364  ac6sg  8368  ac9s  8373  numthcor  8374  zorn2lem1  8376  zorn2lem4  8379  zorn2lem7  8382  zorng  8384  zornn0g  8385  ttukeylem5  8393  ttukeylem6  8394  ttukeylem7  8395  axdclem  8399  axdclem2  8400  fodomg  8403  fodomb  8404  brdom3  8406  brdom5  8407  brdom4  8408  brdom7disj  8409  brdom6disj  8410  iunfo  8414  ondomon  8438  cardmin  8439  alephval2  8447  dominfac  8448  fpwwe2lem1  8506  fpwwe2lem8  8512  fpwwe2lem11  8515  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  fpwwe  8521  canthwe  8526  canthp1lem1  8527  pwfseqlem1  8533  pwfseqlem2  8534  pwfseqlem3  8535  pwfseqlem4a  8536  pwfseqlem5  8538  pwxpndom2  8540  gchac  8548  gch2  8554  inawinalem  8564  winainflem  8568  winalim2  8571  winafp  8572  gchina  8574  wunfi  8596  intwun  8610  wunex2  8613  uniwun  8615  eltsk2g  8626  inttsk  8649  inar1  8650  rankcf  8652  tskcard  8656  tskuni  8658  gruun  8681  intgru  8689  ingru  8690  wfgru  8691  grudomon  8692  gruina  8693  grur1a  8694  grur1  8695  grutsk  8697  axgroth5  8699  axgroth2  8700  grothpw  8701  grothpwex  8702  axgroth6  8703  grothomex  8704  grothac  8705  axgroth3  8706  grothprim  8709  grothtsk  8710  inaprc  8711  nqereu  8806  nqerf  8807  dmrecnq  8845  ltaddnq  8851  genpnnp  8882  genpnmax  8884  genpcl  8885  nqpr  8891  addclprlem1  8893  mulclprlem  8896  distrlem4pr  8903  1idpr  8906  prlem934  8910  ltaddpr  8911  ltexprlem3  8915  ltexprlem4  8916  ltexprlem6  8918  ltexprlem7  8919  prlem936  8924  reclem2pr  8925  reclem3pr  8926  mulasssr  8965  ltsosr  8969  0idsr  8972  1idsr  8973  ltasr  8975  recexsrlem  8978  mulgt0sr  8980  supsrlem  8986  ltresr  9015  axmulass  9032  axrrecex  9038  axpre-lttri  9040  wuncn  9045  renfdisj  9138  wloglei  9559  lbinfm  9961  supmul1  9973  supmullem1  9974  supmullem2  9975  supmul  9976  dfinfmr  9985  infmsup  9986  infmrgelb  9988  infmrlb  9989  dfnn2  10013  dflt2  10741  xrinfmss2  10889  infmxrgelb  10913  xrinfm0  10915  fzpr  11101  uzrdgfni  11298  axdc4uzlem  11321  axdc4uz  11322  seqval  11334  seqfeq4  11372  serle  11378  seqof  11380  hash1snb  11681  hash2prde  11688  hash2prb  11689  hashxplem  11696  hashmap  11698  hashpw  11699  hashfun  11700  hashbclem  11701  hashfacen  11703  hashf1lem1  11704  hashf1lem2  11705  hashf1  11706  fz1isolem  11710  brfi1uzind  11715  ccatfn  11741  wrdexb  11763  wrdind  11791  shftfval  11885  shftfib  11887  shftfn  11888  2shfti  11895  sqrlem6  12053  rexfiuz  12151  rlimdm  12345  fclim  12347  climshft  12370  fsum2dlem  12554  fsumcom2  12558  fsum0diag2  12566  fsumabs  12580  fsumrlim  12590  fsumo1  12591  fsumiun  12600  incexclem  12616  isumltss  12628  supcvg  12635  xpnnenOLD  12809  rpnnen2lem11  12824  algrf  13064  isprm2lem  13086  isprm2  13087  prmind2  13090  iserodd  13209  4sqlem12  13324  vdwmc  13346  vdwlem10  13358  vdwlem13  13361  ramtlecl  13368  hashbc0  13373  ramval  13376  ramcl2lem  13377  ramub2  13382  0ram  13388  ram0  13390  ramub1lem1  13394  ramub1lem2  13395  ramub1  13396  restfn  13652  elrest  13655  restsspw  13659  prdsval  13678  prdsle  13684  prdsless  13685  prdsleval  13699  pwsle  13714  imasaddfnlem  13753  imasvscafn  13762  imasleval  13766  xpsc0  13785  xpsc1  13786  xpsfrnel2  13790  ismre  13815  fnmre  13816  ismred  13827  mremre  13829  fnmrc  13832  mrcfval  13833  mrisval  13855  mreexexlem4d  13872  isacs2  13878  mreacs  13883  acsfn  13884  acsfn1  13886  acsfn2  13888  cidffn  13903  comfeq  13932  invsym2  13988  oppcsect2  14000  brssc  14014  sscpwex  14015  isssc  14020  issubc  14035  isfuncd  14062  cofucl  14085  funcres2b  14094  funcpropd  14097  setcmon  14242  catcval  14251  fnxpc  14273  xpcval  14274  xpccatid  14285  curf2ndf  14344  drsdirfi  14395  isdrs2  14396  clatl  14543  odupos  14562  oduposb  14563  oduglb  14566  odulub  14568  posglbd  14576  ipoval  14580  ipolerval  14582  fpwipodrs  14590  ipodrsima  14591  isacs5lem  14595  psdmrn  14639  psssdm2  14647  submacs  14765  pwsdiagmhm  14768  gsumwspan  14791  mulgpropd  14923  subgacs  14975  nsgacs  14976  eqgfval  14988  eqgval  14989  gicsubgen  15065  gaid  15076  gaorb  15084  orbsta  15090  symgval  15094  symgbas  15095  symgplusg  15099  sylow1lem2  15233  sylow2alem1  15251  sylow2alem2  15252  sylow2a  15253  sylow2blem1  15254  sylow2blem2  15255  sylow2blem3  15256  sylow3lem1  15261  sylow3lem3  15263  sylow3lem6  15266  efgval  15349  efgval2  15356  efgrelexlemb  15382  efgcpbllema  15386  efgcpbllemb  15387  vrgpfval  15398  frgpuplem  15404  divsabl  15480  frgpnabllem1  15484  gsumval3  15514  gsumzaddlem  15526  gsumzadd  15527  gsum2d  15546  gsum2d2  15548  gsumcom2  15549  gsumxp  15550  dprdfadd  15578  dprdres  15586  subgdmdprd  15592  dprd2dlem1  15599  dprd2d2  15602  ablfac1eulem  15630  pgpfac1lem5  15637  opprsubg  15741  subrgmre  15892  subsubrg2  15895  subrgpropd  15902  lss1d  16039  lssintcl  16040  lssmre  16042  lssacs  16043  pwsdiaglmhm  16133  lbsextlem4  16233  drngnidl  16300  lidldvgen  16326  psrbaglefi  16437  mplcoe1  16528  mplcoe2  16530  ltbval  16532  ltbwe  16533  opsrle  16536  opsrtoslem1  16544  opsrtoslem2  16545  evlslem4  16564  coe1mul2  16662  coe1tm  16665  znleval  16835  cssmre  16920  thlle  16924  pjfval2  16936  istopon  16990  tgval2  17021  bastg  17031  tgdom  17043  distop  17060  indistopon  17065  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  fncld  17086  cldss2  17094  ntreq0  17141  discld  17153  mretopd  17156  toponmre  17157  neisspw  17171  opnnei  17184  tgrest  17223  resttopon  17225  restco  17228  restdis  17242  neitr  17244  ordtbas2  17255  ordtcnv  17265  ordtrest2  17268  pnfnei  17284  mnfnei  17285  iscnp2  17303  subbascn  17318  cnntr  17339  cnrest2  17350  cnpresti  17352  cnprest  17353  cnprest2  17354  ist1-3  17413  hausnei2  17417  isnrm2  17422  dishaus  17446  cmpcovf  17454  fincmp  17456  cmpsublem  17462  cmpsub  17463  cmpcld  17465  uncmp  17466  fiuncmp  17467  hauscmplem  17469  cmpfi  17471  bwth  17473  dfcon2  17482  consuba  17483  cnconn  17485  uncon  17492  t1conperf  17499  is1stc2  17505  1stcfb  17508  2ndcsb  17512  2ndc1stc  17514  1stcrest  17516  2ndcctbss  17518  2ndcdisj  17519  2ndcomap  17521  2ndcsep  17522  dis2ndc  17523  llyi  17537  nllyi  17538  nlly2i  17539  llynlly  17540  subislly  17544  restnlly  17545  restlly  17546  islly2  17547  llyrest  17548  llyidm  17551  nllyidm  17552  hausllycmp  17557  cldllycmp  17558  lly1stc  17559  dislly  17560  hausmapdom  17563  kgenf  17573  iskgen3  17581  llycmpkgen2  17582  1stckgenlem  17585  1stckgen  17586  kgencn2  17589  txuni2  17597  txbas  17599  eltx  17600  ptpjpre1  17603  ptuni2  17608  ptpjcn  17643  ptpjopn  17644  ptclsg  17647  dfac14  17650  xkoccn  17651  txcnp  17652  txcnmpt  17656  prdstopn  17660  txrest  17663  txdis  17664  txindis  17666  txdis1cn  17667  txlly  17668  txnlly  17669  pthaus  17670  txcmplem1  17673  txcmplem2  17674  hausdiag  17677  txlm  17680  tx1stc  17682  tx2ndc  17683  txkgen  17684  xkopt  17687  xkococnlem  17691  xkococn  17692  cnmpt1st  17700  cnmpt2nd  17701  xkofvcn  17716  xkoinjcn  17719  txcon  17721  imasnopn  17722  imasncld  17723  imasncls  17724  qtoptop2  17731  qtopuni  17734  basqtop  17743  tgqtop  17744  hmphdis  17828  indishmph  17830  txhmeo  17835  pt1hmeo  17838  ptuncnv  17839  ptunhmeo  17840  xpstopnlem1  17841  ptcmpfi  17845  xkohmeo  17847  isfbas  17861  isfbas2  17867  fbssfi  17869  trfbas2  17875  isfild  17890  snfil  17896  elfg  17903  fgcl  17910  filcon  17915  fbasrn  17916  filuni  17917  trfil2  17919  cfinfil  17925  csdfil  17926  supfil  17927  zfbas  17928  isufil2  17940  filssufilg  17943  acufl  17949  filufint  17952  uffix  17953  ufildr  17963  fin1aufil  17964  rnelfmlem  17984  rnelfm  17985  fmfnfmlem3  17988  fmfnfmlem4  17989  fmfnfm  17990  ufldom  17994  flimrest  18015  hauspwpwf1  18019  txflf  18038  fclsrest  18056  fclscmp  18062  alexsubb  18077  alexsubALTlem1  18078  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  alexsubALT  18082  ptcmplem2  18084  ptcmplem3  18085  ptcmplem4  18086  ptcmplem5  18087  cnextf  18097  cnextcn  18098  tmdgsum  18125  symgtgp  18131  cldsubg  18140  tgpconcomp  18142  divstgplem  18150  divstgphaus  18152  prdstmdd  18153  tsmsval2  18159  tsmssubm  18172  ustfn  18231  ustfilxp  18242  ustn0  18250  restutopopn  18268  ustuqtop0  18270  ustuqtop1  18271  ustuqtop2  18272  ustuqtop3  18273  ustuqtop4  18274  utopsnneiplem  18277  utopreg  18282  ucnimalem  18310  ucnima  18311  fmucndlem  18321  neipcfilu  18326  imasdsf1olem  18403  xpsdsval  18411  xmetec  18464  prdsbl  18521  stdbdxmet  18545  met1stc  18551  prdsxmslem2  18559  metustidOLD  18589  metustid  18590  metustsymOLD  18591  metustsym  18592  metustexhalfOLD  18593  metustexhalf  18594  metustfbasOLD  18595  metustfbas  18596  blval2  18605  metuel2  18609  metustblOLD  18610  metustbl  18611  restmetu  18617  dscopn  18621  xrtgioo  18837  xrsblre  18842  icccmplem1  18853  icccmplem2  18854  fsumcn  18900  fsum2cn  18901  cnllycmp  18981  isphtpc  19019  pi1blem  19064  iscmet3  19246  metcld2  19259  bcthlem4  19280  minveclem3b  19329  ovolfiniun  19397  ovoliunlem1  19398  ovoliunlem2  19399  finiunmbl  19438  volfiniun  19441  iundisj2  19443  uniioombllem3  19477  vitalilem2  19501  vitalilem3  19502  vitali  19505  mbfimaopnlem  19547  itg1addlem4  19591  mbfi1fseqlem4  19610  mbfi1fseqlem6  19612  itgfsum  19718  ellimc2  19764  limcflf  19768  perfdvf  19790  dvres  19798  dvres2  19799  dvnff  19809  dvcj  19836  dvrec  19841  dvmptfsum  19859  dvef  19864  rolle  19874  dvivthlem1  19892  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  dvfsumlem3  19912  ftc1cn  19927  mpfind  19965  pf1ind  19975  vieta1lem2  20228  elqaalem2  20237  ulmdv  20319  logfac  20495  xrlimcnp  20807  jensenlem1  20825  jensenlem2  20826  jensen  20827  wilthlem2  20852  prmorcht  20961  lgsquadlem1  21138  lgsquadlem2  21139  dchrisumlema  21182  dchrisumlem3  21185  umgraex  21358  isusgra0  21376  usgra2edg  21402  usgrarnedg  21404  usgraedg4  21406  usgraedgreu  21407  usgraexmpl  21420  usgrafis  21429  nbgraf1olem5  21455  nb3graprlem1  21460  cusgrarn  21468  cusgrares  21481  cusgrasize  21487  cusgrafilem1  21488  cusgrafilem2  21489  isuvtx  21497  uvtx01vtx  21501  trls  21536  wlkntrllem2  21560  wlkntrl  21562  constr1trl  21588  2pthon  21602  dfconngra1  21658  eupath  21703  ex-natded9.26  21727  nvss  22072  vsfval  22114  h2hlm  22483  axhcompl-zf  22501  hlim2  22694  hhcmpl  22702  hhcms  22705  shex  22714  isch2  22726  helch  22746  hhsscms  22779  occl  22806  chintcli  22833  dfch2  22909  spanuni  23046  spansni  23059  elnlfn  23431  nmopun  23517  nlelchi  23564  cnlnssadj  23583  adjbd1o  23588  branmfn  23608  pjnmopi  23651  hmopidmchi  23654  abrexss  23993  iuninc  24011  disjabrex  24024  disjabrexf  24025  disjpreima  24026  disjxpin  24028  iundisj2f  24030  suppss2f  24049  fmptdF  24069  fmptcof2  24076  ofpreima  24081  funcnvmptOLD  24082  funcnvmpt  24083  disjdsct  24090  1stpreima  24095  2ndpreima  24096  ctex  24100  iundisj2fi  24153  ishashinf  24159  tosglb  24192  pstmxmet  24292  tpr2rico  24310  esum0  24444  esumc  24446  gsumesum  24451  esumcst  24455  esumfsup  24460  esumpfinvalf  24466  hasheuni  24475  sigaex  24492  sigaval  24493  isrnsigaOLD  24495  pwsiga  24513  sigainb  24519  insiga  24520  dmsigagen  24527  measbase  24551  ismeas  24553  isrnmeas  24554  measiuns  24571  measdivcstOLD  24578  measdivcst  24579  cntmeas  24580  mbfmco2  24615  mbfmcnt  24618  br2base  24619  dya2iocrfn  24629  dya2iocct  24630  dya2iocnrect  24631  dya2iocucvr  24634  sxbrsigalem2  24636  ballotlem2  24746  ballotlemsf1o  24771  ballotlemirc  24789  derangenlem  24857  subfacp1lem1  24865  subfacp1lem3  24868  subfacp1lem4  24869  subfacp1lem5  24870  erdszelem7  24883  erdszelem8  24884  erdsze2lem2  24890  kur14lem9  24900  ptpcon  24920  indispcon  24921  conpcon  24922  cnllyscon  24932  rellyscon  24938  cvmsss2  24961  cvmcov2  24962  cvmliftlem15  24985  cvmlift2lem1  24989  cvmlift2lem12  25001  ghomgrplem  25100  relexpindlem  25139  rtrclreclem.trans  25146  dfrtrcl2  25148  untsucf  25159  dfid4  25183  shftvalg  25208  ntrivcvg  25225  fprodfac  25296  fprod2dlem  25304  fprodcom2  25308  dftr6  25373  coepr  25375  dffr5  25376  dfso2  25377  dfpo2  25378  br8  25379  br6  25380  br4  25381  dfres3  25382  cnvco1  25383  cnvco2  25384  eldm3  25385  pocnv  25387  socnv  25388  fundmpss  25390  fprb  25397  dfdm5  25400  dfrn5  25401  opelco3  25403  elima4  25404  setinds  25405  dfon2lem1  25410  dfon2lem3  25412  dfon2lem6  25415  dfon2lem7  25416  dfon2lem8  25417  dfon2  25419  rdgprc  25422  dfrdg2  25423  dfpred3g  25450  predreseq  25454  predpo  25459  predbrg  25461  setlikespec  25462  predep  25467  preddowncl  25471  preduz  25475  predfz  25478  tz6.26  25480  trpredrec  25516  poseq  25528  soseq  25529  wfrlem5  25542  wfrlem10  25547  wfrlem12  25549  wfrlem13  25550  wfrlem14  25551  wfrlem16  25553  wzel  25575  wsuclem  25576  frrlem5  25586  frrlem11  25594  sltsolem1  25623  nofulllem5  25661  txpss3v  25723  brtxp  25725  brtxp2  25726  pprodss4v  25729  brpprod  25730  brpprod3a  25731  brpprod3b  25732  brsset  25734  idsset  25735  dfon3  25737  brtxpsd  25739  brbigcup  25743  dfbigcup2  25744  fobigcup  25745  elfix  25748  elfix2  25749  dffix2  25750  fixcnv  25753  dfom5b  25757  sscoid  25758  dffun10  25759  elfuns  25760  elfunsg  25761  elsingles  25763  fnsingle  25764  fvsingle  25765  dfiota3  25768  brimage  25771  brimageg  25772  funimage  25773  fnimage  25774  imageval  25775  brcart  25777  brdomaing  25780  brrangeg  25781  brimg  25782  brapply  25783  brcup  25784  brcap  25785  brsuccf  25786  funpartlem  25787  funpartfun  25788  funpartfv  25790  fullfunfv  25792  brrestrict  25794  dfrdg4  25795  tfrqfree  25796  dfint3  25797  imagesset  25798  brlb  25800  altopelaltxp  25821  altxpsspw  25822  brsegle  26042  fvline  26078  liness  26079  ellines  26086  bpoly2  26103  bpoly3  26104  rankung  26107  ranksng  26108  rankelg  26109  rankpwg  26110  rankeq1o  26112  elhf2g  26117  hfext  26124  onsucconi  26187  supaddc  26237  supadd  26238  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  mbfresfi  26253  ftc1cnnc  26279  ftc1anclem6  26285  areacirclem5  26296  trer  26319  finminlem  26321  gtinf  26322  fneer  26368  fnessref  26373  refssfne  26374  islocfin  26376  comppfsc  26387  neibastop1  26388  neibastop2lem  26389  neibastop3  26391  topmeet  26393  topjoin  26394  neifg  26400  tailfb  26406  filnetlem2  26408  filnetlem3  26409  filnetlem4  26410  cover2g  26416  f1opr  26426  inixp  26430  indexdom  26436  frinfm  26437  sdclem2  26446  sdclem1  26447  fdc  26449  isbndx  26491  prdstotbnd  26503  heibor1lem  26518  heiborlem1  26520  heiborlem3  26522  heiborlem4  26523  heiborlem5  26524  heiborlem6  26525  heiborlem8  26527  heiborlem10  26529  ismrer1  26547  riscer  26604  divrngidl  26638  intidl  26639  isfldidl  26678  ispridlc  26680  prtlem10  26714  prtlem13  26717  prtlem16  26718  prtlem19  26727  prter2  26730  prter3  26731  ralxpmap  26742  elrfi  26748  ismrcd1  26752  ismrcd2  26753  istopclsd  26754  ismrc  26755  mrefg2  26761  isnacs3  26764  mzpclall  26784  mzpincl  26791  mzpsubst  26805  mzpcompact2lem  26808  mzpcompact2  26809  eldioph2lem1  26818  eldioph2lem2  26819  eldiophss  26833  diophrex  26834  rexrabdioph  26854  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  rabren3dioph  26876  fphpd  26877  rencldnfilem  26881  pellexlem5  26896  pellex  26898  rmxypairf1o  26974  monotuz  27004  monotoddzzfi  27005  oddcomabszz  27007  2nn0ind  27008  zindbi  27009  mzpcong  27037  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  setindtr  27095  setindtrs  27096  dford3lem2  27098  ttac  27107  pw2f1ocnv  27108  wepwsolem  27116  inisegn0  27118  dnnumch1  27119  fnwe2val  27124  fnwe2lem2  27126  aomclem1  27129  aomclem2  27130  aomclem6  27134  dfac11  27137  kelac2lem  27139  dfac21  27141  islssfg2  27146  lmhmlnmsplit  27162  pwssplit3  27167  filnm  27169  pwslnmlem1  27171  pwslnm  27173  dsmmval  27177  frlmlbs  27226  unxpwdom3  27233  enfixsn  27234  dfacbasgrp  27250  islindf4  27285  lmisfree  27289  lnr2i  27297  lnrfg  27300  hbtlem6  27310  rngunsnply  27355  pmtrfval  27370  symggen  27388  gsumcom3  27431  acsfn1p  27484  sdrgacs  27486  idomsubgmo  27491  fgraphxp  27507  expgrowth  27529  2sbc6g  27592  iotain  27594  compel  27617  ipo0  27628  ifr0  27629  fnchoice  27676  infrglb  27698  stoweidlem31  27756  stoweidlem57  27782  stirlinglem13  27811  funressnfv  27968  dfdfat2  27971  csbafv12g  27977  tz6.12-afv  28013  rlimdmafv  28017  csbaovg  28020  oprabv  28085  wlkelwrd  28295  wlkcompim  28302  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  usg2wlkonot  28350  usg2wotspth  28351  2wot2wont  28353  2spontn0vne  28354  2spot2iun2spont  28358  0egra0rgra  28375  frisusgranb  28387  frgra3vlem1  28390  frgra3vlem2  28391  3vfriswmgralem  28394  2pthfrgra  28401  frgrancvvdeqlem3  28421  frgrancvvdeqlem4  28422  frgrawopreg1  28439  frgrawopreg2  28440  frg2woteq  28449  2spotiundisj  28451  usg2spot2nb  28454  onfrALTlem5  28628  onfrALTlem4  28629  onfrALTlem3  28630  opelopab4  28638  a9e2nd  28645  trsspwALT  28931  trsspwALT2  28932  trsspwALT3  28933  pwtrVD  28937  unipwrVD  28944  unipwr  28945  onfrALTlem5VD  28997  onfrALTlem4VD  28998  onfrALTlem3VD  28999  relopabVD  29013  a9e2ndVD  29020  sspwimp  29030  sspwimpVD  29031  sspwimpcf  29032  sspwimpcfVD  29033  sspwimpALT  29037  sspwimpALT2  29040  a9e2ndALT  29042  bnj23  29083  bnj62  29085  bnj156  29095  bnj219  29100  bnj610  29115  bnj918  29135  bnj927  29139  bnj976  29148  bnj1098  29154  bnj1379  29202  bnj110  29229  bnj98  29238  bnj154  29249  bnj155  29250  bnj535  29261  bnj556  29271  bnj557  29272  bnj581  29279  bnj591  29282  bnj594  29283  bnj580  29284  bnj607  29287  bnj609  29288  bnj600  29290  bnj849  29296  bnj893  29299  bnj908  29302  bnj934  29306  bnj944  29309  bnj964  29314  bnj966  29315  bnj969  29317  bnj970  29318  bnj910  29319  bnj986  29325  bnj999  29328  bnj1018  29333  bnj907  29336  bnj1039  29340  bnj1040  29341  bnj1052  29344  bnj1123  29355  bnj1030  29356  bnj1133  29358  bnj1128  29359  bnj1145  29362  bnj1204  29381  bnj1373  29399  bnj1417  29410  bnj1421  29411  bnj1498  29430  eqlkr2  29898  glbconxN  30175  pmapglbx  30566  pmapglb  30567  pclclN  30688  pclfinN  30697  polval2N  30703  pclfinclN  30747  osumcllem10N  30762  pexmidlem7N  30773  cdleme31sdnN  31184  cdlemefr44  31222  cdleme48fv  31296  cdleme46fvaw  31298  cdleme48bw  31299  cdleme46fsvlpq  31302  cdlemeg46fvcl  31303  cdlemeg49le  31308  cdlemeg46fjgN  31318  cdlemeg46fjv  31320  cdleme48d  31332  cdlemeg49lebilem  31336  cdleme50eq  31338  cdleme50f  31339  cdlemg2jlemOLDN  31390  cdlemg2klem  31392  cdlemk40  31714  cdlemk56  31768  diaglbN  31853  dvhlveclem  31906  dib1dim  31963  dibglbN  31964  diblss  31968  diblsmopel  31969  dicelvalN  31976  diclspsn  31992  cdlemn7  32001  dihordlem7  32012  dihopelvalcpre  32046  xihopellsmN  32052  dihopellsm  32053  dih1  32084  dihmeetlem1N  32088  dihglblem5apreN  32089  dihmeetlem2N  32097  dihglbcpreN  32098  dihmeetlem4preN  32104  dihmeetlem13N  32117  dih1dimatlem  32127  dihatlat  32132  dihjatcclem4  32219  lcdlss  32417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-v 2958
  Copyright terms: Public domain W3C validator