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

Theorem vex 2804
Description: All set variables are sets (see isset 2805). 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 eqid 2296 . 2  |-  x  =  x
2 df-v 2803 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2403 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 200 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   _Vcvv 2801
This theorem is referenced by:  isset  2805  ralv  2814  rexv  2815  reuv  2816  rmov  2817  rabab  2818  sbhypf  2846  ceqex  2911  ralab  2939  rexab  2941  moeq3  2955  mo2icl  2957  reu8  2974  sbc2or  3012  csbvarg  3121  csbiebg  3133  sbcnestgf  3141  sbnfc2  3154  ddif  3321  csbing  3389  dfun2  3417  dfin2  3418  vn0  3475  eqv  3483  abvor0  3485  sbss  3576  csbifg  3606  ifexg  3637  elpwg  3645  dftp2  3692  prnzg  3759  snssg  3767  difprsnss  3769  sneqrg  3798  preq12bg  3807  pwpr  3839  pwtp  3840  pwv  3842  unipr  3857  uniprg  3858  unisng  3860  elintg  3886  elintrabg  3891  intss1  3893  ssint  3894  intmin  3898  intss  3899  intssuni  3900  intmin4  3907  intab  3908  intun  3910  intpr  3911  intprg  3912  uniintsn  3915  iinconst  3930  iuniin  3931  iinss1  3933  dfiin2g  3952  ssiinf  3967  iinss  3969  iinss2  3970  0iin  3976  iinab  3979  iinun2  3984  iundif2  3985  iindif2  3987  iinin2  3988  iinuni  4001  sspwuni  4003  iinpw  4006  iunpwss  4007  brab1  4084  csbopabg  4110  mptv  4128  trint  4144  trintss  4145  vprc  4168  inex1g  4173  ssexg  4176  intex  4183  inuni  4189  axpweq  4203  pwexg  4210  pwuni  4222  axpr  4229  zfpair2  4231  elALT  4234  rext  4238  sspwb  4239  unipw  4240  ssextss  4243  nnullss  4251  exss  4252  opth  4261  opthg  4262  copsexg  4268  copsex4g  4271  moop2  4277  euotd  4283  opelopabsbOLD  4289  opelopabsb  4291  pwin  4313  pwunss  4314  pwssun  4315  pwundifOLD  4317  epelg  4322  epel  4324  dfid3  4326  pofun  4346  epse  4392  wefrc  4403  tron  4431  onfr  4447  sucel  4481  suctr  4491  uniexg  4533  unexb  4536  snnex  4540  uniuni  4543  eusvnf  4545  eusvnfb  4546  reusv6OLD  4561  iunpw  4586  onint  4602  ordpwsuc  4622  unon  4638  ordunisuc  4639  onuninsuci  4647  orduninsuc  4650  limsssuc  4657  limuni3  4659  tfinds  4666  tfindsg  4667  tfindsg2  4668  tfinds2  4670  dfom2  4674  peano5  4695  finds  4698  findsg  4699  finds2  4700  0nelxp  4733  opelxp  4735  opeliunxp  4756  elvv  4764  elvvv  4765  elvvuni  4766  xpsspw  4813  xpsspwOLD  4814  relopabi  4827  opabid2  4831  difopab  4833  xpiindi  4837  ralxpf  4846  relop  4850  cnvco  4881  dfrn2  4884  dfdm4  4888  dmss  4894  dmin  4902  dmiun  4903  dmuni  4904  dm0  4908  dmi  4909  reldm0  4912  elreldm  4919  elrnmpt1  4944  dmrnssfld  4954  dmcoss  4960  dmcosseq  4962  opelresg  4978  resieq  4981  dmres  4992  elres  5006  relssres  5008  resopab  5012  resiexg  5013  iss  5014  dfres2  5018  dfima2  5030  csbima12g  5038  imadmrn  5040  imai  5043  elimasng  5055  args  5057  epini  5059  iniseg  5060  dffr3  5061  dfse2  5062  exse2  5063  cotr  5071  issref  5072  cnvsym  5073  intasym  5074  asymref  5075  asymref2  5076  intirr  5077  brcodir  5078  codir  5079  qfto  5080  poirr2  5083  cnvopab  5099  cnv0  5100  cnvi  5101  cnvdif  5103  rniun  5107  dminss  5111  imainss  5112  ssrnres  5132  rninxp  5133  dminxp  5134  cnvcnv3  5139  dfrel2  5140  dmsnn0  5154  dmsnopg  5160  cnvcnvsn  5166  dmsnsnsn  5167  cnvsng  5174  elxp4  5176  elxp5  5177  cnvresima  5178  dfco2  5188  dfco2a  5189  cores  5192  resco  5193  imaco  5194  rnco  5195  coiun  5198  co02  5202  coi1  5204  coass  5207  relssdmrn  5209  unielrel  5213  unixp0  5222  ressn  5227  cnviin  5228  cnvpo  5229  cnvso  5230  uniabio  5245  iotaval  5246  sniota  5262  csbiotag  5264  dffun2  5281  dffun7  5296  dffun8  5297  dffun9  5298  funopg  5302  funssres  5310  funun  5312  funcnvsn  5313  funcnv2  5325  funcnv  5326  funcnv3  5327  fun2cnv  5328  funcnvuni  5333  imadif  5343  isarep1  5347  2elresin  5371  fnres  5376  fcnvres  5434  fabexg  5438  fconstg  5444  fun11iun  5509  f1osng  5530  dffv3  5537  fv3  5557  fvres  5558  nfunsn  5574  funimass4  5589  ssimaexg  5601  dffv2  5608  dmfco  5609  fvopab6  5637  fndmdif  5645  iinpreima  5671  fvelrn  5677  dff3  5689  dffo4  5692  exfo  5694  f1ompt  5698  fmptco  5707  fsng  5713  dfmpt  5717  fnressn  5721  fressnfv  5723  fvsng  5730  zfrep6  5764  funfvima3  5771  idref  5775  fvclss  5776  fvresex  5778  abrexco  5782  opabex3  5785  imaiun  5787  dff13  5799  foeqcnvco  5820  f1eqcocnv  5821  fliftcnv  5826  isocnv2  5844  isomin  5850  isoini  5851  isofr  5855  isose  5856  f1oweALT  5867  wemoiso  5871  wemoiso2  5872  knatar  5873  oprabid  5898  csbovg  5905  eloprabga  5950  mpt2v  5953  caovmo  6073  f1opw  6088  ofmres  6132  op1stg  6148  op2ndg  6149  1stval2  6153  2ndval2  6154  fo1st  6155  fo2nd  6156  f1stres  6157  f2ndres  6158  fo1stres  6159  fo2ndres  6160  1st2val  6161  2nd2val  6162  xp1st  6165  xp2nd  6166  sbcopeq1a  6188  csbopeq1a  6189  eloprabi  6202  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  ovmptss  6216  fmpt2co  6218  df1st2  6221  df2nd2  6222  1stconst  6223  2ndconst  6224  curry1  6226  curry2  6229  fparlem1  6234  fparlem2  6235  fpar  6238  fsplit  6239  frxp  6241  xporderlem  6242  soxp  6244  fnwelem  6246  fnse  6248  reldmtpos  6258  dmtpos  6262  rntpos  6263  ovtpos  6265  dftpos3  6268  dftpos4  6269  tpostpos  6270  porpss  6297  sorpss  6298  sorpsscmpl  6304  opiota  6306  opabiotafun  6307  opabiota  6309  riotav  6325  csbriotag  6333  onovuni  6375  smogt  6400  tfrlem3  6409  tfrlem8  6416  tfrlem9a  6418  tfrlem16  6425  tz7.44lem1  6434  rdg0g  6456  rdglim2  6461  tz7.48-1  6471  seqomlem1  6478  seqomlem2  6479  abianfplem  6486  oacl  6550  omcl  6551  oecl  6552  oa0r  6553  om0r  6554  om1r  6557  oe1m  6559  oaordi  6560  oawordri  6564  oawordeulem  6568  oalimcl  6574  oaass  6575  oarec  6576  omordi  6580  omwordri  6586  omlimcl  6592  odi  6593  omass  6594  omeulem1  6596  oen0  6600  oeordi  6601  oewordri  6606  oeworde  6607  oeoalem  6610  oeoelem  6612  nnawordex  6651  omabs  6661  omsmolem  6667  ercnv  6697  iserd  6702  eqerlem  6708  eqer  6709  ecdmn0  6718  erth  6720  erdisj  6723  qsss  6736  ecid  6740  qsid  6741  iiner  6747  qsel  6754  erovlem  6770  ecopovsym  6776  ecopovtrn  6777  ecopover  6778  mapprc  6792  fnmap  6795  fnpm  6796  mapval2  6813  pmsspw  6818  mapsn  6825  mapsncnv  6830  ixpconstg  6841  ixpprc  6853  uniixp  6855  ixpin  6857  ixpiin  6858  resixpfo  6870  elixpsn  6871  ixpsnf1o  6872  boxriin  6874  boxcutc  6875  bren  6887  brdomg  6888  domen  6891  domeng  6892  idssen  6922  ener  6924  domtr  6930  ensn1g  6942  en1  6944  en1b  6945  fundmen  6950  fundmeng  6951  mapsnen  6954  unen  6959  domdifsn  6961  xpsnen  6962  xpsneng  6963  xpcomeng  6970  xpassen  6972  xpdom2  6973  xpdom2g  6974  domunsncan  6978  omxpenlem  6979  pw2f1o  6983  fopwdom  6986  sbthlem10  6996  sbth  6997  sbthcl  6999  domunsn  7027  fodomr  7028  pwdom  7029  canth2  7030  canth2g  7031  domssex  7038  xpf1o  7039  mapen  7041  mapunen  7046  map2xp  7047  mapdom2  7048  mapdom3  7049  ssenen  7051  infensuc  7055  nneneq  7060  php  7061  php2  7062  php3  7063  sucdom2  7073  1sdom  7081  unxpdomlem2  7084  unxpdomlem3  7085  isinf  7092  fineqvlem  7093  fineqv  7094  pssnn  7097  ssfi  7099  dif1enOLD  7106  dif1en  7107  findcard  7113  findcard2  7114  findcard2s  7115  ac6sfi  7117  frfi  7118  fimax2g  7119  unbnn2  7130  isfinite2  7131  xpfi  7144  domunfican  7145  fiint  7149  fodomfi  7151  fodomfib  7152  iunfi  7160  pwfilem  7166  ixpfi2  7170  fissuni  7176  fipreima  7177  finsschain  7178  fival  7182  ssfii  7188  fi0  7189  fiin  7191  dffi2  7192  fipwuni  7195  fisn  7196  elfiun  7199  dffi3  7200  fifo  7201  marypha1lem  7202  dfsup2  7211  dfsup2OLD  7212  ordiso2  7246  oismo  7271  hartogslem1  7273  hartogs  7275  wofib  7276  wemappo  7280  wemapso2lem  7281  card2on  7284  brwdom  7297  brwdomn0  7299  brwdom2  7303  wdomtr  7305  wdompwdom  7308  canthwdom  7309  xpwdomg  7315  unxpwdom2  7318  ixpiunwdom  7321  elirrv  7327  zfregfr  7332  inf0  7338  inf3lema  7341  inf3lemd  7344  inf3lem1  7345  inf3lem2  7346  inf3lem3  7347  inf3lem5  7349  inf3lem6  7350  inf3lem7  7351  inf3  7352  infeq5  7354  omex  7360  dfom3  7364  dfom5  7367  infdifsn  7373  cantnfdm  7381  cantnfval  7385  cantnfval2  7386  cantnflt  7389  cantnff  7391  oemapso  7400  cantnflem1  7407  wemapwe  7416  cnfcom  7419  cnfcom3clem  7424  epfrs  7429  tcvalg  7439  tctr  7441  tcmin  7442  r1sdom  7462  r1val1  7474  tz9.12lem1  7475  tz9.12lem3  7477  tz9.13  7479  tz9.13g  7480  rankf  7482  unir1  7501  rankvalg  7505  rankonidlem  7516  r1val2  7525  bndrank  7529  ranklim  7532  r1pwOLD  7534  rankunb  7538  rankuni2b  7541  rankuni  7551  rankval4  7555  rankxplim  7565  rankxplim3  7567  rankxpsuc  7568  tcrank  7570  cp  7577  bnd2  7579  kardex  7580  karden  7581  cardf2  7592  tskwe  7599  cardlim  7621  harcard  7627  cardiun  7631  pm54.43  7649  r0weon  7656  infxpenlem  7657  infxpenc2lem2  7663  fseqenlem1  7667  fseqenlem2  7668  fseqen  7670  dfac8alem  7672  dfac8clem  7675  ac10ct  7677  ween  7678  acnlem  7691  finacn  7693  acndom  7694  acndom2  7697  wdomfil  7704  infpwfien  7705  alephon  7712  alephcard  7713  alephordi  7717  cardaleph  7732  alephval3  7753  iunfictbso  7757  aceq3lem  7763  dfac3  7764  dfac4  7765  dfac5lem1  7766  dfac5lem2  7767  dfac5lem3  7768  dfac5lem4  7769  dfac5lem5  7770  dfac5  7771  dfac2a  7772  dfac2  7773  dfac8  7777  dfac9  7778  dfac10b  7781  acacni  7782  dfacacn  7783  dfac13  7784  kmlem1  7792  kmlem2  7793  kmlem9  7800  kmlem10  7801  kmlem11  7802  kmlem12  7803  kmlem13  7804  cdafn  7811  pwsdompw  7846  infmap2  7860  ackbij1lem5  7866  ackbij1lem8  7869  ackbij2lem3  7883  ackbij2  7885  cflm  7892  cardcf  7894  cfeq0  7898  cfsuc  7899  cff1  7900  cfflb  7901  cfval2  7902  cflim2  7905  cfss  7907  cfslb2n  7910  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  coftr  7915  sornom  7919  infpssr  7950  fin4en1  7951  fin23lem11  7959  enfin2i  7963  fin23lem26  7967  fin23lem14  7975  fin23lem16  7977  fin23lem17  7980  fin23lem21  7981  fin23lem32  7986  fin23lem34  7988  fin23lem39  7992  compsscnvlem  8012  compssiso  8016  isf34lem4  8019  enfin1ai  8026  isfin1-3  8028  fin67  8037  dffin7-2  8040  fin1a2lem7  8048  fin1a2lem10  8051  fin1a2lem12  8053  fin1a2lem13  8054  fin12  8055  itunitc1  8062  itunitc  8063  ituniiun  8064  hsmexlem2  8069  hsmexlem4  8071  hsmex  8074  axcc2lem  8078  axcc3  8080  acncc  8082  fin41  8086  dominf  8087  dcomex  8089  axdc2lem  8090  axdc3lem  8092  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  ac9  8126  ac6s  8127  ac6sg  8131  ac9s  8136  numthcor  8137  zorn2lem1  8139  zorn2lem4  8142  zorn2lem7  8145  zorng  8147  zornn0g  8148  ttukeylem5  8156  ttukeylem6  8157  ttukeylem7  8158  axdclem  8162  axdclem2  8163  fodomg  8166  fodomb  8167  brdom3  8169  brdom5  8170  brdom4  8171  brdom7disj  8172  brdom6disj  8173  iunfo  8177  ondomon  8201  cardmin  8202  alephval2  8210  dominfac  8211  fpwwe2lem1  8269  fpwwe2lem8  8275  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  fpwwe  8284  canthwe  8289  canthp1lem1  8290  pwfseqlem1  8296  pwfseqlem2  8297  pwfseqlem3  8298  pwfseqlem4a  8299  pwfseqlem5  8301  pwxpndom2  8303  gchac  8311  gch2  8317  inawinalem  8327  winainflem  8331  winalim2  8334  winafp  8335  gchina  8337  wunfi  8359  intwun  8373  wunex2  8376  uniwun  8378  eltsk2g  8389  inttsk  8412  inar1  8413  rankcf  8415  tskcard  8419  tskuni  8421  gruun  8444  intgru  8452  ingru  8453  wfgru  8454  grudomon  8455  gruina  8456  grur1a  8457  grur1  8458  grutsk  8460  axgroth5  8462  axgroth2  8463  grothpw  8464  grothpwex  8465  axgroth6  8466  grothomex  8467  grothac  8468  axgroth3  8469  grothprim  8472  grothtsk  8473  inaprc  8474  nqereu  8569  nqerf  8570  dmrecnq  8608  ltaddnq  8614  genpnnp  8645  genpnmax  8647  genpcl  8648  nqpr  8654  addclprlem1  8656  mulclprlem  8659  distrlem4pr  8666  1idpr  8669  prlem934  8673  ltaddpr  8674  ltexprlem3  8678  ltexprlem4  8679  ltexprlem6  8681  ltexprlem7  8682  prlem936  8687  reclem2pr  8688  reclem3pr  8689  mulasssr  8728  ltsosr  8732  0idsr  8735  1idsr  8736  ltasr  8738  recexsrlem  8741  mulgt0sr  8743  supsrlem  8749  ltresr  8778  axmulass  8795  axrrecex  8801  axpre-lttri  8803  wuncn  8808  renfdisj  8901  wloglei  9321  lbinfm  9723  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  dfinfmr  9747  infmsup  9748  infmrgelb  9750  infmrlb  9751  dfnn2  9775  dflt2  10498  xrinfmss2  10645  infmxrgelb  10669  xrinfm0  10671  fzpr  10856  uzrdgfni  11037  axdc4uzlem  11060  axdc4uz  11061  seqval  11073  seqfeq4  11111  serle  11117  seqof  11119  hashxplem  11401  hashmap  11403  hashpw  11404  hashfun  11405  hashbclem  11406  hashfacen  11408  hashf1lem1  11409  hashf1lem2  11410  hashf1  11411  fz1isolem  11415  ccatfn  11443  wrdexb  11465  wrdind  11493  shftfval  11581  shftfib  11583  shftfn  11584  2shfti  11591  sqrlem6  11749  rexfiuz  11847  rlimdm  12041  fclim  12043  climshft  12066  fsum2dlem  12249  fsumcom2  12253  fsum0diag2  12261  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  incexclem  12311  isumltss  12323  supcvg  12330  xpnnenOLD  12504  rpnnen2lem11  12519  algrf  12759  isprm2lem  12781  isprm2  12782  prmind2  12785  iserodd  12904  4sqlem12  13019  vdwmc  13041  vdwlem10  13053  vdwlem13  13056  ramtlecl  13063  hashbc0  13068  ramval  13071  ramcl2lem  13072  ramub2  13077  0ram  13083  ram0  13085  ramub1lem1  13089  ramub1lem2  13090  ramub1  13091  restfn  13345  elrest  13348  restsspw  13352  prdsval  13371  prdsle  13377  prdsless  13378  prdsleval  13392  pwsle  13407  imasaddfnlem  13446  imasvscafn  13455  imasleval  13459  xpsc0  13478  xpsc1  13479  xpsfrnel2  13483  ismre  13508  fnmre  13509  ismred  13520  mremre  13522  fnmrc  13525  mrcfval  13526  mrisval  13548  mreexexlem4d  13565  isacs2  13571  mreacs  13576  acsfn  13577  acsfn1  13579  acsfn2  13581  cidffn  13596  comfeq  13625  invsym2  13681  oppcsect2  13693  brssc  13707  sscpwex  13708  isssc  13713  issubc  13728  isfuncd  13755  cofucl  13778  funcres2b  13787  funcpropd  13790  setcmon  13935  catcval  13944  fnxpc  13966  xpcval  13967  xpccatid  13978  curf2ndf  14037  drsdirfi  14088  isdrs2  14089  clatl  14236  odupos  14255  oduposb  14256  oduglb  14259  odulub  14261  posglbd  14269  ipoval  14273  ipolerval  14275  fpwipodrs  14283  ipodrsima  14284  isacs5lem  14288  psdmrn  14332  psssdm2  14340  submacs  14458  pwsdiagmhm  14461  gsumwspan  14484  mulgpropd  14616  subgacs  14668  nsgacs  14669  eqgfval  14681  eqgval  14682  gicsubgen  14758  gaid  14769  gaorb  14777  orbsta  14783  symgval  14787  symgbas  14788  symgplusg  14792  sylow1lem2  14926  sylow2alem1  14944  sylow2alem2  14945  sylow2a  14946  sylow2blem1  14947  sylow2blem2  14948  sylow2blem3  14949  sylow3lem1  14954  sylow3lem3  14956  sylow3lem6  14959  efgval  15042  efgval2  15049  efgrelexlemb  15075  efgcpbllema  15079  efgcpbllemb  15080  vrgpfval  15091  frgpuplem  15097  divsabl  15173  frgpnabllem1  15177  gsumval3  15207  gsumzaddlem  15219  gsumzadd  15220  gsum2d  15239  gsum2d2  15241  gsumcom2  15242  gsumxp  15243  dprdfadd  15271  dprdres  15279  subgdmdprd  15285  dprd2dlem1  15292  dprd2d2  15295  ablfac1eulem  15323  pgpfac1lem5  15330  opprsubg  15434  subrgmre  15585  subsubrg2  15588  subrgpropd  15595  lss1d  15736  lssintcl  15737  lssmre  15739  lssacs  15740  pwsdiaglmhm  15830  islbs3  15924  lbsextlem4  15930  drngnidl  15997  lidldvgen  16023  psrbaglefi  16134  mplcoe1  16225  mplcoe2  16227  ltbval  16229  ltbwe  16230  opsrle  16233  opsrtoslem1  16241  opsrtoslem2  16242  evlslem4  16261  coe1mul2  16362  coe1tm  16365  znleval  16524  cssmre  16609  thlle  16613  pjfval2  16625  istopon  16679  tgval2  16710  bastg  16720  tgdom  16732  distop  16749  indistopon  16754  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  fncld  16775  cldss2  16783  ntreq0  16830  discld  16842  mretopd  16845  toponmre  16846  neisspw  16860  opnnei  16873  tgrest  16906  resttopon  16908  restco  16911  restdis  16925  ordtbas2  16937  ordtcnv  16947  ordtrest2  16950  pnfnei  16966  mnfnei  16967  iscnp2  16985  subbascn  17000  cnntr  17020  cnrest2  17030  cnpresti  17032  cnprest  17033  cnprest2  17034  ist1-3  17093  hausnei2  17097  isnrm2  17102  dishaus  17126  cmpcovf  17134  fincmp  17136  cmpsublem  17142  cmpsub  17143  cmpcld  17145  uncmp  17146  fiuncmp  17147  hauscmplem  17149  cmpfi  17151  dfcon2  17161  consuba  17162  cnconn  17164  uncon  17171  t1conperf  17178  is1stc2  17184  1stcfb  17187  2ndcsb  17191  2ndc1stc  17193  1stcrest  17195  2ndcctbss  17197  2ndcdisj  17198  2ndcomap  17200  2ndcsep  17201  dis2ndc  17202  llyi  17216  nllyi  17217  nlly2i  17218  llynlly  17219  subislly  17223  restnlly  17224  restlly  17225  islly2  17226  llyrest  17227  llyidm  17230  nllyidm  17231  hausllycmp  17236  cldllycmp  17237  lly1stc  17238  dislly  17239  hausmapdom  17242  kgenf  17252  iskgen3  17260  llycmpkgen2  17261  1stckgenlem  17264  1stckgen  17265  kgencn2  17268  txuni2  17276  txbas  17278  eltx  17279  ptpjpre1  17282  ptuni2  17287  ptpjcn  17321  ptpjopn  17322  ptclsg  17325  dfac14  17328  xkoccn  17329  txcnp  17330  txcnmpt  17334  prdstopn  17338  txrest  17341  txdis  17342  txindis  17344  txdis1cn  17345  txlly  17346  txnlly  17347  pthaus  17348  txcmplem1  17351  txcmplem2  17352  hausdiag  17355  txlm  17358  tx1stc  17360  tx2ndc  17361  txkgen  17362  xkopt  17365  xkococnlem  17369  xkococn  17370  cnmpt1st  17378  cnmpt2nd  17379  xkofvcn  17394  xkoinjcn  17397  txcon  17399  qtoptop2  17406  qtopuni  17409  basqtop  17418  tgqtop  17419  hmphdis  17503  indishmph  17505  txhmeo  17510  pt1hmeo  17513  ptuncnv  17514  ptunhmeo  17515  xpstopnlem1  17516  ptcmpfi  17520  xkohmeo  17522  isfbas  17540  isfbas2  17546  fbssfi  17548  trfbas2  17554  isfild  17569  snfil  17575  elfg  17582  fgcl  17589  filcon  17594  fbasrn  17595  filuni  17596  trfil2  17598  cfinfil  17604  csdfil  17605  supfil  17606  zfbas  17607  isufil2  17619  filssufilg  17622  acufl  17628  filufint  17631  uffix  17632  ufinffr  17640  ufildr  17642  fin1aufil  17643  rnelfmlem  17663  rnelfm  17664  fmfnfmlem3  17667  fmfnfmlem4  17668  fmfnfm  17669  ufldom  17673  flimrest  17694  hauspwpwf1  17698  txflf  17717  fclsrest  17735  fclscmp  17741  alexsubb  17756  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  ptcmplem4  17765  ptcmplem5  17766  tmdgsum  17794  symgtgp  17800  cldsubg  17809  tgpconcomp  17811  divstgplem  17819  divstgphaus  17821  prdstmdd  17822  tsmsval2  17828  tsmssubm  17841  imasdsf1olem  17953  xpsdsval  17961  xmetec  17996  prdsbl  18053  stdbdxmet  18077  met1stc  18083  prdsxmslem2  18091  dscopn  18112  xrtgioo  18328  xrsblre  18333  icccmplem1  18343  icccmplem2  18344  fsumcn  18390  fsum2cn  18391  cnllycmp  18470  isphtpc  18508  pi1blem  18553  iscmet3  18735  metcld2  18748  bcthlem4  18765  minveclem3b  18808  ovolfiniun  18876  ovoliunlem1  18877  ovoliunlem2  18878  finiunmbl  18917  volfiniun  18920  iundisj2  18922  uniioombllem3  18956  vitalilem2  18980  vitalilem3  18981  vitali  18984  mbfimaopnlem  19026  itg1addlem4  19070  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  itgfsum  19197  ellimc2  19243  limcflf  19247  perfdvf  19269  dvres  19277  dvres2  19278  dvnff  19288  dvcj  19315  dvrec  19320  dvmptfsum  19338  dvef  19343  rolle  19353  dvivthlem1  19371  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem3  19391  ftc1cn  19406  mpfind  19444  pf1ind  19454  vieta1lem2  19707  elqaalem2  19716  ulmdv  19796  logfac  19970  xrlimcnp  20279  jensenlem1  20297  jensenlem2  20298  jensen  20299  wilthlem2  20323  prmorcht  20432  lgsquadlem1  20609  lgsquadlem2  20610  dchrisumlema  20653  dchrisumlem3  20656  ex-natded9.26  20822  nvss  21165  vsfval  21207  h2hlm  21576  axhcompl-zf  21594  hlim2  21787  hhcmpl  21795  hhcms  21798  shex  21807  isch2  21819  helch  21839  hhsscms  21872  occl  21899  chintcli  21926  dfch2  22002  spanuni  22139  spansni  22152  elnlfn  22524  nmopun  22610  nlelchi  22657  cnlnssadj  22676  adjbd1o  22681  branmfn  22701  pjnmopi  22744  hmopidmchi  22747  abrexss  23056  ballotlem2  23063  ballotlemsf1o  23088  ballotlemirc  23106  iuninc  23174  suppss2f  23216  fmptdF  23236  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  tpr2rico  23311  ctex  23351  disjabrex  23374  disjabrexf  23375  disjpreima  23376  iundisj2fi  23379  iundisj2f  23381  disjdsct  23384  ishashinf  23404  esumel  23441  esum0  23443  esumc  23445  esumcst  23451  esumpfinvalf  23459  hasheuni  23468  sigaex  23485  sigaval  23486  isrnsigaOLD  23488  pwsiga  23506  sigainb  23512  insiga  23513  dmsigagen  23520  measbase  23543  ismeas  23545  isrnmeas  23546  measiuns  23559  measdivcstOLD  23566  measdivcst  23567  cntmeas  23568  mbfmco2  23585  mbfmcnt  23588  br2base  23589  coinfliplem  23694  dmgmseqn0  23711  derangenlem  23717  subfacp1lem1  23725  subfacp1lem3  23728  subfacp1lem4  23729  subfacp1lem5  23730  erdszelem7  23743  erdszelem8  23744  erdsze2lem2  23750  kur14lem9  23760  ptpcon  23779  indispcon  23780  conpcon  23781  cnllyscon  23791  rellyscon  23797  cvmsss2  23820  cvmcov2  23821  cvmliftlem15  23844  cvmlift2lem1  23848  cvmlift2lem12  23860  umgraex  23890  eupath  23920  ghomgrplem  24011  relexpindlem  24051  rtrclreclem.trans  24058  dfrtrcl2  24060  untsucf  24071  dftr6  24178  coepr  24180  dffr5  24181  dfso2  24182  dfpo2  24183  br8  24184  br6  24185  br4  24186  dfres3  24187  cnvco1  24188  cnvco2  24189  eldm3  24190  fundmpss  24193  fprb  24200  dfdm5  24203  dfrn5  24204  setinds  24205  dfon2lem1  24210  dfon2lem3  24212  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  rdgprc  24222  dfrdg2  24223  predreseq  24250  predpo  24255  predbrg  24257  setlikespec  24258  predep  24263  preddowncl  24267  preduz  24271  predfz  24274  tz6.26  24276  trpredrec  24312  poseq  24324  soseq  24325  wfrlem5  24331  wfrlem10  24336  wfrlem12  24338  wfrlem13  24339  wfrlem14  24340  wfrlem16  24342  tfrALTlem  24347  frrlem5  24356  frrlem11  24364  sltsolem1  24393  nofulllem5  24431  txpss3v  24489  brtxp  24491  brtxp2  24492  pprodss4v  24495  brpprod  24496  brpprod3a  24497  brpprod3b  24498  brsset  24500  idsset  24501  dfon3  24503  brtxpsd  24505  brbigcup  24509  dfbigcup2  24510  fobigcup  24511  elfix  24514  elfix2  24515  dffix2  24516  fixcnv  24519  limitssson  24522  dfom5b  24523  dffun10  24524  elfuns  24525  elfunsg  24526  elsingles  24528  fnsingle  24529  fvsingle  24530  dfiota3  24533  brimage  24536  brimageg  24537  funimage  24538  fnimage  24539  imageval  24540  brcart  24542  brdomaing  24545  brrangeg  24546  brimg  24547  brapply  24548  brcup  24549  brcap  24550  brsuccf  24551  funpartlem  24552  funpartfun  24553  funpartfv  24555  fullfunfv  24557  brrestrict  24559  dfrdg4  24560  tfrqfree  24561  altopelaltxp  24582  altxpsspw  24583  brsegle  24803  fvline  24839  liness  24840  ellines  24847  bpoly2  24864  bpoly3  24865  rankung  24868  ranksng  24869  rankelg  24870  rankpwg  24871  rankeq1o  24873  elhf2g  24878  hfext  24885  onsucconi  24948  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnc  25005  ftc1cnnc  25025  areacirclem6  25033  tpssg  25035  fatesg  25059  eqvinopb  25068  copsexgb  25069  elo  25144  stcat  25147  splint  25151  domfldrefc  25160  ranfldrefc  25161  domrngref  25163  domintrefb  25166  restidsing  25179  prj1b  25182  prj3  25183  eloi  25189  elintabg  25193  domintrefc  25228  inttpemp  25242  mapmapmap  25251  injsurinj  25252  npincppr  25262  repfuntw  25263  repcpwti  25264  cbcpcp  25265  cbicp  25269  prjmapcp2  25273  dstr  25274  iscst4  25280  islatalg  25286  domrancur1c  25305  mnlmxl2  25372  defse3  25375  inpc  25380  inposet  25381  tolat  25389  toplat  25393  dfdir2  25394  prodeq3ii  25411  fprodser  25423  symgfo  25471  svs2  25590  inttop2  25618  sallnei  25632  nsn  25633  dmhmph  25636  rnhmph  25637  intopcoaconlem3b  25641  intopcoaconlem3  25642  qusp  25645  efilcp  25655  fgsb2  25658  bwt2  25695  dmrngcmp  25854  dualded  25886  ishomd  25893  vtarsuelt  25998  fnctartar  26010  fnctartar2  26011  dfiunv2  26019  prismorcset2  26021  domcatfun  26028  codcatfun  26037  idcatfun  26044  empklst  26112  fnckle  26148  pfsubkl  26150  pgapspf2  26156  isconcl5a  26204  isconcl5ab  26205  bosser  26270  pdiveql  26271  abhp2  26278  bhp2a  26279  cnvresimaOLD  26329  trer  26330  finminlem  26334  gtinf  26337  fneer  26391  fnessref  26396  refssfne  26397  islocfin  26399  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  neibastop3  26414  topmeet  26416  topjoin  26417  neifg  26423  tailfb  26429  filnetlem2  26431  filnetlem3  26432  filnetlem4  26433  cover2g  26462  f1opr  26494  inixp  26502  indexdom  26516  frinfm  26519  sdclem2  26555  sdclem1  26556  fdc  26558  isbndx  26609  prdstotbnd  26621  heibor1lem  26636  heiborlem1  26638  heiborlem3  26640  heiborlem4  26641  heiborlem5  26642  heiborlem6  26643  heiborlem8  26645  heiborlem10  26647  ismrer1  26665  riscer  26722  divrngidl  26756  intidl  26757  isfldidl  26796  ispridlc  26798  prtlem10  26836  prtlem13  26839  prtlem16  26840  prtlem19  26849  prter2  26852  prter3  26853  ralxpmap  26864  elrfi  26872  ismrcd1  26876  ismrcd2  26877  istopclsd  26878  ismrc  26879  mrefg2  26885  isnacs3  26888  mzpclall  26908  mzpincl  26915  mzpsubst  26929  mzpcompact2lem  26932  mzpcompact2  26933  eldioph2lem1  26942  eldioph2lem2  26943  eldiophss  26957  diophrex  26958  rexrabdioph  26978  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  rabren3dioph  27001  fphpd  27002  rencldnfilem  27006  pellexlem5  27021  pellex  27023  rmxypairf1o  27099  monotuz  27129  monotoddzzfi  27130  oddcomabszz  27132  2nn0ind  27133  zindbi  27134  mzpcong  27162  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  setindtr  27220  setindtrs  27221  dford3lem2  27223  ttac  27232  pw2f1ocnv  27233  wepwsolem  27241  inisegn0  27243  dnnumch1  27244  fnwe2val  27249  fnwe2lem2  27251  aomclem1  27254  aomclem2  27255  aomclem6  27259  dfac11  27263  kelac2lem  27265  dfac21  27267  islssfg2  27272  lmhmlnmsplit  27288  pwssplit3  27293  filnm  27295  pwslnmlem1  27297  pwslnm  27299  dsmmval  27303  frlmlbs  27352  unxpwdom3  27359  enfixsn  27360  dfacbasgrp  27376  islindf4  27411  lmisfree  27415  lnr2i  27423  lnrfg  27426  hbtlem6  27436  rngunsnply  27481  pmtrfval  27496  symggen  27514  gsumcom3  27557  acsfn1p  27610  sdrgacs  27612  idomsubgmo  27617  fgraphxp  27633  expgrowth  27655  2sbc6g  27718  iotain  27720  compel  27743  ipo0  27755  ifr0  27756  fnchoice  27803  infrglb  27825  stoweidlem31  27883  stoweidlem57  27909  stoweidlem62  27914  stirlinglem13  27938  funressnfv  28096  dfdfat2  28099  csbafv12g  28105  tz6.12-afv  28141  rlimdmafv  28145  csbaovg  28148  opabex3d  28190  0neqopab  28192  isusgra0  28238  usgraexmpl  28267  nb3graprlem1  28287  isuvtx  28301  uvtx01vtx  28305  trls  28335  wlkntrllem3  28347  wlkntrllem4  28348  frgra3vlem1  28424  frgra3vlem2  28425  3vfriswmgralem  28428  onfrALTlem5  28606  onfrALTlem4  28607  onfrALTlem3  28608  opelopab4  28616  a9e2nd  28623  trsspwALT  28908  trsspwALT2  28909  trsspwALT3  28910  pwtrVD  28914  pwtrOLD  28915  unipwrVD  28924  unipwr  28925  onfrALTlem5VD  28977  onfrALTlem4VD  28978  onfrALTlem3VD  28979  relopabVD  28993  a9e2ndVD  29000  sspwimp  29010  sspwimpVD  29011  sspwimpcf  29012  sspwimpcfVD  29013  sspwimpALT  29017  sspwimpALT2  29021  a9e2ndALT  29023  bnj23  29060  bnj62  29062  bnj156  29072  bnj219  29077  bnj610  29092  bnj918  29112  bnj927  29116  bnj976  29125  bnj1098  29131  bnj1379  29179  bnj110  29206  bnj98  29215  bnj154  29226  bnj155  29227  bnj535  29238  bnj556  29248  bnj557  29249  bnj581  29256  bnj591  29259  bnj594  29260  bnj580  29261  bnj607  29264  bnj609  29265  bnj600  29267  bnj849  29273  bnj893  29276  bnj908  29279  bnj934  29283  bnj944  29286  bnj964  29291  bnj966  29292  bnj969  29294  bnj970  29295  bnj910  29296  bnj986  29302  bnj999  29305  bnj1018  29310  bnj907  29313  bnj1039  29317  bnj1040  29318  bnj1052  29321  bnj1123  29332  bnj1030  29333  bnj1133  29335  bnj1128  29336  bnj1145  29339  bnj1204  29358  bnj1373  29376  bnj1417  29387  bnj1421  29388  bnj1498  29407  eqlkr2  29912  glbconxN  30189  pmapglbx  30580  pmapglb  30581  pclclN  30702  pclfinN  30711  polval2N  30717  pclfinclN  30761  osumcllem10N  30776  pexmidlem7N  30787  cdleme31sdnN  31198  cdlemefr44  31236  cdleme48fv  31310  cdleme46fvaw  31312  cdleme48bw  31313  cdleme46fsvlpq  31316  cdlemeg46fvcl  31317  cdlemeg49le  31322  cdlemeg46fjgN  31332  cdlemeg46fjv  31334  cdleme48d  31346  cdlemeg49lebilem  31350  cdleme50eq  31352  cdleme50f  31353  cdlemg2jlemOLDN  31404  cdlemg2klem  31406  cdlemk40  31728  cdlemk56  31782  diaglbN  31867  dvhlveclem  31920  dib1dim  31977  dibglbN  31978  diblss  31982  diblsmopel  31983  dicelvalN  31990  diclspsn  32006  cdlemn7  32015  dihordlem7  32026  dihopelvalcpre  32060  xihopellsmN  32066  dihopellsm  32067  dih1  32098  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetlem4preN  32118  dihmeetlem13N  32131  dih1dimatlem  32141  dihatlat  32146  dihjatcclem4  32233  lcdlss  32431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator