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

Theorem vex 2792
Description: All set variables are sets (see isset 2793). 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 2284 . 2  |-  x  =  x
2 df-v 2791 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2391 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 202 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1628    e. wcel 1688   _Vcvv 2789
This theorem is referenced by:  isset  2793  ralv  2802  rexv  2803  reuv  2804  rmov  2805  rabab  2806  sbhypf  2834  ceqex  2899  ralab  2927  rexab  2929  moeq3  2943  mo2icl  2945  reu8  2962  sbc2or  3000  csbvarg  3109  csbiebg  3121  sbcnestgf  3129  sbnfc2  3142  ddif  3309  csbing  3377  dfun2  3405  dfin2  3406  vn0  3463  eqv  3471  abvor0  3473  sbss  3564  csbifg  3594  ifexg  3625  elpwg  3633  dftp2  3680  prnzg  3747  snssg  3755  difprsn  3757  sneqrg  3783  preq12bg  3792  pwpr  3824  pwtp  3825  pwv  3827  unipr  3842  uniprg  3843  unisng  3845  elintg  3871  elintrabg  3876  intss1  3878  ssint  3879  intmin  3883  intss  3884  intssuni  3885  intmin4  3892  intab  3893  intun  3895  intpr  3896  intprg  3897  uniintsn  3900  iinconst  3915  iuniin  3916  iinss1  3918  dfiin2g  3937  ssiinf  3952  iinss  3954  iinss2  3955  0iin  3961  iinab  3964  iinun2  3969  iundif2  3970  iindif2  3972  iinin2  3973  iinuni  3986  sspwuni  3988  iinpw  3991  iunpwss  3992  brab1  4069  csbopabg  4095  mptv  4113  trint  4129  trintss  4130  vprc  4153  inex1g  4158  ssexg  4161  intex  4170  inuni  4176  axpweq  4186  pwexg  4193  pwuni  4205  axpr  4212  zfpair2  4214  elALT  4217  rext  4221  sspwb  4222  unipw  4223  ssextss  4226  nnullss  4234  exss  4235  opth  4244  opthg  4245  copsexg  4251  copsex4g  4254  moop2  4260  euotd  4266  opelopabsbOLD  4272  opelopabsb  4274  pwin  4296  pwunss  4297  pwssun  4298  pwundifOLD  4300  epelg  4305  epel  4307  dfid3  4309  pofun  4329  epse  4375  wefrc  4386  tron  4414  onfr  4430  sucel  4464  suctr  4474  uniexg  4516  unexb  4519  snnex  4523  uniuni  4526  eusvnf  4528  eusvnfb  4529  reusv6OLD  4544  iunpw  4569  onint  4585  ordpwsuc  4605  unon  4621  ordunisuc  4622  onuninsuci  4630  orduninsuc  4633  limsssuc  4640  limuni3  4642  tfinds  4649  tfindsg  4650  tfindsg2  4651  tfinds2  4653  dfom2  4657  peano5  4678  finds  4681  findsg  4682  finds2  4683  0nelxp  4716  opelxp  4718  opeliunxp  4739  elvv  4747  elvvv  4748  elvvuni  4749  xpsspw  4796  xpsspwOLD  4797  relopabi  4810  opabid2  4814  difopab  4816  xpiindi  4820  ralxpf  4829  relop  4833  cnvco  4864  dfrn2  4867  dfdm4  4871  dmss  4877  dmin  4885  dmiun  4886  dmuni  4887  dm0  4891  dmi  4892  reldm0  4895  elreldm  4902  elrnmpt1  4927  dmrnssfld  4937  dmcoss  4943  dmcosseq  4945  opelresg  4961  resieq  4964  dmres  4975  elres  4989  relssres  4991  resopab  4995  resiexg  4996  iss  4997  dfres2  5001  dfima2  5013  csbima12g  5021  imadmrn  5023  imai  5026  elimasng  5038  args  5040  epini  5042  iniseg  5043  dffr3  5044  dfse2  5045  exse2  5046  cotr  5054  issref  5055  cnvsym  5056  intasym  5057  asymref  5058  asymref2  5059  intirr  5060  brcodir  5061  codir  5062  qfto  5063  poirr2  5066  cnvopab  5082  cnv0  5083  cnvi  5084  cnvdif  5086  rniun  5090  dminss  5094  imainss  5095  ssrnres  5115  rninxp  5116  dminxp  5117  cnvcnv3  5122  dfrel2  5123  dmsnn0  5136  dmsnopg  5142  cnvcnvsn  5148  dmsnsnsn  5149  cnvsng  5156  elxp4  5158  elxp5  5159  cnvresima  5160  dfco2  5170  dfco2a  5171  cores  5174  resco  5175  imaco  5176  rnco  5177  coiun  5180  co02  5184  coi1  5186  coass  5189  relssdmrn  5191  unielrel  5195  unixp0  5204  ressn  5209  cnviin  5210  cnvpo  5211  cnvso  5212  dffun2  5231  dffun7  5246  dffun8  5247  dffun9  5248  funopg  5252  funssres  5259  funun  5261  funcnvsn  5262  funcnv2  5274  funcnv  5275  funcnv3  5276  fun2cnv  5277  funcnvuni  5282  imadif  5292  isarep1  5296  2elresin  5320  fnres  5325  fcnvres  5383  fabexg  5387  fconstg  5393  fun11iun  5458  f1osng  5479  fv2  5481  fvprc  5482  fvex  5499  fv3  5501  nfunsn  5519  funimass4  5534  ssimaexg  5546  dffv2  5553  dmfco  5554  fvopab6  5582  fndmdif  5590  iinpreima  5616  fvelrn  5622  dff3  5634  dffo4  5637  exfo  5639  f1ompt  5643  fmptco  5652  fsng  5658  dfmpt  5662  fnressn  5666  fressnfv  5668  fvsng  5675  zfrep6  5709  funfvima3  5716  idref  5720  fvclss  5721  fvresex  5723  abrexco  5727  opabex3  5730  imaiun  5732  dff13  5744  foeqcnvco  5765  f1eqcocnv  5766  fliftcnv  5771  isocnv2  5789  isomin  5795  isoini  5796  isofr  5800  isose  5801  f1oweALT  5812  wemoiso  5816  wemoiso2  5817  knatar  5818  oprabid  5843  csbovg  5850  eloprabga  5895  mpt2v  5898  caovmo  6018  f1opw  6033  ofmres  6077  op1stg  6093  op2ndg  6094  1stval2  6098  2ndval2  6099  fo1st  6100  fo2nd  6101  f1stres  6102  f2ndres  6103  fo1stres  6104  fo2ndres  6105  1st2val  6106  2nd2val  6107  xp1st  6110  xp2nd  6111  sbcopeq1a  6133  csbopeq1a  6134  eloprabi  6147  mpt2mptsx  6148  dmmpt2ssx  6150  fmpt2x  6151  ovmptss  6161  fmpt2co  6163  df1st2  6166  df2nd2  6167  1stconst  6168  2ndconst  6169  curry1  6171  curry2  6174  fparlem1  6179  fparlem2  6180  fpar  6183  fsplit  6184  frxp  6186  xporderlem  6187  soxp  6189  fnwelem  6191  fnse  6193  reldmtpos  6203  dmtpos  6207  rntpos  6208  ovtpos  6210  dftpos3  6213  dftpos4  6214  tpostpos  6215  porpss  6242  sorpss  6243  sorpsscmpl  6249  uniabio  6262  iotaval  6263  sniota  6279  opiota  6283  opabiotafun  6284  opabiota  6286  riotav  6304  csbriotag  6312  onovuni  6354  smogt  6379  tfrlem3  6388  tfrlem8  6395  tfrlem9a  6397  tfrlem16  6404  tz7.44lem1  6413  rdg0g  6435  rdglim2  6440  tz7.48-1  6450  seqomlem1  6457  seqomlem2  6458  abianfplem  6465  oacl  6529  omcl  6530  oecl  6531  oa0r  6532  om0r  6533  om1r  6536  oe1m  6538  oaordi  6539  oawordri  6543  oawordeulem  6547  oalimcl  6553  oaass  6554  oarec  6555  omordi  6559  omwordri  6565  omlimcl  6571  odi  6572  omass  6573  omeulem1  6575  oen0  6579  oeordi  6580  oewordri  6585  oeworde  6586  oeoalem  6589  oeoelem  6591  nnawordex  6630  omabs  6640  omsmolem  6646  ercnv  6676  iserd  6681  eqerlem  6687  eqer  6688  ecdmn0  6697  erth  6699  erdisj  6702  qsss  6715  ecid  6719  qsid  6720  iiner  6726  qsel  6733  erovlem  6749  ecopovsym  6755  ecopovtrn  6756  ecopover  6757  mapprc  6771  fnmap  6774  fnpm  6775  mapval2  6792  pmsspw  6797  mapsn  6804  mapsncnv  6809  ixpconstg  6820  ixpprc  6832  uniixp  6834  ixpin  6836  ixpiin  6837  resixpfo  6849  elixpsn  6850  ixpsnf1o  6851  boxriin  6853  boxcutc  6854  bren  6866  brdomg  6867  domen  6870  domeng  6871  idssen  6901  ener  6903  domtr  6909  ensn1g  6921  en1  6923  en1b  6924  fundmen  6929  fundmeng  6930  mapsnen  6933  unen  6938  domdifsn  6940  xpsnen  6941  xpsneng  6942  xpcomeng  6949  xpassen  6951  xpdom2  6952  xpdom2g  6953  domunsncan  6957  omxpenlem  6958  pw2f1o  6962  fopwdom  6965  sbthlem10  6975  sbth  6976  sbthcl  6978  domunsn  7006  fodomr  7007  pwdom  7008  canth2  7009  canth2g  7010  domssex  7017  xpf1o  7018  mapen  7020  mapunen  7025  map2xp  7026  mapdom2  7027  mapdom3  7028  ssenen  7030  infensuc  7034  nneneq  7039  php  7040  php2  7041  php3  7042  sucdom2  7052  1sdom  7060  unxpdomlem2  7063  unxpdomlem3  7064  isinf  7071  fineqvlem  7072  fineqv  7073  pssnn  7076  ssfi  7078  dif1enOLD  7085  dif1en  7086  findcard  7092  findcard2  7093  findcard2s  7094  ac6sfi  7096  frfi  7097  fimax2g  7098  unbnn2  7109  isfinite2  7110  xpfi  7123  domunfican  7124  fiint  7128  fodomfi  7130  fodomfib  7131  iunfi  7139  pwfilem  7145  ixpfi2  7149  fissuni  7155  fipreima  7156  finsschain  7157  fival  7161  ssfii  7167  fi0  7168  fiin  7170  dffi2  7171  fipwuni  7174  fisn  7175  elfiun  7178  dffi3  7179  fifo  7180  marypha1lem  7181  dfsup2  7190  dfsup2OLD  7191  ordiso2  7225  oismo  7250  hartogslem1  7252  hartogs  7254  wofib  7255  wemappo  7259  wemapso2lem  7260  card2on  7263  brwdom  7276  brwdomn0  7278  brwdom2  7282  wdomtr  7284  wdompwdom  7287  canthwdom  7288  xpwdomg  7294  unxpwdom2  7297  ixpiunwdom  7300  elirrv  7306  zfregfr  7311  inf0  7317  inf3lema  7320  inf3lemd  7323  inf3lem1  7324  inf3lem2  7325  inf3lem3  7326  inf3lem5  7328  inf3lem6  7329  inf3lem7  7330  inf3  7331  infeq5  7333  omex  7339  dfom3  7343  dfom5  7346  infdifsn  7352  cantnfdm  7360  cantnfval  7364  cantnfval2  7365  cantnflt  7368  cantnff  7370  oemapso  7379  cantnflem1  7386  wemapwe  7395  cnfcom  7398  cnfcom3clem  7403  epfrs  7408  tcvalg  7418  tctr  7420  tcmin  7421  r1sdom  7441  r1val1  7453  tz9.12lem1  7454  tz9.12lem3  7456  tz9.13  7458  tz9.13g  7459  rankf  7461  unir1  7480  rankvalg  7484  rankonidlem  7495  r1val2  7504  bndrank  7508  ranklim  7511  r1pwOLD  7513  rankunb  7517  rankuni2b  7520  rankuni  7530  rankval4  7534  rankxplim  7544  rankxplim3  7546  rankxpsuc  7547  tcrank  7549  cp  7556  bnd2  7558  kardex  7559  karden  7560  cardf2  7571  tskwe  7578  cardlim  7600  harcard  7606  cardiun  7610  pm54.43  7628  r0weon  7635  infxpenlem  7636  infxpenc2lem2  7642  fseqenlem1  7646  fseqenlem2  7647  fseqen  7649  dfac8alem  7651  dfac8clem  7654  ac10ct  7656  ween  7657  acnlem  7670  finacn  7672  acndom  7673  acndom2  7676  wdomfil  7683  infpwfien  7684  alephon  7691  alephcard  7692  alephordi  7696  cardaleph  7711  alephval3  7732  iunfictbso  7736  aceq3lem  7742  dfac3  7743  dfac4  7744  dfac5lem1  7745  dfac5lem2  7746  dfac5lem3  7747  dfac5lem4  7748  dfac5lem5  7749  dfac5  7750  dfac2a  7751  dfac2  7752  dfac8  7756  dfac9  7757  dfac10b  7760  acacni  7761  dfacacn  7762  dfac13  7763  kmlem1  7771  kmlem2  7772  kmlem9  7779  kmlem10  7780  kmlem11  7781  kmlem12  7782  kmlem13  7783  cdafn  7790  pwsdompw  7825  infmap2  7839  ackbij1lem5  7845  ackbij1lem8  7848  ackbij2lem3  7862  ackbij2  7864  cflm  7871  cardcf  7873  cfeq0  7877  cfsuc  7878  cff1  7879  cfflb  7880  cfval2  7881  cflim2  7884  cfss  7886  cfslb2n  7889  cofsmo  7890  cfsmolem  7891  cfcoflem  7893  coftr  7894  sornom  7898  infpssr  7929  fin4en1  7930  fin23lem11  7938  enfin2i  7942  fin23lem26  7946  fin23lem14  7954  fin23lem16  7956  fin23lem17  7959  fin23lem21  7960  fin23lem32  7965  fin23lem34  7967  fin23lem39  7971  compsscnvlem  7991  compssiso  7995  isf34lem4  7998  enfin1ai  8005  isfin1-3  8007  fin67  8016  dffin7-2  8019  fin1a2lem7  8027  fin1a2lem10  8030  fin1a2lem12  8032  fin1a2lem13  8033  fin12  8034  itunitc1  8041  itunitc  8042  ituniiun  8043  hsmexlem2  8048  hsmexlem4  8050  hsmex  8053  axcc2lem  8057  axcc3  8059  acncc  8061  fin41  8065  dominf  8066  dcomex  8068  axdc2lem  8069  axdc3lem  8071  axdc3lem2  8072  axdc3lem4  8074  axdc4lem  8076  axcclem  8078  ac9  8105  ac6s  8106  ac6sg  8110  ac9s  8115  numthcor  8116  zorn2lem1  8118  zorn2lem4  8121  zorn2lem7  8124  zorng  8126  zornn0g  8127  ttukeylem5  8135  ttukeylem6  8136  ttukeylem7  8137  axdclem  8141  axdclem2  8142  fodomg  8145  fodomb  8146  brdom3  8148  brdom5  8149  brdom4  8150  brdom7disj  8151  brdom6disj  8152  iunfo  8156  ondomon  8180  cardmin  8181  alephval2  8189  dominfac  8190  fpwwe2lem1  8248  fpwwe2lem8  8254  fpwwe2lem11  8257  fpwwe2lem12  8258  fpwwe2lem13  8259  fpwwe2  8260  fpwwe  8263  canthwe  8268  canthp1lem1  8269  pwfseqlem1  8275  pwfseqlem2  8276  pwfseqlem3  8277  pwfseqlem4a  8278  pwfseqlem5  8280  pwxpndom2  8282  gchac  8290  gch2  8296  inawinalem  8306  winainflem  8310  winalim2  8313  winafp  8314  gchina  8316  wunfi  8338  intwun  8352  wunex2  8355  uniwun  8357  eltsk2g  8368  inttsk  8391  inar1  8392  rankcf  8394  tskcard  8398  tskuni  8400  gruun  8423  intgru  8431  ingru  8432  wfgru  8433  grudomon  8434  gruina  8435  grur1a  8436  grur1  8437  grutsk  8439  axgroth5  8441  axgroth2  8442  grothpw  8443  grothpwex  8444  axgroth6  8445  grothomex  8446  grothac  8447  axgroth3  8448  grothprim  8451  grothtsk  8452  inaprc  8453  nqereu  8548  nqerf  8549  dmrecnq  8587  ltaddnq  8593  genpnnp  8624  genpnmax  8626  genpcl  8627  nqpr  8633  addclprlem1  8635  mulclprlem  8638  distrlem4pr  8645  1idpr  8648  prlem934  8652  ltaddpr  8653  ltexprlem3  8657  ltexprlem4  8658  ltexprlem6  8660  ltexprlem7  8661  prlem936  8666  reclem2pr  8667  reclem3pr  8668  mulasssr  8707  ltsosr  8711  0idsr  8714  1idsr  8715  ltasr  8717  recexsrlem  8720  mulgt0sr  8722  supsrlem  8728  ltresr  8757  axmulass  8774  axrrecex  8780  axpre-lttri  8782  wuncn  8787  renfdisj  8880  wloglei  9300  lbinfm  9702  supmul1  9714  supmullem1  9715  supmullem2  9716  supmul  9717  dfinfmr  9726  infmsup  9727  infmrgelb  9729  infmrlb  9730  dfnn2  9754  dflt2  10477  xrinfmss2  10623  infmxrgelb  10647  xrinfm0  10649  fzpr  10834  uzrdgfni  11015  axdc4uzlem  11038  axdc4uz  11039  seqval  11051  seqfeq4  11089  serle  11095  seqof  11097  hashxplem  11379  hashmap  11381  hashpw  11382  hashfun  11383  hashbclem  11384  hashfacen  11386  hashf1lem1  11387  hashf1lem2  11388  hashf1  11389  fz1isolem  11393  ccatfn  11421  wrdexb  11443  wrdind  11471  shftfval  11559  shftfib  11561  shftfn  11562  2shfti  11569  sqrlem6  11727  rexfiuz  11825  rlimdm  12019  fclim  12021  climshft  12044  fsum2dlem  12227  fsumcom2  12231  fsum0diag2  12239  fsumabs  12253  fsumrlim  12263  fsumo1  12264  fsumiun  12273  incexclem  12289  isumltss  12301  supcvg  12308  xpnnenOLD  12482  rpnnen2lem11  12497  algrf  12737  isprm2lem  12759  isprm2  12760  prmind2  12763  iserodd  12882  4sqlem12  12997  vdwmc  13019  vdwlem10  13031  vdwlem13  13034  ramtlecl  13041  hashbc0  13046  ramval  13049  ramcl2lem  13050  ramub2  13055  0ram  13061  ram0  13063  ramub1lem1  13067  ramub1lem2  13068  ramub1  13069  restfn  13323  elrest  13326  restsspw  13330  prdsval  13349  prdsle  13355  prdsless  13356  prdsleval  13370  pwsle  13385  imasaddfnlem  13424  imasvscafn  13433  imasleval  13437  xpsc0  13456  xpsc1  13457  xpsfrnel2  13461  ismre  13486  fnmre  13487  ismred  13498  mremre  13500  fnmrc  13503  mrcfval  13504  mrisval  13526  mreexexlem4d  13543  isacs2  13549  mreacs  13554  acsfn  13555  acsfn1  13557  acsfn2  13559  cidffn  13574  comfeq  13603  invsym2  13659  oppcsect2  13671  brssc  13685  sscpwex  13686  isssc  13691  issubc  13706  isfuncd  13733  cofucl  13756  funcres2b  13765  funcpropd  13768  setcmon  13913  catcval  13922  fnxpc  13944  xpcval  13945  xpccatid  13956  curf2ndf  14015  drsdirfi  14066  isdrs2  14067  clatl  14214  odupos  14233  oduposb  14234  oduglb  14237  odulub  14239  posglbd  14247  ipoval  14251  ipolerval  14253  fpwipodrs  14261  ipodrsima  14262  isacs5lem  14266  psdmrn  14310  psssdm2  14318  submacs  14436  pwsdiagmhm  14439  gsumwspan  14462  mulgpropd  14594  subgacs  14646  nsgacs  14647  eqgfval  14659  eqgval  14660  gicsubgen  14736  gaid  14747  gaorb  14755  orbsta  14761  symgval  14765  symgbas  14766  symgplusg  14770  sylow1lem2  14904  sylow2alem1  14922  sylow2alem2  14923  sylow2a  14924  sylow2blem1  14925  sylow2blem2  14926  sylow2blem3  14927  sylow3lem1  14932  sylow3lem3  14934  sylow3lem6  14937  efgval  15020  efgval2  15027  efgrelexlemb  15053  efgcpbllema  15057  efgcpbllemb  15058  vrgpfval  15069  frgpuplem  15075  divsabl  15151  frgpnabllem1  15155  gsumval3  15185  gsumzaddlem  15197  gsumzadd  15198  gsum2d  15217  gsum2d2  15219  gsumcom2  15220  gsumxp  15221  dprdfadd  15249  dprdres  15257  subgdmdprd  15263  dprd2dlem1  15270  dprd2d2  15273  ablfac1eulem  15301  pgpfac1lem5  15308  opprsubg  15412  subrgmre  15563  subsubrg2  15566  subrgpropd  15573  lss1d  15714  lssintcl  15715  lssmre  15717  lssacs  15718  pwsdiaglmhm  15808  islbs3  15902  lbsextlem4  15908  drngnidl  15975  lidldvgen  16001  psrbaglefi  16112  mplcoe1  16203  mplcoe2  16205  ltbval  16207  ltbwe  16208  opsrle  16211  opsrtoslem1  16219  opsrtoslem2  16220  evlslem4  16239  coe1mul2  16340  coe1tm  16343  znleval  16502  cssmre  16587  thlle  16591  pjfval2  16603  istopon  16657  tgval2  16688  bastg  16698  tgdom  16710  distop  16727  indistopon  16732  fctop  16735  cctop  16737  ppttop  16738  epttop  16740  fncld  16753  cldss2  16761  ntreq0  16808  discld  16820  mretopd  16823  toponmre  16824  neisspw  16838  opnnei  16851  tgrest  16884  resttopon  16886  restco  16889  restdis  16903  ordtbas2  16915  ordtcnv  16925  ordtrest2  16928  pnfnei  16944  mnfnei  16945  iscnp2  16963  subbascn  16978  cnntr  16998  cnrest2  17008  cnpresti  17010  cnprest  17011  cnprest2  17012  ist1-3  17071  hausnei2  17075  isnrm2  17080  dishaus  17104  cmpcovf  17112  fincmp  17114  cmpsublem  17120  cmpsub  17121  cmpcld  17123  uncmp  17124  fiuncmp  17125  hauscmplem  17127  cmpfi  17129  dfcon2  17139  consuba  17140  cnconn  17142  uncon  17149  t1conperf  17156  is1stc2  17162  1stcfb  17165  2ndcsb  17169  2ndc1stc  17171  1stcrest  17173  2ndcctbss  17175  2ndcdisj  17176  2ndcomap  17178  2ndcsep  17179  dis2ndc  17180  llyi  17194  nllyi  17195  nlly2i  17196  llynlly  17197  subislly  17201  restnlly  17202  restlly  17203  islly2  17204  llyrest  17205  llyidm  17208  nllyidm  17209  hausllycmp  17214  cldllycmp  17215  lly1stc  17216  dislly  17217  hausmapdom  17220  kgenf  17230  iskgen3  17238  llycmpkgen2  17239  1stckgenlem  17242  1stckgen  17243  kgencn2  17246  txuni2  17254  txbas  17256  eltx  17257  ptpjpre1  17260  ptuni2  17265  ptpjcn  17299  ptpjopn  17300  ptclsg  17303  dfac14  17306  xkoccn  17307  txcnp  17308  txcnmpt  17312  prdstopn  17316  txrest  17319  txdis  17320  txindis  17322  txdis1cn  17323  txlly  17324  txnlly  17325  pthaus  17326  txcmplem1  17329  txcmplem2  17330  hausdiag  17333  txlm  17336  tx1stc  17338  tx2ndc  17339  txkgen  17340  xkopt  17343  xkococnlem  17347  xkococn  17348  cnmpt1st  17356  cnmpt2nd  17357  xkofvcn  17372  xkoinjcn  17375  txcon  17377  qtoptop2  17384  qtopuni  17387  basqtop  17396  tgqtop  17397  hmphdis  17481  indishmph  17483  txhmeo  17488  pt1hmeo  17491  ptuncnv  17492  ptunhmeo  17493  xpstopnlem1  17494  ptcmpfi  17498  xkohmeo  17500  isfbas  17518  isfbas2  17524  fbssfi  17526  trfbas2  17532  isfild  17547  snfil  17553  elfg  17560  fgcl  17567  filcon  17572  fbasrn  17573  filuni  17574  trfil2  17576  cfinfil  17582  csdfil  17583  supfil  17584  zfbas  17585  isufil2  17597  filssufilg  17600  acufl  17606  filufint  17609  uffix  17610  ufinffr  17618  ufildr  17620  fin1aufil  17621  rnelfmlem  17641  rnelfm  17642  fmfnfmlem3  17645  fmfnfmlem4  17646  fmfnfm  17647  ufldom  17651  flimrest  17672  hauspwpwf1  17676  txflf  17695  fclsrest  17713  fclscmp  17719  alexsubb  17734  alexsubALTlem1  17735  alexsubALTlem2  17736  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  ptcmplem2  17741  ptcmplem3  17742  ptcmplem4  17743  ptcmplem5  17744  tmdgsum  17772  symgtgp  17778  cldsubg  17787  tgpconcomp  17789  divstgplem  17797  divstgphaus  17799  prdstmdd  17800  tsmsval2  17806  tsmssubm  17819  imasdsf1olem  17931  xpsdsval  17939  xmetec  17974  prdsbl  18031  stdbdxmet  18055  met1stc  18061  prdsxmslem2  18069  dscopn  18090  xrtgioo  18306  xrsblre  18311  icccmplem1  18321  icccmplem2  18322  fsumcn  18368  fsum2cn  18369  cnllycmp  18448  isphtpc  18486  pi1blem  18531  iscmet3  18713  metcld2  18726  bcthlem4  18743  minveclem3b  18786  ovolfiniun  18854  ovoliunlem1  18855  ovoliunlem2  18856  finiunmbl  18895  volfiniun  18898  iundisj2  18900  uniioombllem3  18934  vitalilem2  18958  vitalilem3  18959  vitali  18962  mbfimaopnlem  19004  itg1addlem4  19048  mbfi1fseqlem4  19067  mbfi1fseqlem6  19069  itgfsum  19175  ellimc2  19221  limcflf  19225  perfdvf  19247  dvres  19255  dvres2  19256  dvnff  19266  dvcj  19293  dvrec  19298  dvmptfsum  19316  dvef  19321  rolle  19331  dvivthlem1  19349  dvfsumle  19362  dvfsumabs  19364  dvfsumlem2  19368  dvfsumlem3  19369  ftc1cn  19384  mpfind  19422  pf1ind  19432  vieta1lem2  19685  elqaalem2  19694  ulmdv  19774  logfac  19948  xrlimcnp  20257  jensenlem1  20275  jensenlem2  20276  jensen  20277  wilthlem2  20301  prmorcht  20410  lgsquadlem1  20587  lgsquadlem2  20588  dchrisumlema  20631  dchrisumlem3  20634  ex-natded9.26  20826  nvss  21141  vsfval  21183  h2hlm  21552  axhcompl-zf  21570  hlim2  21763  hhcmpl  21771  hhcms  21774  shex  21783  isch2  21795  helch  21815  hhsscms  21848  occl  21875  chintcli  21902  dfch2  21978  spanuni  22115  spansni  22128  elnlfn  22500  nmopun  22586  nlelchi  22633  cnlnssadj  22652  adjbd1o  22657  branmfn  22677  pjnmopi  22720  hmopidmchi  22723  abrexss  23033  ballotlem2  23040  ballotlemsf1o  23065  ballotlemirc  23083  dmgmseqn0  23100  derangenlem  23106  subfacp1lem1  23114  subfacp1lem3  23117  subfacp1lem4  23118  subfacp1lem5  23119  erdszelem7  23132  erdszelem8  23133  erdsze2lem2  23139  kur14lem9  23149  ptpcon  23168  indispcon  23169  conpcon  23170  cnllyscon  23180  rellyscon  23186  cvmsss2  23209  cvmcov2  23210  cvmliftlem15  23233  cvmlift2lem1  23237  cvmlift2lem12  23249  umgraex  23279  eupath  23309  ghomgrplem  23400  relexpindlem  23440  rtrclreclem.trans  23447  dfrtrcl2  23449  untsucf  23460  dftr6  23510  coepr  23512  dffr5  23513  dfso2  23514  dfpo2  23515  br8  23516  br6  23517  br4  23518  dfres3  23519  cnvco1  23520  cnvco2  23521  fundmpss  23523  fprb  23530  dfdm5  23533  dfrn5  23534  setinds  23535  dfon2lem1  23540  dfon2lem3  23542  dfon2lem6  23545  dfon2lem7  23546  dfon2lem8  23547  dfon2  23549  rdgprc  23552  dfrdg2  23553  predreseq  23580  predpo  23585  predbrg  23587  setlikespec  23588  predep  23593  preddowncl  23597  preduz  23601  predfz  23604  tz6.26  23606  trpredrec  23642  poseq  23654  soseq  23655  wfrlem5  23661  wfrlem10  23666  wfrlem12  23668  wfrlem13  23669  wfrlem14  23670  wfrlem16  23672  tfrALTlem  23677  frrlem5  23686  frrlem11  23694  axsltsolem1  23722  axfelem18  23764  axfelem22  23768  txpss3v  23826  brtxp  23828  brtxp2  23829  pprodss4v  23832  brpprod  23833  brpprod3a  23834  brpprod3b  23835  brsset  23837  idsset  23838  dfon3  23840  brtxpsd  23842  brbigcup  23846  dfbigcup2  23847  fobigcup  23848  elfix  23851  elfix2  23852  dffix2  23853  fixcnv  23856  limitssson  23859  dfom5b  23860  elfuns  23861  elfunsg  23862  elsingles  23864  fnsingle  23865  fvsingle  23866  dfiota3  23869  brimage  23872  brimageg  23873  funimage  23874  fnimage  23875  imageval  23876  brcart  23878  brdomaing  23881  brrangeg  23882  brimg  23883  brapply  23884  brcup  23885  brcap  23886  brsuccf  23887  funpartfun  23888  funpartfv  23890  fullfunfv  23892  brrestrict  23894  dfrdg4  23895  tfrqfree  23896  altopelaltxp  23917  altxpsspw  23918  brsegle  24138  fvline  24174  liness  24175  ellines  24182  bpoly2  24199  bpoly3  24200  rankung  24203  ranksng  24204  rankelg  24205  rankpwg  24206  rankeq1o  24208  elhf2g  24213  hfext  24220  onsucconi  24283  tpssg  24330  fatesg  24354  eqvinopb  24363  copsexgb  24364  elo  24439  stcat  24442  splint  24446  domfldrefc  24455  ranfldrefc  24456  domrngref  24458  domintrefb  24461  restidsing  24474  prj1b  24477  prj3  24478  eloi  24484  elintabg  24488  domintrefc  24524  inttpemp  24538  mapmapmap  24547  injsurinj  24548  npincppr  24558  repcpwti  24560  cbcpcp  24561  cbicp  24565  prjmapcp2  24569  dstr  24570  iscst4  24576  islatalg  24582  domrancur1c  24601  mnlmxl2  24668  defse3  24671  inpc  24676  inposet  24677  tolat  24685  toplat  24689  dfdir2  24690  prodeq3ii  24707  fprodser  24719  symgfo  24767  svs2  24886  inttop2  24914  sallnei  24928  nsn  24929  dmhmph  24932  rnhmph  24933  intopcoaconlem3b  24937  intopcoaconlem3  24938  qusp  24941  efilcp  24951  fgsb2  24954  bwt2  24991  dmrngcmp  25150  dualded  25182  ishomd  25189  vtarsuelt  25294  fnctartar  25306  fnctartar2  25307  dfiunv2  25315  prismorcset2  25317  domcatfun  25324  codcatfun  25333  idcatfun  25340  empklst  25408  fnckle  25444  pfsubkl  25446  pgapspf2  25452  isconcl5a  25500  isconcl5ab  25501  bosser  25566  pdiveql  25567  abhp2  25574  bhp2a  25575  cnvresimaOLD  25625  trer  25626  finminlem  25630  gtinf  25633  fneer  25687  fnessref  25692  refssfne  25693  islocfin  25695  comppfsc  25706  neibastop1  25707  neibastop2lem  25708  neibastop3  25710  topmeet  25712  topjoin  25713  neifg  25719  tailfb  25725  filnetlem2  25727  filnetlem3  25728  filnetlem4  25729  cover2g  25758  f1opr  25790  inixp  25798  indexdom  25812  frinfm  25815  sdclem2  25851  sdclem1  25852  fdc  25854  isbndx  25905  prdstotbnd  25917  heibor1lem  25932  heiborlem1  25934  heiborlem3  25936  heiborlem4  25937  heiborlem5  25938  heiborlem6  25939  heiborlem8  25941  heiborlem10  25943  ismrer1  25961  riscer  26018  divrngidl  26052  intidl  26053  isfldidl  26092  ispridlc  26094  prtlem10  26132  prtlem13  26135  prtlem16  26136  prtlem19  26145  prter2  26148  prter3  26149  ralxpmap  26160  elrfi  26168  ismrcd1  26172  ismrcd2  26173  istopclsd  26174  ismrc  26175  mrefg2  26181  isnacs3  26184  mzpclall  26204  mzpincl  26211  mzpsubst  26225  mzpcompact2lem  26228  mzpcompact2  26229  eldioph2lem1  26238  eldioph2lem2  26239  eldiophss  26253  diophrex  26254  rexrabdioph  26274  2rexfrabdioph  26276  3rexfrabdioph  26277  4rexfrabdioph  26278  6rexfrabdioph  26279  7rexfrabdioph  26280  rabren3dioph  26297  fphpd  26298  rencldnfilem  26302  pellexlem5  26317  pellex  26319  rmxypairf1o  26395  monotuz  26425  monotoddzzfi  26426  oddcomabszz  26428  2nn0ind  26429  zindbi  26430  mzpcong  26458  rmydioph  26506  rmxdioph  26508  expdiophlem2  26514  setindtr  26516  setindtrs  26517  dford3lem2  26519  ttac  26528  pw2f1ocnv  26529  wepwsolem  26537  inisegn0  26539  dnnumch1  26540  fnwe2val  26545  fnwe2lem2  26547  aomclem1  26550  aomclem2  26551  aomclem6  26555  dfac11  26559  kelac2lem  26561  dfac21  26563  islssfg2  26568  lmhmlnmsplit  26584  pwssplit3  26589  filnm  26591  pwslnmlem1  26593  pwslnm  26595  dsmmval  26599  frlmlbs  26648  unxpwdom3  26655  enfixsn  26656  dfacbasgrp  26672  islindf4  26707  lmisfree  26711  lnr2i  26719  lnrfg  26722  hbtlem6  26732  rngunsnply  26777  pmtrfval  26792  symggen  26810  gsumcom3  26853  acsfn1p  26906  sdrgacs  26908  idomsubgmo  26913  fgraphxp  26929  expgrowth  26951  2sbc6g  27014  iotain  27016  compel  27039  ipo0  27051  ifr0  27052  fnchoice  27099  infrglb  27121  stoweidlem31  27179  stoweidlem57  27205  stoweidlem62  27210  stirlinglem13  27234  funressnfv  27364  dfdfat2  27369  csbafv12g  27377  tz6.12-afv  27412  csbaovg  27419  onfrALTlem5  27578  onfrALTlem4  27579  onfrALTlem3  27580  opelopab4  27588  a9e2nd  27595  trsspwALT  27860  trsspwALT2  27861  trsspwALT3  27862  pwtrVD  27866  pwtrOLD  27867  unipwrVD  27876  unipwr  27877  onfrALTlem5VD  27929  onfrALTlem4VD  27930  onfrALTlem3VD  27931  relopabVD  27945  a9e2ndVD  27952  sspwimp  27962  sspwimpVD  27963  sspwimpcf  27964  sspwimpcfVD  27965  sspwimpALT  27969  sspwimpALT2  27973  a9e2ndALT  27975  bnj23  28011  bnj62  28013  bnj156  28023  bnj219  28028  bnj610  28043  bnj918  28063  bnj927  28067  bnj976  28076  bnj1098  28082  bnj1379  28130  bnj110  28157  bnj98  28166  bnj154  28177  bnj155  28178  bnj535  28189  bnj556  28199  bnj557  28200  bnj581  28207  bnj591  28210  bnj594  28211  bnj580  28212  bnj607  28215  bnj609  28216  bnj600  28218  bnj849  28224  bnj893  28227  bnj908  28230  bnj934  28234  bnj944  28237  bnj964  28242  bnj966  28243  bnj969  28245  bnj970  28246  bnj910  28247  bnj986  28253  bnj999  28256  bnj1018  28261  bnj907  28264  bnj1039  28268  bnj1040  28269  bnj1052  28272  bnj1123  28283  bnj1030  28284  bnj1133  28286  bnj1128  28287  bnj1145  28290  bnj1204  28309  bnj1373  28327  bnj1417  28338  bnj1421  28339  bnj1498  28358  eqlkr2  28557  glbconxN  28834  pmapglbx  29225  pmapglb  29226  pclclN  29347  pclfinN  29356  polval2N  29362  pclfinclN  29406  osumcllem10N  29421  pexmidlem7N  29432  cdleme31sdnN  29843  cdlemefr44  29881  cdleme48fv  29955  cdleme46fvaw  29957  cdleme48bw  29958  cdleme46fsvlpq  29961  cdlemeg46fvcl  29962  cdlemeg49le  29967  cdlemeg46fjgN  29977  cdlemeg46fjv  29979  cdleme48d  29991  cdlemeg49lebilem  29995  cdleme50eq  29997  cdleme50f  29998  cdlemg2jlemOLDN  30049  cdlemg2klem  30051  cdlemk40  30373  cdlemk56  30427  diaglbN  30512  dvhlveclem  30565  dib1dim  30622  dibglbN  30623  diblss  30627  diblsmopel  30628  dicelvalN  30635  diclspsn  30651  cdlemn7  30660  dihordlem7  30671  dihopelvalcpre  30705  xihopellsmN  30711  dihopellsm  30712  dih1  30743  dihmeetlem1N  30747  dihglblem5apreN  30748  dihmeetlem2N  30756  dihglbcpreN  30757  dihmeetlem4preN  30763  dihmeetlem13N  30776  dih1dimatlem  30786  dihatlat  30791  dihjatcclem4  30878  lcdlss  31076
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-v 2791
  Copyright terms: Public domain W3C validator