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

Theorem vex 2743
Description: All set variables are sets (see isset 2744). 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 2256 . 2  |-  x  =  x
2 df-v 2742 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2363 . 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 2740
This theorem is referenced by:  isset  2744  ralv  2753  rexv  2754  reuv  2755  rabab  2756  sbhypf  2784  ceqex  2849  ralab  2877  rexab  2879  moeq3  2893  mo2icl  2895  reu8  2914  sbc2or  2943  csbvarg  3050  csbiebg  3062  sbcnestgf  3070  sbnfc2  3083  ddif  3250  csbing  3318  dfun2  3346  dfin2  3347  vn0  3404  eqv  3412  abvor0  3414  sbss  3505  csbifg  3534  ifexg  3565  elpwg  3573  dftp2  3620  prnzg  3687  snssg  3695  difprsn  3697  sneqrg  3723  preq12bg  3732  pwpr  3764  pwtp  3765  pwv  3767  unipr  3782  uniprg  3783  unisng  3785  elintg  3811  elintrabg  3816  intss1  3818  ssint  3819  intmin  3823  intss  3824  intssuni  3825  intmin4  3832  intab  3833  intun  3835  intpr  3836  intprg  3837  uniintsn  3840  iinconst  3855  iuniin  3856  iinss1  3858  dfiin2g  3877  ssiinf  3892  iinss  3894  iinss2  3895  0iin  3901  iinab  3904  iinun2  3909  iundif2  3910  iindif2  3912  iinin2  3913  iinuni  3926  sspwuni  3928  iinpw  3931  iunpwss  3932  brab1  4008  csbopabg  4034  mptv  4052  trint  4068  trintss  4069  vprc  4092  inex1g  4097  ssexg  4100  intex  4109  inuni  4115  axpweq  4125  pwexg  4132  pwuni  4144  axpr  4151  zfpair2  4153  elALT  4156  rext  4160  sspwb  4161  unipw  4162  ssextss  4165  nnullss  4172  exss  4173  opth  4182  opthg  4183  copsexg  4189  copsex4g  4192  moop2  4198  euotd  4204  opelopabsbOLD  4210  opelopabsb  4212  pwin  4234  pwunss  4235  pwssun  4236  pwundifOLD  4238  epelg  4243  epel  4245  dfid3  4247  pofun  4267  epse  4313  wefrc  4324  tron  4352  onfr  4368  sucel  4402  suctr  4412  uniexg  4454  unexb  4457  snnex  4461  uniuni  4464  eusvnf  4466  eusvnfb  4467  reusv6OLD  4482  iunpw  4507  onint  4523  ordpwsuc  4543  unon  4559  ordunisuc  4560  onuninsuci  4568  orduninsuc  4571  limsssuc  4578  limuni3  4580  tfinds  4587  tfindsg  4588  tfindsg2  4589  tfinds2  4591  dfom2  4595  peano5  4616  finds  4619  findsg  4620  finds2  4621  0nelxp  4670  opelxp  4672  opeliunxp  4693  elvv  4701  elvvv  4702  elvvuni  4703  xpsspw  4750  xpsspwOLD  4751  relopabi  4764  opabid2  4768  difopab  4770  xpiindi  4774  ralxpf  4783  relop  4787  cnvco  4818  dfrn2  4821  dfdm4  4825  dmss  4831  dmin  4839  dmiun  4840  dmuni  4841  dm0  4845  dmi  4846  reldm0  4849  elreldm  4856  elrnmpt1  4881  dmrnssfld  4891  dmcoss  4897  dmcosseq  4899  opelresg  4915  resieq  4918  dmres  4929  elres  4943  relssres  4945  resopab  4949  resiexg  4950  iss  4951  dfres2  4955  dfima2  4967  csbima12g  4975  imadmrn  4977  imai  4980  elimasng  4992  args  4994  epini  4996  iniseg  4997  dffr3  4998  dfse2  4999  exse2  5000  cotr  5008  issref  5009  cnvsym  5010  intasym  5011  asymref  5012  asymref2  5013  intirr  5014  brcodir  5015  codir  5016  qfto  5017  poirr2  5020  cnvopab  5036  cnv0  5037  cnvi  5038  cnvdif  5040  rniun  5044  dminss  5048  imainss  5049  ssrnres  5069  rninxp  5070  dminxp  5071  cnvcnv3  5076  dfrel2  5077  dmsnn0  5090  dmsnopg  5096  cnvcnvsn  5102  dmsnsnsn  5103  cnvsng  5110  elxp4  5112  elxp5  5113  cnvresima  5114  dfco2  5124  dfco2a  5125  cores  5128  resco  5129  imaco  5130  rnco  5131  coiun  5134  co02  5138  coi1  5140  coass  5143  relssdmrn  5145  unielrel  5149  unixp0  5158  ressn  5163  cnviin  5164  cnvpo  5165  cnvso  5166  dffun2  5169  dffun7  5184  dffun8  5185  dffun9  5186  funopg  5190  funssres  5197  funun  5199  funcnvsn  5200  funcnv2  5212  funcnv  5213  funcnv3  5214  fun2cnv  5215  funcnvuni  5220  imadif  5230  isarep1  5234  2elresin  5258  fnres  5263  fcnvres  5321  fabexg  5325  fconstg  5331  fun11iun  5396  f1osng  5417  fv2  5419  fvprc  5420  fvex  5437  fv3  5439  nfunsn  5457  funimass4  5472  ssimaexg  5484  dffv2  5491  dmfco  5492  fvopab6  5520  fndmdif  5528  iinpreima  5554  fvelrn  5560  dff3  5572  dffo4  5575  exfo  5577  f1ompt  5581  fmptco  5590  fsng  5596  dfmpt  5600  fnressn  5604  fressnfv  5606  fvsng  5613  zfrep6  5647  funfvima3  5654  idref  5658  fvclss  5659  fvresex  5661  abrexco  5665  opabex3  5668  imaiun  5670  dff13  5682  foeqcnvco  5703  f1eqcocnv  5704  fliftcnv  5709  isocnv2  5727  isomin  5733  isoini  5734  isofr  5738  isose  5739  f1oweALT  5750  wemoiso  5754  wemoiso2  5755  knatar  5756  oprabid  5781  csbovg  5788  eloprabga  5833  mpt2v  5836  caovmo  5956  f1opw  5971  ofmres  6015  op1stg  6031  op2ndg  6032  1stval2  6036  2ndval2  6037  fo1st  6038  fo2nd  6039  f1stres  6040  f2ndres  6041  fo1stres  6042  fo2ndres  6043  1st2val  6044  2nd2val  6045  xp1st  6048  xp2nd  6049  sbcopeq1a  6071  csbopeq1a  6072  eloprabi  6085  mpt2mptsx  6086  dmmpt2ssx  6088  fmpt2x  6089  ovmptss  6099  fmpt2co  6101  df1st2  6104  df2nd2  6105  1stconst  6106  2ndconst  6107  curry1  6109  curry2  6112  fparlem1  6117  fparlem2  6118  fpar  6121  fsplit  6122  frxp  6124  xporderlem  6125  soxp  6127  fnwelem  6129  fnse  6131  reldmtpos  6141  dmtpos  6145  rntpos  6146  ovtpos  6148  dftpos3  6151  dftpos4  6152  tpostpos  6153  porpss  6180  sorpss  6181  sorpsscmpl  6187  uniabio  6200  iotaval  6201  sniota  6217  opiota  6221  opabiotafun  6222  opabiota  6224  riotav  6242  csbriotag  6250  onovuni  6292  smogt  6317  tfrlem3  6326  tfrlem8  6333  tfrlem9a  6335  tfrlem16  6342  tz7.44lem1  6351  rdg0g  6373  rdglim2  6378  tz7.48-1  6388  seqomlem1  6395  seqomlem2  6396  abianfplem  6403  oacl  6467  omcl  6468  oecl  6469  oa0r  6470  om0r  6471  om1r  6474  oe1m  6476  oaordi  6477  oawordri  6481  oawordeulem  6485  oalimcl  6491  oaass  6492  oarec  6493  omordi  6497  omwordri  6503  omlimcl  6509  odi  6510  omass  6511  omeulem1  6513  oen0  6517  oeordi  6518  oewordri  6523  oeworde  6524  oeoalem  6527  oeoelem  6529  nnawordex  6568  omabs  6578  omsmolem  6584  ercnv  6614  iserd  6619  eqerlem  6625  eqer  6626  ecdmn0  6635  erth  6637  erdisj  6640  qsss  6653  ecid  6657  qsid  6658  iiner  6664  qsel  6671  erovlem  6687  ecopovsym  6693  ecopovtrn  6694  ecopover  6695  mapprc  6709  fnmap  6712  fnpm  6713  mapval2  6730  pmsspw  6735  mapsn  6742  mapsncnv  6747  ixpconstg  6758  ixpprc  6770  uniixp  6772  ixpin  6774  ixpiin  6775  resixpfo  6787  elixpsn  6788  ixpsnf1o  6789  boxriin  6791  boxcutc  6792  bren  6804  brdomg  6805  domen  6808  domeng  6809  idssen  6839  ener  6841  domtr  6847  ensn1g  6859  en1  6861  en1b  6862  fundmen  6867  fundmeng  6868  mapsnen  6871  unen  6876  domdifsn  6878  xpsnen  6879  xpsneng  6880  xpcomeng  6887  xpassen  6889  xpdom2  6890  xpdom2g  6891  domunsncan  6895  omxpenlem  6896  pw2f1o  6900  fopwdom  6903  sbthlem10  6913  sbth  6914  sbthcl  6916  domunsn  6944  fodomr  6945  pwdom  6946  canth2  6947  canth2g  6948  domssex  6955  xpf1o  6956  mapen  6958  mapunen  6963  map2xp  6964  mapdom2  6965  mapdom3  6966  ssenen  6968  infensuc  6972  nneneq  6977  php  6978  php2  6979  php3  6980  sucdom2  6990  1sdom  6998  unxpdomlem2  7001  unxpdomlem3  7002  isinf  7009  fineqvlem  7010  fineqv  7011  pssnn  7014  ssfi  7016  dif1enOLD  7023  dif1en  7024  findcard  7030  findcard2  7031  findcard2s  7032  ac6sfi  7034  frfi  7035  fimax2g  7036  unbnn2  7047  isfinite2  7048  xpfi  7061  domunfican  7062  fiint  7066  fodomfi  7068  fodomfib  7069  iunfi  7077  pwfilem  7083  ixpfi2  7087  fissuni  7093  fipreima  7094  finsschain  7095  fival  7099  ssfii  7105  fi0  7106  fiin  7108  dffi2  7109  fipwuni  7112  fisn  7113  elfiun  7116  dffi3  7117  fifo  7118  marypha1lem  7119  dfsup2  7128  dfsup2OLD  7129  ordiso2  7163  oismo  7188  hartogslem1  7190  hartogs  7192  wofib  7193  wemappo  7197  wemapso2lem  7198  card2on  7201  brwdom  7214  brwdomn0  7216  brwdom2  7220  wdomtr  7222  wdompwdom  7225  canthwdom  7226  xpwdomg  7232  unxpwdom2  7235  ixpiunwdom  7238  elirrv  7244  zfregfr  7249  inf0  7255  inf3lema  7258  inf3lemd  7261  inf3lem1  7262  inf3lem2  7263  inf3lem3  7264  inf3lem5  7266  inf3lem6  7267  inf3lem7  7268  inf3  7269  infeq5  7271  omex  7277  dfom3  7281  dfom5  7284  infdifsn  7290  cantnfdm  7298  cantnfval  7302  cantnfval2  7303  cantnflt  7306  cantnff  7308  oemapso  7317  cantnflem1  7324  wemapwe  7333  cnfcom  7336  cnfcom3clem  7341  epfrs  7346  tcvalg  7356  tctr  7358  tcmin  7359  r1sdom  7379  r1val1  7391  tz9.12lem1  7392  tz9.12lem3  7394  tz9.13  7396  tz9.13g  7397  rankf  7399  unir1  7418  rankvalg  7422  rankonidlem  7433  r1val2  7442  bndrank  7446  ranklim  7449  r1pwOLD  7451  rankunb  7455  rankuni2b  7458  rankuni  7468  rankval4  7472  rankxplim  7482  rankxplim3  7484  rankxpsuc  7485  tcrank  7487  cp  7494  bnd2  7496  kardex  7497  karden  7498  cardf2  7509  tskwe  7516  cardlim  7538  harcard  7544  cardiun  7548  pm54.43  7566  r0weon  7573  infxpenlem  7574  infxpenc2lem2  7580  fseqenlem1  7584  fseqenlem2  7585  fseqen  7587  dfac8alem  7589  dfac8clem  7592  ac10ct  7594  ween  7595  acnlem  7608  finacn  7610  acndom  7611  acndom2  7614  wdomfil  7621  infpwfien  7622  alephon  7629  alephcard  7630  alephordi  7634  cardaleph  7649  alephval3  7670  iunfictbso  7674  aceq3lem  7680  dfac3  7681  dfac4  7682  dfac5lem1  7683  dfac5lem2  7684  dfac5lem3  7685  dfac5lem4  7686  dfac5lem5  7687  dfac5  7688  dfac2a  7689  dfac2  7690  dfac8  7694  dfac9  7695  dfac10b  7698  acacni  7699  dfacacn  7700  dfac13  7701  kmlem1  7709  kmlem2  7710  kmlem9  7717  kmlem10  7718  kmlem11  7719  kmlem12  7720  kmlem13  7721  cdafn  7728  pwsdompw  7763  infmap2  7777  ackbij1lem5  7783  ackbij1lem8  7786  ackbij2lem3  7800  ackbij2  7802  cflm  7809  cardcf  7811  cfeq0  7815  cfsuc  7816  cff1  7817  cfflb  7818  cfval2  7819  cflim2  7822  cfss  7824  cfslb2n  7827  cofsmo  7828  cfsmolem  7829  cfcoflem  7831  coftr  7832  sornom  7836  infpssr  7867  fin4en1  7868  fin23lem11  7876  enfin2i  7880  fin23lem26  7884  fin23lem14  7892  fin23lem16  7894  fin23lem17  7897  fin23lem21  7898  fin23lem32  7903  fin23lem34  7905  fin23lem39  7909  compsscnvlem  7929  compssiso  7933  isf34lem4  7936  enfin1ai  7943  isfin1-3  7945  fin67  7954  dffin7-2  7957  fin1a2lem7  7965  fin1a2lem10  7968  fin1a2lem12  7970  fin1a2lem13  7971  fin12  7972  itunitc1  7979  itunitc  7980  ituniiun  7981  hsmexlem2  7986  hsmexlem4  7988  hsmex  7991  axcc2lem  7995  axcc3  7997  acncc  7999  fin41  8003  dominf  8004  dcomex  8006  axdc2lem  8007  axdc3lem  8009  axdc3lem2  8010  axdc3lem4  8012  axdc4lem  8014  axcclem  8016  ac9  8043  ac6s  8044  ac6sg  8048  ac9s  8053  numthcor  8054  zorn2lem1  8056  zorn2lem4  8059  zorn2lem7  8062  zorng  8064  zornn0g  8065  ttukeylem5  8073  ttukeylem6  8074  ttukeylem7  8075  axdclem  8079  axdclem2  8080  fodomg  8083  fodomb  8084  brdom3  8086  brdom5  8087  brdom4  8088  brdom7disj  8089  brdom6disj  8090  iunfo  8094  ondomon  8118  cardmin  8119  alephval2  8127  dominfac  8128  fpwwe2lem1  8186  fpwwe2lem8  8192  fpwwe2lem11  8195  fpwwe2lem12  8196  fpwwe2lem13  8197  fpwwe2  8198  fpwwe  8201  canthwe  8206  canthp1lem1  8207  pwfseqlem1  8213  pwfseqlem2  8214  pwfseqlem3  8215  pwfseqlem4a  8216  pwfseqlem5  8218  pwxpndom2  8220  gchac  8228  gch2  8234  inawinalem  8244  winainflem  8248  winalim2  8251  winafp  8252  gchina  8254  wunfi  8276  intwun  8290  wunex2  8293  uniwun  8295  eltsk2g  8306  inttsk  8329  inar1  8330  rankcf  8332  tskcard  8336  tskuni  8338  gruun  8361  intgru  8369  ingru  8370  wfgru  8371  grudomon  8372  gruina  8373  grur1a  8374  grur1  8375  grutsk  8377  axgroth5  8379  axgroth2  8380  grothpw  8381  grothpwex  8382  axgroth6  8383  grothomex  8384  grothac  8385  axgroth3  8386  grothprim  8389  grothtsk  8390  inaprc  8391  nqereu  8486  nqerf  8487  dmrecnq  8525  ltaddnq  8531  genpnnp  8562  genpnmax  8564  genpcl  8565  nqpr  8571  addclprlem1  8573  mulclprlem  8576  distrlem4pr  8583  1idpr  8586  prlem934  8590  ltaddpr  8591  ltexprlem3  8595  ltexprlem4  8596  ltexprlem6  8598  ltexprlem7  8599  prlem936  8604  reclem2pr  8605  reclem3pr  8606  mulasssr  8645  ltsosr  8649  0idsr  8652  1idsr  8653  ltasr  8655  recexsrlem  8658  mulgt0sr  8660  supsrlem  8666  ltresr  8695  axmulass  8712  axrrecex  8718  axpre-lttri  8720  wuncn  8725  renfdisj  8818  wloglei  9238  lbinfm  9640  supmul1  9652  supmullem1  9653  supmullem2  9654  supmul  9655  dfinfmr  9664  infmsup  9665  infmrgelb  9667  infmrlb  9668  dfnn2  9692  dflt2  10414  xrinfmss2  10560  infmxrgelb  10584  xrinfm0  10586  fzpr  10771  uzrdgfni  10952  axdc4uzlem  10975  axdc4uz  10976  seqval  10988  seqfeq4  11026  serle  11032  seqof  11034  hashxplem  11315  hashmap  11317  hashpw  11318  hashfun  11319  hashbclem  11320  hashfacen  11322  hashf1lem1  11323  hashf1lem2  11324  hashf1  11325  fz1isolem  11329  ccatfn  11357  wrdexb  11379  wrdind  11407  shftfval  11495  shftfib  11497  shftfn  11498  2shfti  11505  sqrlem6  11663  rexfiuz  11761  rlimdm  11955  fclim  11957  climshft  11980  fsum2dlem  12163  fsumcom2  12167  fsum0diag2  12175  fsumabs  12189  fsumrlim  12199  fsumo1  12200  fsumiun  12209  isumltss  12234  supcvg  12241  xpnnenOLD  12415  rpnnen2lem11  12430  algrf  12670  isprm2lem  12692  isprm2  12693  prmind2  12696  iserodd  12815  4sqlem12  12930  vdwmc  12952  vdwlem10  12964  vdwlem13  12967  ramtlecl  12974  hashbc0  12979  ramval  12982  ramcl2lem  12983  ramub2  12988  0ram  12994  ram0  12996  ramub1lem1  13000  ramub1lem2  13001  ramub1  13002  restfn  13256  elrest  13259  restsspw  13263  prdsval  13282  prdsle  13288  prdsless  13289  prdsleval  13303  pwsle  13318  imasaddfnlem  13357  imasvscafn  13366  imasleval  13370  xpsc0  13389  xpsc1  13390  xpsfrnel2  13394  ismre  13419  fnmre  13420  ismred  13431  mremre  13433  fnmrc  13436  mrcfval  13437  mrisval  13459  mreexexlem4d  13476  isacs2  13482  mreacs  13487  acsfn  13488  acsfn1  13490  acsfn2  13492  cidffn  13507  comfeq  13536  invsym2  13592  oppcsect2  13604  brssc  13618  sscpwex  13619  isssc  13624  issubc  13639  isfuncd  13666  cofucl  13689  funcres2b  13698  funcpropd  13701  setcmon  13846  catcval  13855  fnxpc  13877  xpcval  13878  xpccatid  13889  curf2ndf  13948  drsdirfi  13999  isdrs2  14000  clatl  14147  odupos  14166  oduposb  14167  oduglb  14170  odulub  14172  posglbd  14180  ipoval  14184  ipolerval  14186  fpwipodrs  14194  ipodrsima  14195  isacs5lem  14199  psdmrn  14243  psssdm2  14251  submacs  14369  pwsdiagmhm  14372  gsumwspan  14395  mulgpropd  14527  subgacs  14579  nsgacs  14580  eqgfval  14592  eqgval  14593  gicsubgen  14669  gaid  14680  gaorb  14688  orbsta  14694  symgval  14698  symgbas  14699  symgplusg  14703  sylow1lem2  14837  sylow2alem1  14855  sylow2alem2  14856  sylow2a  14857  sylow2blem1  14858  sylow2blem2  14859  sylow2blem3  14860  sylow3lem1  14865  sylow3lem3  14867  sylow3lem6  14870  efgval  14953  efgval2  14960  efgrelexlemb  14986  efgcpbllema  14990  efgcpbllemb  14991  vrgpfval  15002  frgpuplem  15008  divsabl  15084  frgpnabllem1  15088  gsumval3  15118  gsumzaddlem  15130  gsumzadd  15131  gsum2d  15150  gsum2d2  15152  gsumcom2  15153  gsumxp  15154  dprdfadd  15182  dprdres  15190  subgdmdprd  15196  dprd2dlem1  15203  dprd2d2  15206  ablfac1eulem  15234  pgpfac1lem5  15241  opprsubg  15345  subrgmre  15496  subsubrg2  15499  subrgpropd  15506  lss1d  15647  lssintcl  15648  lssmre  15650  lssacs  15651  pwsdiaglmhm  15741  islbs3  15835  lbsextlem4  15841  drngnidl  15908  lidldvgen  15934  psrbaglefi  16045  mplcoe1  16136  mplcoe2  16138  ltbval  16140  ltbwe  16141  opsrle  16144  opsrtoslem1  16152  opsrtoslem2  16153  evlslem4  16172  coe1mul2  16273  coe1tm  16276  znleval  16435  cssmre  16520  thlle  16524  pjfval2  16536  istopon  16590  tgval2  16621  bastg  16631  tgdom  16643  distop  16660  indistopon  16665  fctop  16668  cctop  16670  ppttop  16671  epttop  16673  fncld  16686  cldss2  16694  ntreq0  16741  discld  16753  mretopd  16756  toponmre  16757  neisspw  16771  opnnei  16784  tgrest  16817  resttopon  16819  restco  16822  restdis  16836  ordtbas2  16848  ordtcnv  16858  ordtrest2  16861  pnfnei  16877  mnfnei  16878  iscnp2  16896  subbascn  16911  cnntr  16931  cnrest2  16941  cnpresti  16943  cnprest  16944  cnprest2  16945  ist1-3  17004  hausnei2  17008  isnrm2  17013  dishaus  17037  cmpcovf  17045  fincmp  17047  cmpsublem  17053  cmpsub  17054  cmpcld  17056  uncmp  17057  fiuncmp  17058  hauscmplem  17060  cmpfi  17062  dfcon2  17072  consuba  17073  cnconn  17075  uncon  17082  t1conperf  17089  is1stc2  17095  1stcfb  17098  2ndcsb  17102  2ndc1stc  17104  1stcrest  17106  2ndcctbss  17108  2ndcdisj  17109  2ndcomap  17111  2ndcsep  17112  dis2ndc  17113  llyi  17127  nllyi  17128  nlly2i  17129  llynlly  17130  subislly  17134  restnlly  17135  restlly  17136  islly2  17137  llyrest  17138  llyidm  17141  nllyidm  17142  hausllycmp  17147  cldllycmp  17148  lly1stc  17149  dislly  17150  hausmapdom  17153  kgenf  17163  iskgen3  17171  llycmpkgen2  17172  1stckgenlem  17175  1stckgen  17176  kgencn2  17179  txuni2  17187  txbas  17189  eltx  17190  ptpjpre1  17193  ptuni2  17198  ptpjcn  17232  ptpjopn  17233  ptclsg  17236  dfac14  17239  xkoccn  17240  txcnp  17241  txcnmpt  17245  prdstopn  17249  txrest  17252  txdis  17253  txindis  17255  txdis1cn  17256  txlly  17257  txnlly  17258  pthaus  17259  txcmplem1  17262  txcmplem2  17263  hausdiag  17266  txlm  17269  tx1stc  17271  tx2ndc  17272  txkgen  17273  xkopt  17276  xkococnlem  17280  xkococn  17281  cnmpt1st  17289  cnmpt2nd  17290  xkofvcn  17305  xkoinjcn  17308  txcon  17310  qtoptop2  17317  qtopuni  17320  basqtop  17329  tgqtop  17330  hmphdis  17414  indishmph  17416  txhmeo  17421  pt1hmeo  17424  ptuncnv  17425  ptunhmeo  17426  xpstopnlem1  17427  ptcmpfi  17431  xkohmeo  17433  isfbas  17451  isfbas2  17457  fbssfi  17459  trfbas2  17465  isfild  17480  snfil  17486  elfg  17493  fgcl  17500  filcon  17505  fbasrn  17506  filuni  17507  trfil2  17509  cfinfil  17515  csdfil  17516  supfil  17517  zfbas  17518  isufil2  17530  filssufilg  17533  acufl  17539  filufint  17542  uffix  17543  ufinffr  17551  ufildr  17553  fin1aufil  17554  rnelfmlem  17574  rnelfm  17575  fmfnfmlem3  17578  fmfnfmlem4  17579  fmfnfm  17580  ufldom  17584  flimrest  17605  hauspwpwf1  17609  txflf  17628  fclsrest  17646  fclscmp  17652  alexsubb  17667  alexsubALTlem1  17668  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALTlem4  17671  alexsubALT  17672  ptcmplem2  17674  ptcmplem3  17675  ptcmplem4  17676  ptcmplem5  17677  tmdgsum  17705  symgtgp  17711  cldsubg  17720  tgpconcomp  17722  divstgplem  17730  divstgphaus  17732  prdstmdd  17733  tsmsval2  17739  tsmssubm  17752  imasdsf1olem  17864  xpsdsval  17872  xmetec  17907  prdsbl  17964  stdbdxmet  17988  met1stc  17994  prdsxmslem2  18002  dscopn  18023  xrtgioo  18239  xrsblre  18244  icccmplem1  18254  icccmplem2  18255  fsumcn  18301  fsum2cn  18302  cnllycmp  18381  isphtpc  18419  pi1blem  18464  iscmet3  18646  metcld2  18659  bcthlem4  18676  minveclem3b  18719  ovolfiniun  18787  ovoliunlem1  18788  ovoliunlem2  18789  finiunmbl  18828  volfiniun  18831  iundisj2  18833  uniioombllem3  18867  vitalilem2  18891  vitalilem3  18892  vitali  18895  mbfimaopnlem  18937  itg1addlem4  18981  mbfi1fseqlem4  19000  mbfi1fseqlem6  19002  itgfsum  19108  ellimc2  19154  limcflf  19158  perfdvf  19180  dvres  19188  dvres2  19189  dvnff  19199  dvcj  19226  dvrec  19231  dvmptfsum  19249  dvef  19254  rolle  19264  dvivthlem1  19282  dvfsumle  19295  dvfsumabs  19297  dvfsumlem2  19301  dvfsumlem3  19302  ftc1cn  19317  mpfind  19355  pf1ind  19365  vieta1lem2  19618  elqaalem2  19627  ulmdv  19707  logfac  19881  xrlimcnp  20190  jensenlem1  20208  jensenlem2  20209  jensen  20210  wilthlem2  20234  prmorcht  20343  lgsquadlem1  20520  lgsquadlem2  20521  dchrisumlema  20564  dchrisumlem3  20567  ex-natded9.26  20759  nvss  21074  vsfval  21116  h2hlm  21485  axhcompl-zf  21503  hlim2  21696  hhcmpl  21704  hhcms  21707  shex  21716  isch2  21728  helch  21748  hhsscms  21781  occl  21808  chintcli  21835  dfch2  21911  spanuni  22048  spansni  22061  elnlfn  22433  nmopun  22519  nlelchi  22566  cnlnssadj  22585  adjbd1o  22590  branmfn  22610  pjnmopi  22653  hmopidmchi  22656  abrexss  22966  ballotlem2  22973  ballotlemsf1o  22998  ballotlemirc  23016  dmgmseqn0  23033  derangenlem  23039  subfacp1lem1  23047  subfacp1lem3  23050  subfacp1lem4  23051  subfacp1lem5  23052  erdszelem7  23065  erdszelem8  23066  erdsze2lem2  23072  kur14lem9  23082  ptpcon  23101  indispcon  23102  conpcon  23103  cnllyscon  23113  rellyscon  23119  cvmsss2  23142  cvmcov2  23143  cvmliftlem15  23166  cvmlift2lem1  23170  cvmlift2lem12  23182  umgraex  23212  eupath  23242  ghomgrplem  23333  relexpindlem  23373  rtrclreclem.trans  23380  dfrtrcl2  23382  untsucf  23393  dftr6  23443  coepr  23445  dffr5  23446  dfso2  23447  dfpo2  23448  br8  23449  br6  23450  br4  23451  dfres3  23452  cnvco1  23453  cnvco2  23454  fundmpss  23456  fprb  23463  dfdm5  23466  dfrn5  23467  setinds  23468  dfon2lem1  23473  dfon2lem3  23475  dfon2lem6  23478  dfon2lem7  23479  dfon2lem8  23480  dfon2  23482  rdgprc  23485  dfrdg2  23486  predreseq  23513  predpo  23518  predbrg  23520  setlikespec  23521  predep  23526  preddowncl  23530  preduz  23534  predfz  23537  tz6.26  23539  trpredrec  23575  poseq  23587  soseq  23588  wfrlem5  23594  wfrlem10  23599  wfrlem12  23601  wfrlem13  23602  wfrlem14  23603  wfrlem16  23605  tfrALTlem  23610  frrlem5  23619  frrlem11  23627  axsltsolem1  23655  axfelem18  23697  axfelem22  23701  txpss3v  23759  brtxp  23761  brtxp2  23762  pprodss4v  23765  brpprod  23766  brpprod3a  23767  brpprod3b  23768  brsset  23770  idsset  23771  dfon3  23773  brtxpsd  23775  brbigcup  23779  dfbigcup2  23780  fobigcup  23781  elfix  23784  elfix2  23785  dffix2  23786  fixcnv  23789  limitssson  23792  dfom5b  23793  elfuns  23794  elfunsg  23795  elsingles  23797  fnsingle  23798  fvsingle  23799  dfiota3  23802  brimage  23805  brimageg  23806  funimage  23807  fnimage  23808  imageval  23809  brcart  23811  brdomaing  23814  brrangeg  23815  brimg  23816  brapply  23817  brcup  23818  brcap  23819  brsuccf  23820  funpartfun  23821  funpartfv  23823  fullfunfv  23825  brrestrict  23827  dfrdg4  23828  tfrqfree  23829  altopelaltxp  23850  altxpsspw  23851  brsegle  24071  fvline  24107  liness  24108  ellines  24115  bpoly2  24132  bpoly3  24133  rankung  24136  ranksng  24137  rankelg  24138  rankpwg  24139  rankeq1o  24141  elhf2g  24146  hfext  24153  onsucconi  24216  tpssg  24263  fatesg  24287  eqvinopb  24296  copsexgb  24297  elo  24372  stcat  24375  splint  24379  domfldrefc  24388  ranfldrefc  24389  domrngref  24391  domintrefb  24394  restidsing  24407  prj1b  24410  prj3  24411  eloi  24417  elintabg  24421  domintrefc  24457  inttpemp  24471  mapmapmap  24480  injsurinj  24481  npincppr  24491  repcpwti  24493  cbcpcp  24494  cbicp  24498  prjmapcp2  24502  dstr  24503  iscst4  24509  islatalg  24515  domrancur1c  24534  mnlmxl2  24601  defse3  24604  inpc  24609  inposet  24610  tolat  24618  toplat  24622  dfdir2  24623  prodeq3ii  24640  fprodser  24652  symgfo  24700  svs2  24819  inttop2  24847  sallnei  24861  nsn  24862  dmhmph  24865  rnhmph  24866  intopcoaconlem3b  24870  intopcoaconlem3  24871  qusp  24874  efilcp  24884  fgsb2  24887  bwt2  24924  dmrngcmp  25083  dualded  25115  ishomd  25122  vtarsuelt  25227  fnctartar  25239  fnctartar2  25240  dfiunv2  25248  prismorcset2  25250  domcatfun  25257  codcatfun  25266  idcatfun  25273  empklst  25341  fnckle  25377  pfsubkl  25379  pgapspf2  25385  isconcl5a  25433  isconcl5ab  25434  bosser  25499  pdiveql  25500  abhp2  25507  bhp2a  25508  cnvresimaOLD  25558  trer  25559  finminlem  25563  gtinf  25566  fneer  25620  fnessref  25625  refssfne  25626  islocfin  25628  comppfsc  25639  neibastop1  25640  neibastop2lem  25641  neibastop3  25643  topmeet  25645  topjoin  25646  neifg  25652  tailfb  25658  filnetlem2  25660  filnetlem3  25661  filnetlem4  25662  cover2g  25691  f1opr  25723  inixp  25731  indexdom  25745  frinfm  25748  sdclem2  25784  sdclem1  25785  fdc  25787  isbndx  25838  prdstotbnd  25850  heibor1lem  25865  heiborlem1  25867  heiborlem3  25869  heiborlem4  25870  heiborlem5  25871  heiborlem6  25872  heiborlem8  25874  heiborlem10  25876  ismrer1  25894  riscer  25951  divrngidl  25985  intidl  25986  isfldidl  26025  ispridlc  26027  prtlem10  26065  prtlem13  26068  prtlem16  26069  prtlem19  26078  prter2  26081  prter3  26082  ralxpmap  26093  elrfi  26101  ismrcd1  26105  ismrcd2  26106  istopclsd  26107  ismrc  26108  mrefg2  26114  isnacs3  26117  mzpclall  26137  mzpincl  26144  mzpsubst  26158  mzpcompact2lem  26161  mzpcompact2  26162  eldioph2lem1  26171  eldioph2lem2  26172  eldiophss  26186  diophrex  26187  rexrabdioph  26207  2rexfrabdioph  26209  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  rabren3dioph  26230  fphpd  26231  rencldnfilem  26235  pellexlem5  26250  pellex  26252  rmxypairf1o  26328  monotuz  26358  monotoddzzfi  26359  oddcomabszz  26361  2nn0ind  26362  zindbi  26363  mzpcong  26391  rmydioph  26439  rmxdioph  26441  expdiophlem2  26447  setindtr  26449  setindtrs  26450  dford3lem2  26452  ttac  26461  pw2f1ocnv  26462  wepwsolem  26470  inisegn0  26472  dnnumch1  26473  fnwe2val  26478  fnwe2lem2  26480  aomclem1  26483  aomclem2  26484  aomclem6  26488  dfac11  26492  kelac2lem  26494  dfac21  26496  islssfg2  26501  lmhmlnmsplit  26517  pwssplit3  26522  filnm  26524  pwslnmlem1  26526  pwslnm  26528  dsmmval  26532  frlmlbs  26581  unxpwdom3  26588  enfixsn  26589  dfacbasgrp  26605  islindf4  26640  lmisfree  26644  lnr2i  26652  lnrfg  26655  hbtlem6  26665  rngunsnply  26710  pmtrfval  26725  symggen  26743  gsumcom3  26786  acsfn1p  26839  sdrgacs  26841  idomsubgmo  26846  fgraphxp  26862  expgrowth  26884  2sbc6g  26948  iotain  26950  compel  26973  ipo0  26985  ifr0  26986  fnchoice  27033  stoweidlem31  27080  stoweidlem57  27106  stoweidlem62  27111  onfrALTlem5  27323  onfrALTlem4  27324  onfrALTlem3  27325  opelopab4  27333  a9e2nd  27340  trsspwALT  27605  trsspwALT2  27606  trsspwALT3  27607  pwtrVD  27611  pwtrOLD  27612  unipwrVD  27621  unipwr  27622  onfrALTlem5VD  27674  onfrALTlem4VD  27675  onfrALTlem3VD  27676  relopabVD  27690  a9e2ndVD  27697  sspwimp  27707  sspwimpVD  27708  sspwimpcf  27709  sspwimpcfVD  27710  sspwimpALT  27714  sspwimpALT2  27718  a9e2ndALT  27720  bnj23  27756  bnj62  27758  bnj156  27768  bnj219  27773  bnj610  27788  bnj918  27808  bnj927  27812  bnj976  27821  bnj1098  27827  bnj1379  27875  bnj110  27902  bnj98  27911  bnj154  27922  bnj155  27923  bnj535  27934  bnj556  27944  bnj557  27945  bnj581  27952  bnj591  27955  bnj594  27956  bnj580  27957  bnj607  27960  bnj609  27961  bnj600  27963  bnj849  27969  bnj893  27972  bnj908  27975  bnj934  27979  bnj944  27982  bnj964  27987  bnj966  27988  bnj969  27990  bnj970  27991  bnj910  27992  bnj986  27998  bnj999  28001  bnj1018  28006  bnj907  28009  bnj1039  28013  bnj1040  28014  bnj1052  28017  bnj1123  28028  bnj1030  28029  bnj1133  28031  bnj1128  28032  bnj1145  28035  bnj1204  28054  bnj1373  28072  bnj1417  28083  bnj1421  28084  bnj1498  28103  eqlkr2  28420  glbconxN  28697  pmapglbx  29088  pmapglb  29089  pclclN  29210  pclfinN  29219  polval2N  29225  pclfinclN  29269  osumcllem10N  29284  pexmidlem7N  29295  cdleme31sdnN  29706  cdlemefr44  29744  cdleme48fv  29818  cdleme46fvaw  29820  cdleme48bw  29821  cdleme46fsvlpq  29824  cdlemeg46fvcl  29825  cdlemeg49le  29830  cdlemeg46fjgN  29840  cdlemeg46fjv  29842  cdleme48d  29854  cdlemeg49lebilem  29858  cdleme50eq  29860  cdleme50f  29861  cdlemg2jlemOLDN  29912  cdlemg2klem  29914  cdlemk40  30236  cdlemk56  30290  diaglbN  30375  dvhlveclem  30428  dib1dim  30485  dibglbN  30486  diblss  30490  diblsmopel  30491  dicelvalN  30498  diclspsn  30514  cdlemn7  30523  dihordlem7  30534  dihopelvalcpre  30568  xihopellsmN  30574  dihopellsm  30575  dih1  30606  dihmeetlem1N  30610  dihglblem5apreN  30611  dihmeetlem2N  30619  dihglbcpreN  30620  dihmeetlem4preN  30626  dihmeetlem13N  30639  dih1dimatlem  30649  dihatlat  30654  dihjatcclem4  30741  lcdlss  30939
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 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-v 2742
  Copyright terms: Public domain W3C validator