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

Theorem vex 2730
Description: All set variables are sets (see isset 2731). 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 2253 . 2  |-  x  =  x
2 df-v 2729 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2356 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 202 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2727
This theorem is referenced by:  isset  2731  ralv  2740  rexv  2741  reuv  2742  rabab  2743  sbhypf  2771  ceqex  2835  ralab  2863  rexab  2865  moeq3  2879  mo2icl  2881  reu8  2900  sbc2or  2929  csbvarg  3036  csbiebg  3048  sbcnestgf  3056  sbnfc2  3069  ddif  3222  csbing  3283  dfun2  3311  dfin2  3312  vn0  3369  eqv  3377  abvor0  3379  sbss  3469  csbifg  3498  ifexg  3529  elpwg  3537  dftp2  3583  prnzg  3650  snssg  3656  difprsn  3658  sneqrg  3682  preq12bg  3691  pwpr  3723  pwtp  3724  pwv  3726  unipr  3741  uniprg  3742  unisng  3744  elintg  3768  elintrabg  3773  intss1  3775  ssint  3776  intmin  3780  intss  3781  intssuni  3782  intmin4  3789  intab  3790  intun  3792  intpr  3793  intprg  3794  uniintsn  3797  iinconst  3812  iuniin  3813  iinss1  3815  dfiin2g  3834  ssiinf  3849  iinss  3851  iinss2  3852  0iin  3858  iinab  3861  iinun2  3866  iundif2  3867  iindif2  3869  iinin2  3870  iinuni  3883  sspwuni  3885  iinpw  3888  iunpwss  3889  brab1  3965  csbopabg  3991  mptv  4009  trint  4025  trintss  4026  vprc  4049  inex1g  4054  ssexg  4057  intex  4065  inuni  4071  axpweq  4081  pwexg  4088  pwuni  4100  axpr  4107  zfpair2  4109  elALT  4112  rext  4116  sspwb  4117  unipw  4118  ssextss  4121  nnullss  4128  exss  4129  opth  4138  opthg  4139  copsexg  4145  copsex4g  4148  moop2  4154  euotd  4160  opelopabsbOLD  4166  opelopabsb  4168  pwin  4190  pwunss  4191  pwssun  4192  pwundifOLD  4194  epelg  4199  epel  4201  dfid3  4203  pofun  4223  epse  4269  wefrc  4280  tron  4308  onfr  4324  sucel  4358  suctr  4368  uniexg  4408  unexb  4411  snnex  4415  uniuni  4418  eusvnf  4420  eusvnfb  4421  reusv6OLD  4436  iunpw  4461  onint  4477  ordpwsuc  4497  unon  4513  ordunisuc  4514  onuninsuci  4522  orduninsuc  4525  limsssuc  4532  limuni3  4534  tfinds  4541  tfindsg  4542  tfindsg2  4543  tfinds2  4545  dfom2  4549  peano5  4570  finds  4573  findsg  4574  finds2  4575  0nelxp  4624  opelxp  4626  opeliunxp  4647  elvv  4655  elvvv  4656  elvvuni  4657  xpsspw  4704  xpsspwOLD  4705  relopabi  4718  opabid2  4722  difopab  4724  xpiindi  4728  ralxpf  4737  relop  4741  cnvco  4772  dfrn2  4775  dfdm4  4779  dmss  4785  dmin  4793  dmiun  4794  dmuni  4795  dm0  4799  dmi  4800  reldm0  4803  elreldm  4810  elrnmpt1  4835  dmrnssfld  4845  dmcoss  4851  dmcosseq  4853  opelresg  4869  resieq  4872  dmres  4883  elres  4897  relssres  4899  resopab  4903  resiexg  4904  iss  4905  dfres2  4909  dfima2  4921  csbima12g  4929  imadmrn  4931  imai  4934  elimasng  4946  args  4948  epini  4950  iniseg  4951  dffr3  4952  dfse2  4953  exse2  4954  cotr  4962  issref  4963  cnvsym  4964  intasym  4965  asymref  4966  asymref2  4967  intirr  4968  brcodir  4969  codir  4970  qfto  4971  poirr2  4974  cnvopab  4990  cnv0  4991  cnvi  4992  cnvdif  4994  rniun  4998  dminss  5002  imainss  5003  ssrnres  5023  rninxp  5024  dminxp  5025  cnvcnv3  5030  dfrel2  5031  dmsnn0  5044  dmsnopg  5050  cnvcnvsn  5056  dmsnsnsn  5057  cnvsng  5064  elxp4  5066  elxp5  5067  cnvresima  5068  dfco2  5078  dfco2a  5079  cores  5082  resco  5083  imaco  5084  rnco  5085  coiun  5088  co02  5092  coi1  5094  coass  5097  relssdmrn  5099  unielrel  5103  unixp0  5112  ressn  5117  cnviin  5118  cnvpo  5119  cnvso  5120  dffun2  5123  dffun7  5138  dffun8  5139  dffun9  5140  funopg  5144  funssres  5151  funun  5153  funcnvsn  5154  funcnv2  5166  funcnv  5167  funcnv3  5168  fun2cnv  5169  funcnvuni  5174  imadif  5184  isarep1  5188  2elresin  5212  fnres  5217  fcnvres  5275  fabexg  5279  fconstg  5285  fun11iun  5350  f1osng  5371  fv2  5373  fvprc  5374  fvex  5391  fv3  5393  nfunsn  5410  funimass4  5425  ssimaexg  5437  dffv2  5444  dmfco  5445  fvopab6  5473  fndmdif  5481  iinpreima  5507  fvelrn  5513  dff3  5525  dffo4  5528  exfo  5530  f1ompt  5534  fmptco  5543  fsng  5549  dfmpt  5553  fnressn  5557  fressnfv  5559  fvsng  5566  zfrep6  5600  funfvima3  5607  idref  5611  fvclss  5612  fvresex  5614  abrexco  5618  opabex3  5621  imaiun  5623  dff13  5635  foeqcnvco  5656  f1eqcocnv  5657  fliftcnv  5662  isocnv2  5680  isomin  5686  isoini  5687  isofr  5691  isose  5692  f1oweALT  5703  wemoiso  5707  wemoiso2  5708  knatar  5709  oprabid  5734  csbovg  5741  eloprabga  5786  mpt2v  5789  caovmo  5909  f1opw  5924  ofmres  5968  op1stg  5984  op2ndg  5985  1stval2  5989  2ndval2  5990  fo1st  5991  fo2nd  5992  f1stres  5993  f2ndres  5994  fo1stres  5995  fo2ndres  5996  1st2val  5997  2nd2val  5998  xp1st  6001  xp2nd  6002  sbcopeq1a  6024  csbopeq1a  6025  eloprabi  6038  mpt2mptsx  6039  dmmpt2ssx  6041  fmpt2x  6042  ovmptss  6052  fmpt2co  6054  df1st2  6057  df2nd2  6058  1stconst  6059  2ndconst  6060  curry1  6062  curry2  6065  fparlem1  6070  fparlem2  6071  fpar  6074  fsplit  6075  frxp  6077  xporderlem  6078  soxp  6080  fnwelem  6082  fnse  6084  reldmtpos  6094  dmtpos  6098  rntpos  6099  ovtpos  6101  dftpos3  6104  dftpos4  6105  tpostpos  6106  porpss  6133  sorpss  6134  sorpsscmpl  6140  uniabio  6153  iotaval  6154  sniota  6170  opiota  6174  opabiotafun  6175  opabiota  6177  riotav  6195  csbriotag  6203  onovuni  6245  smogt  6270  tfrlem3  6279  tfrlem8  6286  tfrlem9a  6288  tfrlem16  6295  tz7.44lem1  6304  rdg0g  6326  rdglim2  6331  tz7.48-1  6341  seqomlem1  6348  seqomlem2  6349  abianfplem  6356  oacl  6420  omcl  6421  oecl  6422  oa0r  6423  om0r  6424  om1r  6427  oe1m  6429  oaordi  6430  oawordri  6434  oawordeulem  6438  oalimcl  6444  oaass  6445  oarec  6446  omordi  6450  omwordri  6456  omlimcl  6462  odi  6463  omass  6464  omeulem1  6466  oen0  6470  oeordi  6471  oewordri  6476  oeworde  6477  oeoalem  6480  oeoelem  6482  nnawordex  6521  omabs  6531  omsmolem  6537  ercnv  6567  iserd  6572  eqerlem  6578  eqer  6579  ecdmn0  6588  erth  6590  erdisj  6593  qsss  6606  ecid  6610  qsid  6611  iiner  6617  qsel  6624  erovlem  6640  ecopovsym  6646  ecopovtrn  6647  ecopover  6648  mapprc  6662  fnmap  6665  fnpm  6666  mapval2  6683  pmsspw  6688  mapsn  6695  mapsncnv  6700  ixpconstg  6711  ixpprc  6723  uniixp  6725  ixpin  6727  ixpiin  6728  resixpfo  6740  elixpsn  6741  ixpsnf1o  6742  boxriin  6744  boxcutc  6745  bren  6757  brdomg  6758  domen  6761  domeng  6762  idssen  6792  ener  6794  domtr  6799  ensn1g  6811  en1  6813  en1b  6814  fundmen  6819  fundmeng  6820  mapsnen  6823  unen  6828  domdifsn  6830  xpsnen  6831  xpsneng  6832  xpcomeng  6839  xpassen  6841  xpdom2  6842  xpdom2g  6843  domunsncan  6847  omxpenlem  6848  pw2f1o  6852  fopwdom  6855  sbthlem10  6865  sbth  6866  sbthcl  6868  domunsn  6896  fodomr  6897  pwdom  6898  canth2  6899  canth2g  6900  domssex  6907  xpf1o  6908  mapen  6910  mapunen  6915  map2xp  6916  mapdom2  6917  mapdom3  6918  ssenen  6920  infensuc  6924  nneneq  6929  php  6930  php2  6931  php3  6932  sucdom2  6942  1sdom  6950  unxpdomlem2  6953  unxpdomlem3  6954  isinf  6961  fineqvlem  6962  fineqv  6963  pssnn  6966  ssfi  6968  dif1enOLD  6975  dif1en  6976  findcard  6982  findcard2  6983  findcard2s  6984  ac6sfi  6986  frfi  6987  fimax2g  6988  unbnn2  6999  isfinite2  7000  xpfi  7013  domunfican  7014  fiint  7018  fodomfi  7020  fodomfib  7021  iunfi  7029  pwfilem  7034  ixpfi2  7038  fissuni  7044  fipreima  7045  finsschain  7046  fival  7050  ssfii  7056  fi0  7057  fiin  7059  dffi2  7060  fipwuni  7063  fisn  7064  elfiun  7067  dffi3  7068  fifo  7069  marypha1lem  7070  dfsup2  7079  dfsup2OLD  7080  ordiso2  7114  oismo  7139  hartogslem1  7141  hartogs  7143  wofib  7144  wemappo  7148  wemapso2lem  7149  card2on  7152  brwdom  7165  brwdomn0  7167  brwdom2  7171  wdomtr  7173  wdompwdom  7176  canthwdom  7177  xpwdomg  7183  unxpwdom2  7186  ixpiunwdom  7189  elirrv  7195  zfregfr  7200  inf0  7206  inf3lema  7209  inf3lemd  7212  inf3lem1  7213  inf3lem2  7214  inf3lem3  7215  inf3lem5  7217  inf3lem6  7218  inf3lem7  7219  inf3  7220  infeq5  7222  omex  7228  dfom3  7232  dfom5  7235  infdifsn  7241  cantnfdm  7249  cantnfval  7253  cantnfval2  7254  cantnflt  7257  cantnff  7259  oemapso  7268  cantnflem1  7275  wemapwe  7284  cnfcom  7287  cnfcom3clem  7292  epfrs  7297  tcvalg  7307  tctr  7309  tcmin  7310  r1sdom  7330  r1val1  7342  tz9.12lem1  7343  tz9.12lem3  7345  tz9.13  7347  tz9.13g  7348  rankf  7350  unir1  7369  rankvalg  7373  rankonidlem  7384  r1val2  7393  bndrank  7397  ranklim  7400  r1pwOLD  7402  rankunb  7406  rankuni2b  7409  rankuni  7419  rankval4  7423  rankxplim  7433  rankxplim3  7435  rankxpsuc  7436  tcrank  7438  cp  7445  bnd2  7447  kardex  7448  karden  7449  cardf2  7460  tskwe  7467  cardlim  7489  harcard  7495  cardiun  7499  pm54.43  7517  r0weon  7524  infxpenlem  7525  infxpenc2lem2  7531  fseqenlem1  7535  fseqenlem2  7536  fseqen  7538  dfac8alem  7540  dfac8clem  7543  ac10ct  7545  ween  7546  acnlem  7559  finacn  7561  acndom  7562  acndom2  7565  wdomfil  7572  infpwfien  7573  alephon  7580  alephcard  7581  alephordi  7585  cardaleph  7600  alephval3  7621  iunfictbso  7625  aceq3lem  7631  dfac3  7632  dfac4  7633  dfac5lem1  7634  dfac5lem2  7635  dfac5lem3  7636  dfac5lem4  7637  dfac5lem5  7638  dfac5  7639  dfac2a  7640  dfac2  7641  dfac8  7645  dfac9  7646  dfac10b  7649  acacni  7650  dfacacn  7651  dfac13  7652  kmlem1  7660  kmlem2  7661  kmlem9  7668  kmlem10  7669  kmlem11  7670  kmlem12  7671  kmlem13  7672  cdafn  7679  pwsdompw  7714  infmap2  7728  ackbij1lem5  7734  ackbij1lem8  7737  ackbij2lem3  7751  ackbij2  7753  cflm  7760  cardcf  7762  cfeq0  7766  cfsuc  7767  cff1  7768  cfflb  7769  cfval2  7770  cflim2  7773  cfss  7775  cfslb2n  7778  cofsmo  7779  cfsmolem  7780  cfcoflem  7782  coftr  7783  sornom  7787  infpssr  7818  fin4en1  7819  fin23lem11  7827  enfin2i  7831  fin23lem26  7835  fin23lem14  7843  fin23lem16  7845  fin23lem17  7848  fin23lem21  7849  fin23lem32  7854  fin23lem34  7856  fin23lem39  7860  compsscnvlem  7880  compssiso  7884  isf34lem4  7887  enfin1ai  7894  isfin1-3  7896  fin67  7905  dffin7-2  7908  fin1a2lem7  7916  fin1a2lem10  7919  fin1a2lem12  7921  fin1a2lem13  7922  fin12  7923  itunitc1  7930  itunitc  7931  ituniiun  7932  hsmexlem2  7937  hsmexlem4  7939  hsmex  7942  axcc2lem  7946  axcc3  7948  acncc  7950  fin41  7954  dominf  7955  dcomex  7957  axdc2lem  7958  axdc3lem  7960  axdc3lem2  7961  axdc3lem4  7963  axdc4lem  7965  axcclem  7967  ac9  7994  ac6s  7995  ac6sg  7999  ac9s  8004  numthcor  8005  zorn2lem1  8007  zorn2lem4  8010  zorn2lem7  8013  zorng  8015  zornn0g  8016  ttukeylem5  8024  ttukeylem6  8025  ttukeylem7  8026  axdclem  8030  axdclem2  8031  fodomg  8034  fodomb  8035  brdom3  8037  brdom5  8038  brdom4  8039  brdom7disj  8040  brdom6disj  8041  iunfo  8045  ondomon  8067  cardmin  8068  alephval2  8074  dominfac  8075  fpwwe2lem1  8133  fpwwe2lem8  8139  fpwwe2lem11  8142  fpwwe2lem12  8143  fpwwe2lem13  8144  fpwwe2  8145  fpwwe  8148  canthwe  8153  canthp1lem1  8154  pwfseqlem1  8160  pwfseqlem2  8161  pwfseqlem3  8162  pwfseqlem4a  8163  pwfseqlem5  8165  pwxpndom2  8167  gchac  8175  gch2  8181  inawinalem  8191  winainflem  8195  winalim2  8198  winafp  8199  gchina  8201  wunfi  8223  intwun  8237  wunex2  8240  uniwun  8242  eltsk2g  8253  inttsk  8276  inar1  8277  rankcf  8279  tskcard  8283  tskuni  8285  gruun  8308  intgru  8316  ingru  8317  wfgru  8318  grudomon  8319  gruina  8320  grur1a  8321  grur1  8322  grutsk  8324  axgroth5  8326  axgroth2  8327  grothpw  8328  grothpwex  8329  axgroth6  8330  grothomex  8331  grothac  8332  axgroth3  8333  grothprim  8336  grothtsk  8337  inaprc  8338  nqereu  8433  nqerf  8434  dmrecnq  8472  ltaddnq  8478  genpnnp  8509  genpnmax  8511  genpcl  8512  nqpr  8518  addclprlem1  8520  mulclprlem  8523  distrlem4pr  8530  1idpr  8533  prlem934  8537  ltaddpr  8538  ltexprlem3  8542  ltexprlem4  8543  ltexprlem6  8545  ltexprlem7  8546  prlem936  8551  reclem2pr  8552  reclem3pr  8553  mulasssr  8592  ltsosr  8596  0idsr  8599  1idsr  8600  ltasr  8602  recexsrlem  8605  mulgt0sr  8607  supsrlem  8613  ltresr  8642  axmulass  8659  axrrecex  8665  axpre-lttri  8667  wuncn  8672  renfdisj  8765  wloglei  9185  lbinfm  9587  supmul1  9599  supmullem1  9600  supmullem2  9601  supmul  9602  dfinfmr  9611  infmsup  9612  infmrgelb  9614  infmrlb  9615  dfnn2  9639  dflt2  10361  xrinfmss2  10507  infmxrgelb  10531  xrinfm0  10533  fzpr  10718  uzrdgfni  10899  axdc4uzlem  10922  axdc4uz  10923  seqval  10935  seqfeq4  10973  serle  10979  seqof  10981  hashxplem  11262  hashmap  11264  hashpw  11265  hashfun  11266  hashbclem  11267  hashfacen  11269  hashf1lem1  11270  hashf1lem2  11271  hashf1  11272  fz1isolem  11276  ccatfn  11304  wrdexb  11326  wrdind  11354  shftfval  11442  shftfib  11444  shftfn  11445  2shfti  11452  sqrlem6  11610  rexfiuz  11708  rlimdm  11902  fclim  11904  climshft  11927  fsum2dlem  12110  fsumcom2  12114  fsum0diag2  12122  fsumabs  12136  fsumrlim  12146  fsumo1  12147  fsumiun  12156  isumltss  12181  supcvg  12188  xpnnenOLD  12362  rpnnen2lem11  12377  algrf  12617  isprm2lem  12639  isprm2  12640  prmind2  12643  iserodd  12762  4sqlem12  12877  vdwmc  12899  vdwlem10  12911  vdwlem13  12914  ramtlecl  12921  hashbc0  12926  ramval  12929  ramcl2lem  12930  ramub2  12935  0ram  12941  ram0  12943  ramub1lem1  12947  ramub1lem2  12948  ramub1  12949  restfn  13203  elrest  13206  restsspw  13210  prdsval  13229  prdsle  13235  prdsless  13236  prdsleval  13250  pwsle  13265  imasaddfnlem  13304  imasvscafn  13313  imasleval  13317  xpsc0  13336  xpsc1  13337  xpsfrnel2  13341  ismre  13364  fnmre  13365  ismred  13376  mremre  13378  fnmrc  13381  mrcfval  13382  isacs2  13400  mreacs  13404  acsfn  13405  acsfn1  13407  acsfn2  13409  cidffn  13424  comfeq  13453  invsym2  13509  oppcsect2  13521  brssc  13535  sscpwex  13536  isssc  13541  issubc  13556  isfuncd  13583  cofucl  13606  funcres2b  13615  funcpropd  13618  setcmon  13763  catcval  13772  fnxpc  13794  xpcval  13795  xpccatid  13806  curf2ndf  13865  drsdirfi  13916  isdrs2  13917  clatl  14064  odupos  14083  oduposb  14084  oduglb  14087  odulub  14089  posglbd  14097  ipoval  14101  ipolerval  14103  fpwipodrs  14111  ipodrsima  14112  isacs5lem  14116  psdmrn  14151  psssdm2  14159  submacs  14277  pwsdiagmhm  14280  gsumwspan  14303  mulgpropd  14435  subgacs  14487  nsgacs  14488  eqgfval  14500  eqgval  14501  gicsubgen  14577  gaid  14588  gaorb  14596  orbsta  14602  symgval  14606  symgbas  14607  symgplusg  14611  sylow1lem2  14745  sylow2alem1  14763  sylow2alem2  14764  sylow2a  14765  sylow2blem1  14766  sylow2blem2  14767  sylow2blem3  14768  sylow3lem1  14773  sylow3lem3  14775  sylow3lem6  14778  efgval  14861  efgval2  14868  efgrelexlemb  14894  efgcpbllema  14898  efgcpbllemb  14899  vrgpfval  14910  frgpuplem  14916  divsabl  14992  frgpnabllem1  14996  gsumval3  15026  gsumzaddlem  15038  gsumzadd  15039  gsum2d  15058  gsum2d2  15060  gsumcom2  15061  gsumxp  15062  dprdfadd  15090  dprdres  15098  subgdmdprd  15104  dprd2dlem1  15111  dprd2d2  15114  ablfac1eulem  15142  pgpfac1lem5  15149  opprsubg  15253  subrgmre  15404  subsubrg2  15407  subrgpropd  15414  lss1d  15555  lssintcl  15556  lssmre  15558  lssacs  15559  pwsdiaglmhm  15649  islbs3  15742  lbsextlem4  15746  drngnidl  15813  lidldvgen  15839  psrbaglefi  15950  mplcoe1  16041  mplcoe2  16043  ltbval  16045  ltbwe  16046  opsrle  16049  opsrtoslem1  16057  opsrtoslem2  16058  evlslem4  16077  coe1mul2  16178  coe1tm  16181  znleval  16340  cssmre  16425  thlle  16429  pjfval2  16441  istopon  16495  tgval2  16526  bastg  16536  tgdom  16548  distop  16565  indistopon  16570  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  fncld  16591  cldss2  16599  ntreq0  16646  discld  16658  mretopd  16661  toponmre  16662  neisspw  16676  opnnei  16689  tgrest  16722  resttopon  16724  restco  16727  restdis  16741  ordtbas2  16753  ordtcnv  16763  ordtrest2  16766  pnfnei  16782  mnfnei  16783  iscnp2  16801  subbascn  16816  cnntr  16836  cnrest2  16846  cnpresti  16848  cnprest  16849  cnprest2  16850  ist1-3  16909  hausnei2  16913  isnrm2  16918  dishaus  16942  cmpcovf  16950  fincmp  16952  cmpsublem  16958  cmpsub  16959  cmpcld  16961  uncmp  16962  fiuncmp  16963  hauscmplem  16965  cmpfi  16967  dfcon2  16977  consuba  16978  cnconn  16980  uncon  16987  t1conperf  16994  is1stc2  17000  1stcfb  17003  2ndcsb  17007  2ndc1stc  17009  1stcrest  17011  2ndcctbss  17013  2ndcdisj  17014  2ndcomap  17016  2ndcsep  17017  dis2ndc  17018  llyi  17032  nllyi  17033  nlly2i  17034  llynlly  17035  subislly  17039  restnlly  17040  restlly  17041  islly2  17042  llyrest  17043  llyidm  17046  nllyidm  17047  hausllycmp  17052  cldllycmp  17053  lly1stc  17054  dislly  17055  hausmapdom  17058  kgenf  17068  iskgen3  17076  llycmpkgen2  17077  1stckgenlem  17080  1stckgen  17081  kgencn2  17084  txuni2  17092  txbas  17094  eltx  17095  ptpjpre1  17098  ptuni2  17103  ptpjcn  17137  ptpjopn  17138  ptclsg  17141  dfac14  17144  xkoccn  17145  txcnp  17146  txcnmpt  17150  prdstopn  17154  txrest  17157  txdis  17158  txindis  17160  txdis1cn  17161  txlly  17162  txnlly  17163  pthaus  17164  txcmplem1  17167  txcmplem2  17168  hausdiag  17171  txlm  17174  tx1stc  17176  tx2ndc  17177  txkgen  17178  xkopt  17181  xkococnlem  17185  xkococn  17186  cnmpt1st  17194  cnmpt2nd  17195  xkofvcn  17210  xkoinjcn  17213  txcon  17215  qtoptop2  17222  qtopuni  17225  basqtop  17234  tgqtop  17235  hmphdis  17319  indishmph  17321  txhmeo  17326  pt1hmeo  17329  ptuncnv  17330  ptunhmeo  17331  xpstopnlem1  17332  ptcmpfi  17336  xkohmeo  17338  isfbas  17356  isfbas2  17362  fbssfi  17364  trfbas2  17370  isfild  17385  snfil  17391  elfg  17398  fgcl  17405  filcon  17410  fbasrn  17411  filuni  17412  trfil2  17414  cfinfil  17420  csdfil  17421  supfil  17422  zfbas  17423  isufil2  17435  filssufilg  17438  acufl  17444  filufint  17447  uffix  17448  ufinffr  17456  ufildr  17458  fin1aufil  17459  rnelfmlem  17479  rnelfm  17480  fmfnfmlem3  17483  fmfnfmlem4  17484  fmfnfm  17485  ufldom  17489  flimrest  17510  hauspwpwf1  17514  txflf  17533  fclsrest  17551  fclscmp  17557  alexsubb  17572  alexsubALTlem1  17573  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  ptcmplem2  17579  ptcmplem3  17580  ptcmplem4  17581  ptcmplem5  17582  tmdgsum  17610  symgtgp  17616  cldsubg  17625  tgpconcomp  17627  divstgplem  17635  divstgphaus  17637  prdstmdd  17638  tsmsval2  17644  tsmssubm  17657  imasdsf1olem  17769  xpsdsval  17777  xmetec  17812  prdsbl  17869  stdbdxmet  17893  met1stc  17899  prdsxmslem2  17907  dscopn  17928  xrtgioo  18144  xrsblre  18149  icccmplem1  18159  icccmplem2  18160  fsumcn  18206  fsum2cn  18207  cnllycmp  18286  isphtpc  18324  pi1blem  18369  iscmet3  18551  metcld2  18564  bcthlem4  18581  minveclem3b  18624  ovolfiniun  18692  ovoliunlem1  18693  ovoliunlem2  18694  finiunmbl  18733  volfiniun  18736  iundisj2  18738  uniioombllem3  18772  vitalilem2  18796  vitalilem3  18797  vitali  18800  mbfimaopnlem  18842  itg1addlem4  18886  mbfi1fseqlem4  18905  mbfi1fseqlem6  18907  itgfsum  19013  ellimc2  19059  limcflf  19063  perfdvf  19085  dvres  19093  dvres2  19094  dvnff  19104  dvcj  19131  dvrec  19136  dvmptfsum  19154  dvef  19159  rolle  19169  dvivthlem1  19187  dvfsumle  19200  dvfsumabs  19202  dvfsumlem2  19206  dvfsumlem3  19207  ftc1cn  19222  mpfind  19260  pf1ind  19270  vieta1lem2  19523  elqaalem2  19532  ulmdv  19612  logfac  19786  xrlimcnp  20095  jensenlem1  20113  jensenlem2  20114  jensen  20115  wilthlem2  20139  prmorcht  20248  lgsquadlem1  20425  lgsquadlem2  20426  dchrisumlema  20469  dchrisumlem3  20472  ex-natded9.26  20664  nvss  20979  vsfval  21021  h2hlm  21390  axhcompl-zf  21408  hlim2  21601  hhcmpl  21609  hhcms  21612  shex  21621  isch2  21633  helch  21653  hhsscms  21686  occl  21713  chintcli  21740  dfch2  21816  spanuni  21953  spansni  21966  elnlfn  22338  nmopun  22424  nlelchi  22471  cnlnssadj  22490  adjbd1o  22495  branmfn  22515  pjnmopi  22558  hmopidmchi  22561  dmgmseqn0  22867  derangenlem  22873  subfacp1lem1  22881  subfacp1lem3  22884  subfacp1lem4  22885  subfacp1lem5  22886  erdszelem7  22899  erdszelem8  22900  erdsze2lem2  22906  kur14lem9  22916  ptpcon  22935  indispcon  22936  conpcon  22937  cnllyscon  22947  rellyscon  22953  cvmsss2  22976  cvmcov2  22977  cvmliftlem15  23000  cvmlift2lem1  23004  cvmlift2lem12  23016  umgraex  23046  eupath  23076  ghomgrplem  23167  relexpindlem  23207  rtrclreclem.trans  23214  dfrtrcl2  23216  untsucf  23227  dftr6  23277  coepr  23279  dffr5  23280  dfso2  23281  dfpo2  23282  br8  23283  br6  23284  br4  23285  dfres3  23286  cnvco1  23287  cnvco2  23288  fundmpss  23290  fprb  23297  dfdm5  23300  dfrn5  23301  setinds  23302  dfon2lem1  23307  dfon2lem3  23309  dfon2lem6  23312  dfon2lem7  23313  dfon2lem8  23314  dfon2  23316  rdgprc  23319  dfrdg2  23320  predreseq  23347  predpo  23352  predbrg  23354  setlikespec  23355  predep  23360  preddowncl  23364  preduz  23368  predfz  23371  tz6.26  23373  trpredrec  23409  poseq  23421  soseq  23422  wfrlem5  23428  wfrlem10  23433  wfrlem12  23435  wfrlem13  23436  wfrlem14  23437  wfrlem16  23439  tfrALTlem  23444  frrlem5  23453  frrlem11  23461  axsltsolem1  23489  axfelem18  23531  axfelem22  23535  txpss3v  23593  brtxp  23595  brtxp2  23596  pprodss4v  23599  brpprod  23600  brpprod3a  23601  brpprod3b  23602  brsset  23604  idsset  23605  dfon3  23607  brtxpsd  23609  brbigcup  23613  dfbigcup2  23614  fobigcup  23615  elfix  23618  elfix2  23619  dffix2  23620  fixcnv  23623  limitssson  23626  dfom5b  23627  elfuns  23628  elfunsg  23629  elsingles  23631  fnsingle  23632  fvsingle  23633  dfiota3  23636  brimage  23639  brimageg  23640  funimage  23641  fnimage  23642  imageval  23643  brcart  23645  brdomaing  23648  brrangeg  23649  brimg  23650  brapply  23651  brcup  23652  brcap  23653  brsuccf  23654  funpartfun  23655  funpartfv  23657  fullfunfv  23659  brrestrict  23661  dfrdg4  23662  tfrqfree  23663  altopelaltxp  23684  altxpsspw  23685  brsegle  23905  fvline  23941  liness  23942  ellines  23949  bpoly2  23966  bpoly3  23967  rankung  23970  ranksng  23971  rankelg  23972  rankpwg  23973  rankeq1o  23975  elhf2g  23980  hfext  23987  onsucconi  24050  tpssg  24097  fatesg  24121  eqvinopb  24130  copsexgb  24131  elo  24206  stcat  24209  splint  24213  domfldrefc  24222  ranfldrefc  24223  domrngref  24225  domintrefb  24228  restidsing  24241  prj1b  24244  prj3  24245  eloi  24251  elintabg  24255  domintrefc  24291  inttpemp  24305  mapmapmap  24314  injsurinj  24315  npincppr  24325  repcpwti  24327  cbcpcp  24328  cbicp  24332  prjmapcp2  24336  dstr  24337  iscst4  24343  islatalg  24349  domrancur1c  24368  mnlmxl2  24435  defse3  24438  inpc  24443  inposet  24444  tolat  24452  toplat  24456  dfdir2  24457  prodeq3ii  24474  fprodser  24486  symgfo  24534  svs2  24653  inttop2  24681  sallnei  24695  nsn  24696  dmhmph  24699  rnhmph  24700  intopcoaconlem3b  24704  intopcoaconlem3  24705  qusp  24708  efilcp  24718  fgsb2  24721  bwt2  24758  dmrngcmp  24917  dualded  24949  ishomd  24956  vtarsuelt  25061  fnctartar  25073  fnctartar2  25074  dfiunv2  25082  prismorcset2  25084  domcatfun  25091  codcatfun  25100  idcatfun  25107  empklst  25175  fnckle  25211  pfsubkl  25213  pgapspf2  25219  isconcl5a  25267  isconcl5ab  25268  bosser  25333  pdiveql  25334  abhp2  25341  bhp2a  25342  cnvresimaOLD  25392  trer  25393  finminlem  25397  gtinf  25400  fneer  25454  fnessref  25459  refssfne  25460  islocfin  25462  comppfsc  25473  neibastop1  25474  neibastop2lem  25475  neibastop3  25477  topmeet  25479  topjoin  25480  neifg  25486  tailfb  25492  filnetlem2  25494  filnetlem3  25495  filnetlem4  25496  cover2g  25525  f1opr  25557  inixp  25565  indexdom  25579  frinfm  25582  sdclem2  25618  sdclem1  25619  fdc  25621  isbndx  25672  prdstotbnd  25684  heibor1lem  25699  heiborlem1  25701  heiborlem3  25703  heiborlem4  25704  heiborlem5  25705  heiborlem6  25706  heiborlem8  25708  heiborlem10  25710  ismrer1  25728  riscer  25785  divrngidl  25819  intidl  25820  isfldidl  25859  ispridlc  25861  prtlem10  25899  prtlem13  25902  prtlem16  25903  prtlem19  25912  prter2  25915  prter3  25916  ralxpmap  25927  elrfi  25935  ismrcd1  25939  ismrcd2  25940  istopclsd  25941  ismrc  25942  mrefg2  25948  isnacs3  25951  mzpclall  25971  mzpincl  25978  mzpsubst  25992  mzpcompact2lem  25995  mzpcompact2  25996  eldioph2lem1  26005  eldioph2lem2  26006  eldiophss  26020  diophrex  26021  rexrabdioph  26041  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  rabren3dioph  26064  fphpd  26065  rencldnfilem  26069  pellexlem5  26084  pellex  26086  rmxypairf1o  26162  monotuz  26192  monotoddzzfi  26193  oddcomabszz  26195  2nn0ind  26196  zindbi  26197  mzpcong  26225  rmydioph  26273  rmxdioph  26275  expdiophlem2  26281  setindtr  26283  setindtrs  26284  dford3lem2  26286  ttac  26295  pw2f1ocnv  26296  wepwsolem  26304  inisegn0  26306  dnnumch1  26307  fnwe2val  26312  fnwe2lem2  26314  aomclem1  26317  aomclem2  26318  aomclem6  26322  dfac11  26326  kelac2lem  26328  dfac21  26330  islssfg2  26335  lmhmlnmsplit  26351  pwssplit3  26356  filnm  26358  pwslnmlem1  26360  pwslnm  26362  dsmmval  26366  frlmlbs  26415  unxpwdom3  26422  enfixsn  26423  dfacbasgrp  26439  islindf4  26474  lmisfree  26478  lnr2i  26486  lnrfg  26489  hbtlem6  26499  rngunsnply  26544  pmtrfval  26559  symggen  26577  gsumcom3  26620  acsfn1p  26673  sdrgacs  26675  idomsubgmo  26680  fgraphxp  26696  expgrowth  26718  2sbc6g  26782  iotain  26784  compel  26807  ipo0  26819  ifr0  26820  onfrALTlem5  27000  onfrALTlem4  27001  onfrALTlem3  27002  opelopab4  27010  a9e2nd  27017  trsspwALT  27282  trsspwALT2  27283  trsspwALT3  27284  pwtrVD  27288  pwtrOLD  27289  unipwrVD  27298  unipwr  27299  onfrALTlem5VD  27351  onfrALTlem4VD  27352  onfrALTlem3VD  27353  relopabVD  27367  a9e2ndVD  27374  sspwimp  27384  sspwimpVD  27385  sspwimpcf  27386  sspwimpcfVD  27387  sspwimpALT  27391  sspwimpALT2  27395  a9e2ndALT  27397  bnj23  27433  bnj62  27435  bnj156  27445  bnj219  27450  bnj610  27465  bnj918  27485  bnj927  27489  bnj976  27498  bnj1098  27504  bnj1379  27552  bnj110  27579  bnj98  27588  bnj154  27599  bnj155  27600  bnj535  27611  bnj556  27621  bnj557  27622  bnj581  27629  bnj591  27632  bnj594  27633  bnj580  27634  bnj607  27637  bnj609  27638  bnj600  27640  bnj849  27646  bnj893  27649  bnj908  27652  bnj934  27656  bnj944  27659  bnj964  27664  bnj966  27665  bnj969  27667  bnj970  27668  bnj910  27669  bnj986  27675  bnj999  27678  bnj1018  27683  bnj907  27686  bnj1039  27690  bnj1040  27691  bnj1052  27694  bnj1123  27705  bnj1030  27706  bnj1133  27708  bnj1128  27709  bnj1145  27712  bnj1204  27731  bnj1373  27749  bnj1417  27760  bnj1421  27761  bnj1498  27780  eqlkr2  27979  glbconxN  28256  pmapglbx  28647  pmapglb  28648  pclclN  28769  pclfinN  28778  polval2N  28784  pclfinclN  28828  osumcllem10N  28843  pexmidlem7N  28854  cdleme31sdnN  29265  cdlemefr44  29303  cdleme48fv  29377  cdleme46fvaw  29379  cdleme48bw  29380  cdleme46fsvlpq  29383  cdlemeg46fvcl  29384  cdlemeg49le  29389  cdlemeg46fjgN  29399  cdlemeg46fjv  29401  cdleme48d  29413  cdlemeg49lebilem  29417  cdleme50eq  29419  cdleme50f  29420  cdlemg2jlemOLDN  29471  cdlemg2klem  29473  cdlemk40  29795  cdlemk56  29849  diaglbN  29934  dvhlveclem  29987  dib1dim  30044  dibglbN  30045  diblss  30049  diblsmopel  30050  dicelvalN  30057  diclspsn  30073  cdlemn7  30082  dihordlem7  30093  dihopelvalcpre  30127  xihopellsmN  30133  dihopellsm  30134  dih1  30165  dihmeetlem1N  30169  dihglblem5apreN  30170  dihmeetlem2N  30178  dihglbcpreN  30179  dihmeetlem4preN  30185  dihmeetlem13N  30198  dih1dimatlem  30208  dihatlat  30213  dihjatcclem4  30300  lcdlss  30498
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-v 2729
  Copyright terms: Public domain W3C validator