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

Theorem vex 2876
Description: All set variables are sets (see isset 2877). 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 2366 . 2  |-  x  =  x
2 df-v 2875 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2473 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 200 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1647    e. wcel 1715   _Vcvv 2873
This theorem is referenced by:  isset  2877  ralv  2886  rexv  2887  reuv  2888  rmov  2889  rabab  2890  sbhypf  2918  ceqex  2983  ralab  3012  rexab  3014  moeq3  3028  mo2icl  3030  reu8  3047  sbc2or  3085  csbvarg  3194  csbiebg  3206  sbcnestgf  3214  sbnfc2  3227  ddif  3395  csbing  3464  dfun2  3492  dfin2  3493  vn0  3550  eqv  3558  abvor0  3560  sbss  3652  csbifg  3682  ifexg  3713  elpwg  3721  exsnrex  3763  dftp2  3769  prnzg  3839  snssg  3847  difprsnss  3849  sneqrg  3882  preq12bg  3891  pwpr  3925  pwtp  3926  pwv  3928  unipr  3943  uniprg  3944  unisng  3946  elintg  3972  elintrabg  3977  intss1  3979  ssint  3980  intmin  3984  intss  3985  intssuni  3986  intmin4  3993  intab  3994  intun  3996  intpr  3997  intprg  3998  uniintsn  4001  iinconst  4016  iuniin  4017  iinss1  4019  dfiin2g  4038  ssiinf  4053  iinss  4055  iinss2  4056  0iin  4062  iinab  4065  iinun2  4070  iundif2  4071  iindif2  4073  iinin2  4074  iinuni  4087  sspwuni  4089  iinpw  4092  iunpwss  4093  brab1  4170  csbopabg  4196  mptv  4214  trint  4230  trintss  4231  vprc  4254  inex1g  4259  ssexg  4262  intex  4269  inuni  4275  axpweq  4289  pwexg  4296  pwuni  4308  axpr  4315  zfpair2  4317  elALT  4320  rext  4325  sspwb  4326  unipw  4327  ssextss  4330  nnullss  4338  exss  4339  opth  4348  opthg  4349  copsexg  4355  copsex4g  4358  moop2  4364  euotd  4370  opelopabsbOLD  4376  opelopabsb  4378  pwin  4400  pwunss  4401  pwssun  4402  pwundifOLD  4403  epelg  4409  epel  4411  dfid3  4413  pofun  4433  epse  4479  wefrc  4490  tron  4518  onfr  4534  sucel  4568  suctr  4578  uniexg  4620  unexb  4623  snnex  4627  uniuni  4630  eusvnf  4632  eusvnfb  4633  reusv6OLD  4648  iunpw  4673  onint  4689  ordpwsuc  4709  unon  4725  ordunisuc  4726  onuninsuci  4734  orduninsuc  4737  limsssuc  4744  limuni3  4746  tfinds  4753  tfindsg  4754  tfindsg2  4755  tfinds2  4757  dfom2  4761  peano5  4782  finds  4785  findsg  4786  finds2  4787  0nelxp  4820  opelxp  4822  opeliunxp  4843  elvv  4851  elvvv  4852  elvvuni  4853  xpsspw  4900  xpsspwOLD  4901  relopabi  4914  opabid2  4918  difopab  4920  xpiindi  4924  ralxpf  4933  relop  4937  cnvco  4968  dfrn2  4971  dfdm4  4975  dmss  4981  dmin  4989  dmiun  4990  dmuni  4991  dm0  4995  dmi  4996  reldm0  4999  elreldm  5006  elrnmpt1  5031  dmrnssfld  5041  dmcoss  5047  dmcosseq  5049  opelresg  5065  resieq  5068  dmres  5079  elres  5093  relssres  5095  resopab  5099  resiexg  5100  iss  5101  dfres2  5105  dfima2  5117  csbima12g  5125  imadmrn  5127  imai  5130  elimasng  5142  args  5144  epini  5146  iniseg  5147  dffr3  5148  dfse2  5149  exse2  5150  cotr  5158  issref  5159  cnvsym  5160  intasym  5161  asymref  5162  asymref2  5163  intirr  5164  brcodir  5165  codir  5166  qfto  5167  poirr2  5170  cnvopab  5186  cnv0  5187  cnvi  5188  cnvdif  5190  rniun  5194  dminss  5198  imainss  5199  ssrnres  5219  rninxp  5220  dminxp  5221  cnvcnv3  5226  dfrel2  5227  dmsnn0  5241  dmsnopg  5247  cnvcnvsn  5253  dmsnsnsn  5254  cnvsng  5261  elxp4  5263  elxp5  5264  cnvresima  5265  dfco2  5275  dfco2a  5276  cores  5279  resco  5280  imaco  5281  rnco  5282  coiun  5285  co02  5289  coi1  5291  coass  5294  relssdmrn  5296  unielrel  5300  unixp0  5309  ressn  5314  cnviin  5315  cnvpo  5316  cnvso  5317  uniabio  5332  iotaval  5333  sniota  5349  csbiotag  5351  dffun2  5368  dffun7  5383  dffun8  5384  dffun9  5385  funopg  5389  funssres  5397  funun  5399  funcnvsn  5400  funcnv2  5414  funcnv  5415  funcnv3  5416  fun2cnv  5417  funcnvuni  5422  imadif  5432  isarep1  5436  2elresin  5460  fnres  5465  fcnvres  5524  fabexg  5528  fconstg  5534  fun11iun  5599  f1osng  5620  dffv3  5628  fv3  5648  fvres  5649  nfunsn  5665  funimass4  5680  ssimaexg  5692  dffv2  5699  dmfco  5700  fvopab6  5728  fndmdif  5736  iinpreima  5762  fvelrn  5768  dff3  5784  dffo4  5787  exfo  5789  f1ompt  5793  fmptco  5802  fsng  5808  dfmpt  5812  fnressn  5818  fressnfv  5820  fvsng  5827  fnpr  5850  fnprOLD  5851  zfrep6  5868  funfvima3  5875  idref  5879  fvclss  5880  fvresex  5882  abrexco  5886  opabex3d  5889  opabex3  5890  imaiun  5892  dff13  5904  foeqcnvco  5927  f1eqcocnv  5928  fliftcnv  5933  isocnv2  5951  isomin  5957  isoini  5958  isofr  5962  isose  5963  f1oweALT  5974  wemoiso  5978  wemoiso2  5979  knatar  5980  oprabid  6005  csbovg  6012  0neqopab  6019  eloprabga  6060  mpt2v  6063  caovmo  6184  f1opw  6199  ofmres  6243  op1stg  6259  op2ndg  6260  1stval2  6264  2ndval2  6265  fo1st  6266  fo2nd  6267  f1stres  6268  f2ndres  6269  fo1stres  6270  fo2ndres  6271  1st2val  6272  2nd2val  6273  xp1st  6276  xp2nd  6277  sbcopeq1a  6299  csbopeq1a  6300  eloprabi  6313  mpt2mptsx  6314  dmmpt2ssx  6316  fmpt2x  6317  ovmptss  6328  fmpt2co  6330  df1st2  6333  df2nd2  6334  1stconst  6335  2ndconst  6336  curry1  6338  curry2  6341  fparlem1  6346  fparlem2  6347  fpar  6350  fsplit  6351  frxp  6353  xporderlem  6354  soxp  6356  fnwelem  6358  fnse  6360  reldmtpos  6384  dmtpos  6388  rntpos  6389  ovtpos  6391  dftpos3  6394  dftpos4  6395  tpostpos  6396  porpss  6423  sorpss  6424  sorpsscmpl  6430  opiota  6432  opabiotafun  6433  opabiota  6435  riotav  6451  csbriotag  6459  onovuni  6501  smogt  6526  tfrlem3  6535  tfrlem8  6542  tfrlem9a  6544  tfrlem16  6551  tz7.44lem1  6560  rdg0g  6582  rdglim2  6587  tz7.48-1  6597  seqomlem1  6604  seqomlem2  6605  abianfplem  6612  oacl  6676  omcl  6677  oecl  6678  oa0r  6679  om0r  6680  om1r  6683  oe1m  6685  oaordi  6686  oawordri  6690  oawordeulem  6694  oalimcl  6700  oaass  6701  oarec  6702  omordi  6706  omwordri  6712  omlimcl  6718  odi  6719  omass  6720  omeulem1  6722  oen0  6726  oeordi  6727  oewordri  6732  oeworde  6733  oeoalem  6736  oeoelem  6738  nnawordex  6777  omabs  6787  omsmolem  6793  ercnv  6823  iserd  6828  eqerlem  6834  eqer  6835  ecdmn0  6844  erth  6846  erdisj  6849  qsss  6862  ecid  6866  qsid  6867  iiner  6873  qsel  6880  erovlem  6897  ecopovsym  6903  ecopovtrn  6904  ecopover  6905  mapprc  6919  fnmap  6922  fnpm  6923  mapval2  6940  pmsspw  6945  mapsn  6952  mapsncnv  6957  ixpconstg  6968  ixpprc  6980  uniixp  6982  ixpin  6984  ixpiin  6985  resixpfo  6997  elixpsn  6998  ixpsnf1o  6999  boxriin  7001  boxcutc  7002  bren  7014  brdomg  7015  domen  7018  domeng  7019  idssen  7049  ener  7051  domtr  7057  ensn1g  7069  en1  7071  en1b  7072  fundmen  7077  fundmeng  7078  mapsnen  7081  unen  7086  domdifsn  7088  xpsnen  7089  xpsneng  7090  xpcomeng  7097  xpassen  7099  xpdom2  7100  xpdom2g  7101  domunsncan  7105  omxpenlem  7106  pw2f1o  7110  fopwdom  7113  sbthlem10  7123  sbth  7124  sbthcl  7126  domunsn  7154  fodomr  7155  pwdom  7156  canth2  7157  canth2g  7158  domssex  7165  xpf1o  7166  mapen  7168  mapunen  7173  map2xp  7174  mapdom2  7175  mapdom3  7176  ssenen  7178  infensuc  7182  nneneq  7187  php  7188  php2  7189  php3  7190  sucdom2  7200  1sdom  7208  unxpdomlem2  7211  unxpdomlem3  7212  isinf  7219  fineqvlem  7220  fineqv  7221  pssnn  7224  ssfi  7226  dif1enOLD  7237  dif1en  7238  findcard  7244  findcard2  7245  findcard2s  7246  ac6sfi  7248  frfi  7249  fimax2g  7250  unbnn2  7261  isfinite2  7262  xpfi  7275  domunfican  7276  fiint  7280  fodomfi  7282  fodomfib  7283  iunfi  7291  pwfilem  7297  ixpfi2  7301  fissuni  7307  fipreima  7308  finsschain  7309  fival  7313  ssfii  7319  fi0  7320  fiin  7322  dffi2  7323  fipwuni  7326  fisn  7327  elfiun  7330  dffi3  7331  fifo  7332  marypha1lem  7333  dfsup2  7342  dfsup2OLD  7343  ordiso2  7377  oismo  7402  hartogslem1  7404  hartogs  7406  wofib  7407  wemappo  7411  wemapso2lem  7412  card2on  7415  brwdom  7428  brwdomn0  7430  brwdom2  7434  wdomtr  7436  wdompwdom  7439  canthwdom  7440  xpwdomg  7446  unxpwdom2  7449  ixpiunwdom  7452  elirrv  7458  zfregfr  7463  inf0  7469  inf3lema  7472  inf3lemd  7475  inf3lem1  7476  inf3lem2  7477  inf3lem3  7478  inf3lem5  7480  inf3lem6  7481  inf3lem7  7482  inf3  7483  infeq5  7485  omex  7491  dfom3  7495  dfom5  7498  infdifsn  7504  cantnfdm  7512  cantnfval  7516  cantnfval2  7517  cantnflt  7520  cantnff  7522  oemapso  7531  cantnflem1  7538  wemapwe  7547  cnfcom  7550  cnfcom3clem  7555  epfrs  7560  tcvalg  7570  tctr  7572  tcmin  7573  r1sdom  7593  r1val1  7605  tz9.12lem1  7606  tz9.12lem3  7608  tz9.13  7610  tz9.13g  7611  rankf  7613  unir1  7632  rankvalg  7636  rankonidlem  7647  r1val2  7656  bndrank  7660  ranklim  7663  r1pwOLD  7665  rankunb  7669  rankuni2b  7672  rankuni  7682  rankval4  7686  rankxplim  7696  rankxplim3  7698  rankxpsuc  7699  tcrank  7701  cp  7708  bnd2  7710  kardex  7711  karden  7712  cardf2  7723  tskwe  7730  cardlim  7752  harcard  7758  cardiun  7762  pm54.43  7780  r0weon  7787  infxpenlem  7788  infxpenc2lem2  7794  fseqenlem1  7798  fseqenlem2  7799  fseqen  7801  dfac8alem  7803  dfac8clem  7806  ac10ct  7808  ween  7809  acnlem  7822  finacn  7824  acndom  7825  acndom2  7828  wdomfil  7835  infpwfien  7836  alephon  7843  alephcard  7844  alephordi  7848  cardaleph  7863  alephval3  7884  iunfictbso  7888  aceq3lem  7894  dfac3  7895  dfac4  7896  dfac5lem1  7897  dfac5lem2  7898  dfac5lem3  7899  dfac5lem4  7900  dfac5lem5  7901  dfac5  7902  dfac2a  7903  dfac2  7904  dfac8  7908  dfac9  7909  dfac10b  7912  acacni  7913  dfacacn  7914  dfac13  7915  kmlem1  7923  kmlem2  7924  kmlem9  7931  kmlem10  7932  kmlem11  7933  kmlem12  7934  kmlem13  7935  cdafn  7942  pwsdompw  7977  infmap2  7991  ackbij1lem5  7997  ackbij1lem8  8000  ackbij2lem3  8014  ackbij2  8016  cflm  8023  cardcf  8025  cfeq0  8029  cfsuc  8030  cff1  8031  cfflb  8032  cfval2  8033  cflim2  8036  cfss  8038  cfslb2n  8041  cofsmo  8042  cfsmolem  8043  cfcoflem  8045  coftr  8046  sornom  8050  infpssr  8081  fin4en1  8082  fin23lem11  8090  enfin2i  8094  fin23lem26  8098  fin23lem14  8106  fin23lem16  8108  fin23lem17  8111  fin23lem21  8112  fin23lem32  8117  fin23lem34  8119  fin23lem39  8123  compsscnvlem  8143  compssiso  8147  isf34lem4  8150  enfin1ai  8157  isfin1-3  8159  fin67  8168  dffin7-2  8171  fin1a2lem7  8179  fin1a2lem10  8182  fin1a2lem12  8184  fin1a2lem13  8185  fin12  8186  itunitc1  8193  itunitc  8194  ituniiun  8195  hsmexlem2  8200  hsmexlem4  8202  hsmex  8205  axcc2lem  8209  axcc3  8211  acncc  8213  fin41  8217  dominf  8218  dcomex  8220  axdc2lem  8221  axdc3lem  8223  axdc3lem2  8224  axdc3lem4  8226  axdc4lem  8228  axcclem  8230  ac9  8257  ac6s  8258  ac6sg  8262  ac9s  8267  numthcor  8268  zorn2lem1  8270  zorn2lem4  8273  zorn2lem7  8276  zorng  8278  zornn0g  8279  ttukeylem5  8287  ttukeylem6  8288  ttukeylem7  8289  axdclem  8293  axdclem2  8294  fodomg  8297  fodomb  8298  brdom3  8300  brdom5  8301  brdom4  8302  brdom7disj  8303  brdom6disj  8304  iunfo  8308  ondomon  8332  cardmin  8333  alephval2  8341  dominfac  8342  fpwwe2lem1  8400  fpwwe2lem8  8406  fpwwe2lem11  8409  fpwwe2lem12  8410  fpwwe2lem13  8411  fpwwe2  8412  fpwwe  8415  canthwe  8420  canthp1lem1  8421  pwfseqlem1  8427  pwfseqlem2  8428  pwfseqlem3  8429  pwfseqlem4a  8430  pwfseqlem5  8432  pwxpndom2  8434  gchac  8442  gch2  8448  inawinalem  8458  winainflem  8462  winalim2  8465  winafp  8466  gchina  8468  wunfi  8490  intwun  8504  wunex2  8507  uniwun  8509  eltsk2g  8520  inttsk  8543  inar1  8544  rankcf  8546  tskcard  8550  tskuni  8552  gruun  8575  intgru  8583  ingru  8584  wfgru  8585  grudomon  8586  gruina  8587  grur1a  8588  grur1  8589  grutsk  8591  axgroth5  8593  axgroth2  8594  grothpw  8595  grothpwex  8596  axgroth6  8597  grothomex  8598  grothac  8599  axgroth3  8600  grothprim  8603  grothtsk  8604  inaprc  8605  nqereu  8700  nqerf  8701  dmrecnq  8739  ltaddnq  8745  genpnnp  8776  genpnmax  8778  genpcl  8779  nqpr  8785  addclprlem1  8787  mulclprlem  8790  distrlem4pr  8797  1idpr  8800  prlem934  8804  ltaddpr  8805  ltexprlem3  8809  ltexprlem4  8810  ltexprlem6  8812  ltexprlem7  8813  prlem936  8818  reclem2pr  8819  reclem3pr  8820  mulasssr  8859  ltsosr  8863  0idsr  8866  1idsr  8867  ltasr  8869  recexsrlem  8872  mulgt0sr  8874  supsrlem  8880  ltresr  8909  axmulass  8926  axrrecex  8932  axpre-lttri  8934  wuncn  8939  renfdisj  9032  wloglei  9452  lbinfm  9854  supmul1  9866  supmullem1  9867  supmullem2  9868  supmul  9869  dfinfmr  9878  infmsup  9879  infmrgelb  9881  infmrlb  9882  dfnn2  9906  dflt2  10634  xrinfmss2  10782  infmxrgelb  10806  xrinfm0  10808  fzpr  10993  uzrdgfni  11185  axdc4uzlem  11208  axdc4uz  11209  seqval  11221  seqfeq4  11259  serle  11265  seqof  11267  hash1snb  11568  hash2prde  11575  hash2prb  11576  hashxplem  11583  hashmap  11585  hashpw  11586  hashfun  11587  hashbclem  11588  hashfacen  11590  hashf1lem1  11591  hashf1lem2  11592  hashf1  11593  fz1isolem  11597  brfi1uzind  11602  ccatfn  11628  wrdexb  11650  wrdind  11678  shftfval  11772  shftfib  11774  shftfn  11775  2shfti  11782  sqrlem6  11940  rexfiuz  12038  rlimdm  12232  fclim  12234  climshft  12257  fsum2dlem  12441  fsumcom2  12445  fsum0diag2  12453  fsumabs  12467  fsumrlim  12477  fsumo1  12478  fsumiun  12487  incexclem  12503  isumltss  12515  supcvg  12522  xpnnenOLD  12696  rpnnen2lem11  12711  algrf  12951  isprm2lem  12973  isprm2  12974  prmind2  12977  iserodd  13096  4sqlem12  13211  vdwmc  13233  vdwlem10  13245  vdwlem13  13248  ramtlecl  13255  hashbc0  13260  ramval  13263  ramcl2lem  13264  ramub2  13269  0ram  13275  ram0  13277  ramub1lem1  13281  ramub1lem2  13282  ramub1  13283  restfn  13539  elrest  13542  restsspw  13546  prdsval  13565  prdsle  13571  prdsless  13572  prdsleval  13586  pwsle  13601  imasaddfnlem  13640  imasvscafn  13649  imasleval  13653  xpsc0  13672  xpsc1  13673  xpsfrnel2  13677  ismre  13702  fnmre  13703  ismred  13714  mremre  13716  fnmrc  13719  mrcfval  13720  mrisval  13742  mreexexlem4d  13759  isacs2  13765  mreacs  13770  acsfn  13771  acsfn1  13773  acsfn2  13775  cidffn  13790  comfeq  13819  invsym2  13875  oppcsect2  13887  brssc  13901  sscpwex  13902  isssc  13907  issubc  13922  isfuncd  13949  cofucl  13972  funcres2b  13981  funcpropd  13984  setcmon  14129  catcval  14138  fnxpc  14160  xpcval  14161  xpccatid  14172  curf2ndf  14231  drsdirfi  14282  isdrs2  14283  clatl  14430  odupos  14449  oduposb  14450  oduglb  14453  odulub  14455  posglbd  14463  ipoval  14467  ipolerval  14469  fpwipodrs  14477  ipodrsima  14478  isacs5lem  14482  psdmrn  14526  psssdm2  14534  submacs  14652  pwsdiagmhm  14655  gsumwspan  14678  mulgpropd  14810  subgacs  14862  nsgacs  14863  eqgfval  14875  eqgval  14876  gicsubgen  14952  gaid  14963  gaorb  14971  orbsta  14977  symgval  14981  symgbas  14982  symgplusg  14986  sylow1lem2  15120  sylow2alem1  15138  sylow2alem2  15139  sylow2a  15140  sylow2blem1  15141  sylow2blem2  15142  sylow2blem3  15143  sylow3lem1  15148  sylow3lem3  15150  sylow3lem6  15153  efgval  15236  efgval2  15243  efgrelexlemb  15269  efgcpbllema  15273  efgcpbllemb  15274  vrgpfval  15285  frgpuplem  15291  divsabl  15367  frgpnabllem1  15371  gsumval3  15401  gsumzaddlem  15413  gsumzadd  15414  gsum2d  15433  gsum2d2  15435  gsumcom2  15436  gsumxp  15437  dprdfadd  15465  dprdres  15473  subgdmdprd  15479  dprd2dlem1  15486  dprd2d2  15489  ablfac1eulem  15517  pgpfac1lem5  15524  opprsubg  15628  subrgmre  15779  subsubrg2  15782  subrgpropd  15789  lss1d  15930  lssintcl  15931  lssmre  15933  lssacs  15934  pwsdiaglmhm  16024  islbs3  16118  lbsextlem4  16124  drngnidl  16191  lidldvgen  16217  psrbaglefi  16328  mplcoe1  16419  mplcoe2  16421  ltbval  16423  ltbwe  16424  opsrle  16427  opsrtoslem1  16435  opsrtoslem2  16436  evlslem4  16455  coe1mul2  16556  coe1tm  16559  znleval  16725  cssmre  16810  thlle  16814  pjfval2  16826  istopon  16880  tgval2  16911  bastg  16921  tgdom  16933  distop  16950  indistopon  16955  fctop  16958  cctop  16960  ppttop  16961  epttop  16963  fncld  16976  cldss2  16984  ntreq0  17031  discld  17043  mretopd  17046  toponmre  17047  neisspw  17061  opnnei  17074  tgrest  17107  resttopon  17109  restco  17112  restdis  17126  ordtbas2  17138  ordtcnv  17148  ordtrest2  17151  pnfnei  17167  mnfnei  17168  iscnp2  17186  subbascn  17201  cnntr  17221  cnrest2  17231  cnpresti  17233  cnprest  17234  cnprest2  17235  ist1-3  17294  hausnei2  17298  isnrm2  17303  dishaus  17327  cmpcovf  17335  fincmp  17337  cmpsublem  17343  cmpsub  17344  cmpcld  17346  uncmp  17347  fiuncmp  17348  hauscmplem  17350  cmpfi  17352  dfcon2  17362  consuba  17363  cnconn  17365  uncon  17372  t1conperf  17379  is1stc2  17385  1stcfb  17388  2ndcsb  17392  2ndc1stc  17394  1stcrest  17396  2ndcctbss  17398  2ndcdisj  17399  2ndcomap  17401  2ndcsep  17402  dis2ndc  17403  llyi  17417  nllyi  17418  nlly2i  17419  llynlly  17420  subislly  17424  restnlly  17425  restlly  17426  islly2  17427  llyrest  17428  llyidm  17431  nllyidm  17432  hausllycmp  17437  cldllycmp  17438  lly1stc  17439  dislly  17440  hausmapdom  17443  kgenf  17453  iskgen3  17461  llycmpkgen2  17462  1stckgenlem  17465  1stckgen  17466  kgencn2  17469  txuni2  17477  txbas  17479  eltx  17480  ptpjpre1  17483  ptuni2  17488  ptpjcn  17522  ptpjopn  17523  ptclsg  17526  dfac14  17529  xkoccn  17530  txcnp  17531  txcnmpt  17535  prdstopn  17539  txrest  17542  txdis  17543  txindis  17545  txdis1cn  17546  txlly  17547  txnlly  17548  pthaus  17549  txcmplem1  17552  txcmplem2  17553  hausdiag  17556  txlm  17559  tx1stc  17561  tx2ndc  17562  txkgen  17563  xkopt  17566  xkococnlem  17570  xkococn  17571  cnmpt1st  17579  cnmpt2nd  17580  xkofvcn  17595  xkoinjcn  17598  txcon  17600  qtoptop2  17607  qtopuni  17610  basqtop  17619  tgqtop  17620  hmphdis  17704  indishmph  17706  txhmeo  17711  pt1hmeo  17714  ptuncnv  17715  ptunhmeo  17716  xpstopnlem1  17717  ptcmpfi  17721  xkohmeo  17723  isfbas  17737  isfbas2  17743  fbssfi  17745  trfbas2  17751  isfild  17766  snfil  17772  elfg  17779  fgcl  17786  filcon  17791  fbasrn  17792  filuni  17793  trfil2  17795  cfinfil  17801  csdfil  17802  supfil  17803  zfbas  17804  isufil2  17816  filssufilg  17819  acufl  17825  filufint  17828  uffix  17829  ufinffr  17837  ufildr  17839  fin1aufil  17840  rnelfmlem  17860  rnelfm  17861  fmfnfmlem3  17864  fmfnfmlem4  17865  fmfnfm  17866  ufldom  17870  flimrest  17891  hauspwpwf1  17895  txflf  17914  fclsrest  17932  fclscmp  17938  alexsubb  17953  alexsubALTlem1  17954  alexsubALTlem2  17955  alexsubALTlem3  17956  alexsubALTlem4  17957  alexsubALT  17958  ptcmplem2  17960  ptcmplem3  17961  ptcmplem4  17962  ptcmplem5  17963  tmdgsum  17991  symgtgp  17997  cldsubg  18006  tgpconcomp  18008  divstgplem  18016  divstgphaus  18018  prdstmdd  18019  tsmsval2  18025  tsmssubm  18038  imasdsf1olem  18150  xpsdsval  18158  xmetec  18193  prdsbl  18250  stdbdxmet  18274  met1stc  18280  prdsxmslem2  18288  dscopn  18309  xrtgioo  18525  xrsblre  18530  icccmplem1  18541  icccmplem2  18542  fsumcn  18588  fsum2cn  18589  cnllycmp  18669  isphtpc  18707  pi1blem  18752  iscmet3  18934  metcld2  18947  bcthlem4  18964  minveclem3b  19007  ovolfiniun  19075  ovoliunlem1  19076  ovoliunlem2  19077  finiunmbl  19116  volfiniun  19119  iundisj2  19121  uniioombllem3  19155  vitalilem2  19179  vitalilem3  19180  vitali  19183  mbfimaopnlem  19225  itg1addlem4  19269  mbfi1fseqlem4  19288  mbfi1fseqlem6  19290  itgfsum  19396  ellimc2  19442  limcflf  19446  perfdvf  19468  dvres  19476  dvres2  19477  dvnff  19487  dvcj  19514  dvrec  19519  dvmptfsum  19537  dvef  19542  rolle  19552  dvivthlem1  19570  dvfsumle  19583  dvfsumabs  19585  dvfsumlem2  19589  dvfsumlem3  19590  ftc1cn  19605  mpfind  19643  pf1ind  19653  vieta1lem2  19906  elqaalem2  19915  ulmdv  19997  logfac  20173  xrlimcnp  20485  jensenlem1  20503  jensenlem2  20504  jensen  20505  wilthlem2  20530  prmorcht  20639  lgsquadlem1  20816  lgsquadlem2  20817  dchrisumlema  20860  dchrisumlem3  20863  umgraex  21036  isusgra0  21054  usgra2edg  21079  usgrarnedg  21081  usgraedg4  21083  usgraedgreu  21084  usgrafis  21099  ex-natded9.26  21117  nvss  21462  vsfval  21504  h2hlm  21873  axhcompl-zf  21891  hlim2  22084  hhcmpl  22092  hhcms  22095  shex  22104  isch2  22116  helch  22136  hhsscms  22169  occl  22196  chintcli  22223  dfch2  22299  spanuni  22436  spansni  22449  elnlfn  22821  nmopun  22907  nlelchi  22954  cnlnssadj  22973  adjbd1o  22978  branmfn  22998  pjnmopi  23041  hmopidmchi  23044  abrexss  23388  iuninc  23409  disjabrex  23422  disjabrexf  23423  disjpreima  23424  iundisj2f  23427  inimasn  23434  suppss2f  23452  fmptdF  23471  fmptcof2  23479  funcnvmptOLD  23484  funcnvmpt  23485  disjdsct  23493  1stpreima  23498  2ndpreima  23499  ctex  23503  iundisj2fi  23556  ishashinf  23562  tpr2rico  23665  cnextf  23702  cnextcn  23703  ustfn  23706  ustfilxp  23717  ustn0  23723  restutopopn  23741  ustuqtop0  23743  ustuqtop1  23744  ustuqtop2  23745  ustuqtop3  23746  ustuqtop4  23747  ustuqtop5  23748  utopsnneiplem  23750  ucnimalem  23774  ucnima  23775  fmucndlem  23784  metustid  23797  metustsym  23798  metustexhalf  23799  metustfbas  23800  blval2  23807  metustbl  23809  restmetu  23814  esumel  23907  esum0  23909  esumc  23911  gsumesum  23916  esumcst  23920  esumfsup  23925  esumpfinvalf  23931  hasheuni  23940  sigaex  23957  sigaval  23958  isrnsigaOLD  23960  pwsiga  23978  sigainb  23984  insiga  23985  dmsigagen  23992  measbase  24016  ismeas  24018  isrnmeas  24019  measiuns  24034  measdivcstOLD  24041  measdivcst  24042  cntmeas  24043  mbfmco2  24078  mbfmcnt  24081  br2base  24082  dya2iocrfn  24092  dya2iocct  24093  dya2iocnrect  24094  dya2iocucvr  24097  sxbrsigalem2  24099  sxbrsiga  24103  coinfliplem  24184  ballotlem2  24194  ballotlemsf1o  24219  ballotlemirc  24237  derangenlem  24305  subfacp1lem1  24313  subfacp1lem3  24316  subfacp1lem4  24317  subfacp1lem5  24318  erdszelem7  24331  erdszelem8  24332  erdsze2lem2  24338  kur14lem9  24348  ptpcon  24367  indispcon  24368  conpcon  24369  cnllyscon  24379  rellyscon  24385  cvmsss2  24408  cvmcov2  24409  cvmliftlem15  24432  cvmlift2lem1  24436  cvmlift2lem12  24448  eupath  24492  ghomgrplem  24583  relexpindlem  24623  rtrclreclem.trans  24630  dfrtrcl2  24632  untsucf  24643  dfid4  24667  shftvalg  24692  ntrivcvg  24709  fprodfac  24780  dftr6  24848  coepr  24850  dffr5  24851  dfso2  24852  dfpo2  24853  br8  24854  br6  24855  br4  24856  dfres3  24857  cnvco1  24858  cnvco2  24859  eldm3  24860  fundmpss  24863  fprb  24870  dfdm5  24873  dfrn5  24874  setinds  24875  dfon2lem1  24880  dfon2lem3  24882  dfon2lem6  24885  dfon2lem7  24886  dfon2lem8  24887  dfon2  24889  rdgprc  24892  dfrdg2  24893  predreseq  24920  predpo  24925  predbrg  24927  setlikespec  24928  predep  24933  preddowncl  24937  preduz  24941  predfz  24944  tz6.26  24946  trpredrec  24982  poseq  24994  soseq  24995  wfrlem5  25001  wfrlem10  25006  wfrlem12  25008  wfrlem13  25009  wfrlem14  25010  wfrlem16  25012  tfrALTlem  25017  frrlem5  25026  frrlem11  25034  sltsolem1  25063  nofulllem5  25101  txpss3v  25159  brtxp  25161  brtxp2  25162  pprodss4v  25165  brpprod  25166  brpprod3a  25167  brpprod3b  25168  brsset  25170  idsset  25171  dfon3  25173  brtxpsd  25175  brbigcup  25179  dfbigcup2  25180  fobigcup  25181  elfix  25184  elfix2  25185  dffix2  25186  fixcnv  25189  limitssson  25192  dfom5b  25193  dffun10  25194  elfuns  25195  elfunsg  25196  elsingles  25198  fnsingle  25199  fvsingle  25200  dfiota3  25203  brimage  25206  brimageg  25207  funimage  25208  fnimage  25209  imageval  25210  brcart  25212  brdomaing  25215  brrangeg  25216  brimg  25217  brapply  25218  brcup  25219  brcap  25220  brsuccf  25221  funpartlem  25222  funpartfun  25223  funpartfv  25225  fullfunfv  25227  brrestrict  25229  dfrdg4  25230  tfrqfree  25231  altopelaltxp  25252  altxpsspw  25253  brsegle  25473  fvline  25509  liness  25510  ellines  25517  bpoly2  25534  bpoly3  25535  rankung  25538  ranksng  25539  rankelg  25540  rankpwg  25541  rankeq1o  25543  elhf2g  25548  hfext  25555  onsucconi  25618  supaddc  25665  supadd  25666  itg2addnclem  25675  itg2addnc  25677  ftc1cnnc  25697  areacirclem6  25705  cnvresimaOLD  25733  trer  25734  finminlem  25738  gtinf  25741  fneer  25795  fnessref  25800  refssfne  25801  islocfin  25803  comppfsc  25814  neibastop1  25815  neibastop2lem  25816  neibastop3  25818  topmeet  25820  topjoin  25821  neifg  25827  tailfb  25833  filnetlem2  25835  filnetlem3  25836  filnetlem4  25837  cover2g  25866  f1opr  25898  inixp  25906  indexdom  25920  frinfm  25923  sdclem2  25959  sdclem1  25960  fdc  25962  isbndx  26012  prdstotbnd  26024  heibor1lem  26039  heiborlem1  26041  heiborlem3  26043  heiborlem4  26044  heiborlem5  26045  heiborlem6  26046  heiborlem8  26048  heiborlem10  26050  ismrer1  26068  riscer  26125  divrngidl  26159  intidl  26160  isfldidl  26199  ispridlc  26201  prtlem10  26239  prtlem13  26242  prtlem16  26243  prtlem19  26252  prter2  26255  prter3  26256  ralxpmap  26267  elrfi  26275  ismrcd1  26279  ismrcd2  26280  istopclsd  26281  ismrc  26282  mrefg2  26288  isnacs3  26291  mzpclall  26311  mzpincl  26318  mzpsubst  26332  mzpcompact2lem  26335  mzpcompact2  26336  eldioph2lem1  26345  eldioph2lem2  26346  eldiophss  26360  diophrex  26361  rexrabdioph  26381  2rexfrabdioph  26383  3rexfrabdioph  26384  4rexfrabdioph  26385  6rexfrabdioph  26386  7rexfrabdioph  26387  rabren3dioph  26404  fphpd  26405  rencldnfilem  26409  pellexlem5  26424  pellex  26426  rmxypairf1o  26502  monotuz  26532  monotoddzzfi  26533  oddcomabszz  26535  2nn0ind  26536  zindbi  26537  mzpcong  26565  rmydioph  26613  rmxdioph  26615  expdiophlem2  26621  setindtr  26623  setindtrs  26624  dford3lem2  26626  ttac  26635  pw2f1ocnv  26636  wepwsolem  26644  inisegn0  26646  dnnumch1  26647  fnwe2val  26652  fnwe2lem2  26654  aomclem1  26657  aomclem2  26658  aomclem6  26662  dfac11  26666  kelac2lem  26668  dfac21  26670  islssfg2  26675  lmhmlnmsplit  26691  pwssplit3  26696  filnm  26698  pwslnmlem1  26700  pwslnm  26702  dsmmval  26706  frlmlbs  26755  unxpwdom3  26762  enfixsn  26763  dfacbasgrp  26779  islindf4  26814  lmisfree  26818  lnr2i  26826  lnrfg  26829  hbtlem6  26839  rngunsnply  26884  pmtrfval  26899  symggen  26917  gsumcom3  26960  acsfn1p  27013  sdrgacs  27015  idomsubgmo  27020  fgraphxp  27036  expgrowth  27058  2sbc6g  27121  iotain  27123  compel  27146  ipo0  27158  ifr0  27159  fnchoice  27206  infrglb  27228  stoweidlem31  27286  stoweidlem57  27312  stoweidlem62  27317  stirlinglem13  27341  funressnfv  27499  dfdfat2  27502  csbafv12g  27508  tz6.12-afv  27544  rlimdmafv  27548  csbaovg  27551  usgraexmpl  27585  nbgraf1olem5  27611  nb3graprlem1  27616  cusgrarn  27624  cusgrares  27637  cusgrasize  27643  cusgrafilem1  27644  cusgrafilem2  27645  isuvtx  27653  uvtx01vtx  27657  trls  27690  wlkntrllem3  27705  wlkntrllem4  27706  constr1trl  27726  2trllem1  27732  constr2trl  27736  2pthon  27740  dfconngra1  27797  frisusgranb  27832  frgra3vlem1  27835  frgra3vlem2  27836  3vfriswmgralem  27839  2pthfrgra  27846  frgrancvvdeqlem3  27867  frgrancvvdeqlem4  27868  frgrawopreg1  27885  frgrawopreg2  27886  onfrALTlem5  28054  onfrALTlem4  28055  onfrALTlem3  28056  opelopab4  28064  a9e2nd  28071  trsspwALT  28356  trsspwALT2  28357  trsspwALT3  28358  pwtrVD  28362  pwtrOLD  28363  unipwrVD  28372  unipwr  28373  onfrALTlem5VD  28425  onfrALTlem4VD  28426  onfrALTlem3VD  28427  relopabVD  28441  a9e2ndVD  28448  sspwimp  28458  sspwimpVD  28459  sspwimpcf  28460  sspwimpcfVD  28461  sspwimpALT  28465  sspwimpALT2  28469  a9e2ndALT  28471  bnj23  28508  bnj62  28510  bnj156  28520  bnj219  28525  bnj610  28540  bnj918  28560  bnj927  28564  bnj976  28573  bnj1098  28579  bnj1379  28627  bnj110  28654  bnj98  28663  bnj154  28674  bnj155  28675  bnj535  28686  bnj556  28696  bnj557  28697  bnj581  28704  bnj591  28707  bnj594  28708  bnj580  28709  bnj607  28712  bnj609  28713  bnj600  28715  bnj849  28721  bnj893  28724  bnj908  28727  bnj934  28731  bnj944  28734  bnj964  28739  bnj966  28740  bnj969  28742  bnj970  28743  bnj910  28744  bnj986  28750  bnj999  28753  bnj1018  28758  bnj907  28761  bnj1039  28765  bnj1040  28766  bnj1052  28769  bnj1123  28780  bnj1030  28781  bnj1133  28783  bnj1128  28784  bnj1145  28787  bnj1204  28806  bnj1373  28824  bnj1417  28835  bnj1421  28836  bnj1498  28855  eqlkr2  29361  glbconxN  29638  pmapglbx  30029  pmapglb  30030  pclclN  30151  pclfinN  30160  polval2N  30166  pclfinclN  30210  osumcllem10N  30225  pexmidlem7N  30236  cdleme31sdnN  30647  cdlemefr44  30685  cdleme48fv  30759  cdleme46fvaw  30761  cdleme48bw  30762  cdleme46fsvlpq  30765  cdlemeg46fvcl  30766  cdlemeg49le  30771  cdlemeg46fjgN  30781  cdlemeg46fjv  30783  cdleme48d  30795  cdlemeg49lebilem  30799  cdleme50eq  30801  cdleme50f  30802  cdlemg2jlemOLDN  30853  cdlemg2klem  30855  cdlemk40  31177  cdlemk56  31231  diaglbN  31316  dvhlveclem  31369  dib1dim  31426  dibglbN  31427  diblss  31431  diblsmopel  31432  dicelvalN  31439  diclspsn  31455  cdlemn7  31464  dihordlem7  31475  dihopelvalcpre  31509  xihopellsmN  31515  dihopellsm  31516  dih1  31547  dihmeetlem1N  31551  dihglblem5apreN  31552  dihmeetlem2N  31560  dihglbcpreN  31561  dihmeetlem4preN  31567  dihmeetlem13N  31580  dih1dimatlem  31590  dihatlat  31595  dihjatcclem4  31682  lcdlss  31880
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-v 2875
  Copyright terms: Public domain W3C validator