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

Theorem vex 2766
Description: All set variables are sets (see isset 2767). 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 2258 . 2  |-  x  =  x
2 df-v 2765 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2365 . 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 2763
This theorem is referenced by:  isset  2767  ralv  2776  rexv  2777  reuv  2778  rmov  2779  rabab  2780  sbhypf  2808  ceqex  2873  ralab  2901  rexab  2903  moeq3  2917  mo2icl  2919  reu8  2936  sbc2or  2974  csbvarg  3083  csbiebg  3095  sbcnestgf  3103  sbnfc2  3116  ddif  3283  csbing  3351  dfun2  3379  dfin2  3380  vn0  3437  eqv  3445  abvor0  3447  sbss  3538  csbifg  3567  ifexg  3598  elpwg  3606  dftp2  3653  prnzg  3720  snssg  3728  difprsn  3730  sneqrg  3756  preq12bg  3765  pwpr  3797  pwtp  3798  pwv  3800  unipr  3815  uniprg  3816  unisng  3818  elintg  3844  elintrabg  3849  intss1  3851  ssint  3852  intmin  3856  intss  3857  intssuni  3858  intmin4  3865  intab  3866  intun  3868  intpr  3869  intprg  3870  uniintsn  3873  iinconst  3888  iuniin  3889  iinss1  3891  dfiin2g  3910  ssiinf  3925  iinss  3927  iinss2  3928  0iin  3934  iinab  3937  iinun2  3942  iundif2  3943  iindif2  3945  iinin2  3946  iinuni  3959  sspwuni  3961  iinpw  3964  iunpwss  3965  brab1  4042  csbopabg  4068  mptv  4086  trint  4102  trintss  4103  vprc  4126  inex1g  4131  ssexg  4134  intex  4143  inuni  4149  axpweq  4159  pwexg  4166  pwuni  4178  axpr  4185  zfpair2  4187  elALT  4190  rext  4194  sspwb  4195  unipw  4196  ssextss  4199  nnullss  4207  exss  4208  opth  4217  opthg  4218  copsexg  4224  copsex4g  4227  moop2  4233  euotd  4239  opelopabsbOLD  4245  opelopabsb  4247  pwin  4269  pwunss  4270  pwssun  4271  pwundifOLD  4273  epelg  4278  epel  4280  dfid3  4282  pofun  4302  epse  4348  wefrc  4359  tron  4387  onfr  4403  sucel  4437  suctr  4447  uniexg  4489  unexb  4492  snnex  4496  uniuni  4499  eusvnf  4501  eusvnfb  4502  reusv6OLD  4517  iunpw  4542  onint  4558  ordpwsuc  4578  unon  4594  ordunisuc  4595  onuninsuci  4603  orduninsuc  4606  limsssuc  4613  limuni3  4615  tfinds  4622  tfindsg  4623  tfindsg2  4624  tfinds2  4626  dfom2  4630  peano5  4651  finds  4654  findsg  4655  finds2  4656  0nelxp  4705  opelxp  4707  opeliunxp  4728  elvv  4736  elvvv  4737  elvvuni  4738  xpsspw  4785  xpsspwOLD  4786  relopabi  4799  opabid2  4803  difopab  4805  xpiindi  4809  ralxpf  4818  relop  4822  cnvco  4853  dfrn2  4856  dfdm4  4860  dmss  4866  dmin  4874  dmiun  4875  dmuni  4876  dm0  4880  dmi  4881  reldm0  4884  elreldm  4891  elrnmpt1  4916  dmrnssfld  4926  dmcoss  4932  dmcosseq  4934  opelresg  4950  resieq  4953  dmres  4964  elres  4978  relssres  4980  resopab  4984  resiexg  4985  iss  4986  dfres2  4990  dfima2  5002  csbima12g  5010  imadmrn  5012  imai  5015  elimasng  5027  args  5029  epini  5031  iniseg  5032  dffr3  5033  dfse2  5034  exse2  5035  cotr  5043  issref  5044  cnvsym  5045  intasym  5046  asymref  5047  asymref2  5048  intirr  5049  brcodir  5050  codir  5051  qfto  5052  poirr2  5055  cnvopab  5071  cnv0  5072  cnvi  5073  cnvdif  5075  rniun  5079  dminss  5083  imainss  5084  ssrnres  5104  rninxp  5105  dminxp  5106  cnvcnv3  5111  dfrel2  5112  dmsnn0  5125  dmsnopg  5131  cnvcnvsn  5137  dmsnsnsn  5138  cnvsng  5145  elxp4  5147  elxp5  5148  cnvresima  5149  dfco2  5159  dfco2a  5160  cores  5163  resco  5164  imaco  5165  rnco  5166  coiun  5169  co02  5173  coi1  5175  coass  5178  relssdmrn  5180  unielrel  5184  unixp0  5193  ressn  5198  cnviin  5199  cnvpo  5200  cnvso  5201  dffun2  5204  dffun7  5219  dffun8  5220  dffun9  5221  funopg  5225  funssres  5232  funun  5234  funcnvsn  5235  funcnv2  5247  funcnv  5248  funcnv3  5249  fun2cnv  5250  funcnvuni  5255  imadif  5265  isarep1  5269  2elresin  5293  fnres  5298  fcnvres  5356  fabexg  5360  fconstg  5366  fun11iun  5431  f1osng  5452  fv2  5454  fvprc  5455  fvex  5472  fv3  5474  nfunsn  5492  funimass4  5507  ssimaexg  5519  dffv2  5526  dmfco  5527  fvopab6  5555  fndmdif  5563  iinpreima  5589  fvelrn  5595  dff3  5607  dffo4  5610  exfo  5612  f1ompt  5616  fmptco  5625  fsng  5631  dfmpt  5635  fnressn  5639  fressnfv  5641  fvsng  5648  zfrep6  5682  funfvima3  5689  idref  5693  fvclss  5694  fvresex  5696  abrexco  5700  opabex3  5703  imaiun  5705  dff13  5717  foeqcnvco  5738  f1eqcocnv  5739  fliftcnv  5744  isocnv2  5762  isomin  5768  isoini  5769  isofr  5773  isose  5774  f1oweALT  5785  wemoiso  5789  wemoiso2  5790  knatar  5791  oprabid  5816  csbovg  5823  eloprabga  5868  mpt2v  5871  caovmo  5991  f1opw  6006  ofmres  6050  op1stg  6066  op2ndg  6067  1stval2  6071  2ndval2  6072  fo1st  6073  fo2nd  6074  f1stres  6075  f2ndres  6076  fo1stres  6077  fo2ndres  6078  1st2val  6079  2nd2val  6080  xp1st  6083  xp2nd  6084  sbcopeq1a  6106  csbopeq1a  6107  eloprabi  6120  mpt2mptsx  6121  dmmpt2ssx  6123  fmpt2x  6124  ovmptss  6134  fmpt2co  6136  df1st2  6139  df2nd2  6140  1stconst  6141  2ndconst  6142  curry1  6144  curry2  6147  fparlem1  6152  fparlem2  6153  fpar  6156  fsplit  6157  frxp  6159  xporderlem  6160  soxp  6162  fnwelem  6164  fnse  6166  reldmtpos  6176  dmtpos  6180  rntpos  6181  ovtpos  6183  dftpos3  6186  dftpos4  6187  tpostpos  6188  porpss  6215  sorpss  6216  sorpsscmpl  6222  uniabio  6235  iotaval  6236  sniota  6252  opiota  6256  opabiotafun  6257  opabiota  6259  riotav  6277  csbriotag  6285  onovuni  6327  smogt  6352  tfrlem3  6361  tfrlem8  6368  tfrlem9a  6370  tfrlem16  6377  tz7.44lem1  6386  rdg0g  6408  rdglim2  6413  tz7.48-1  6423  seqomlem1  6430  seqomlem2  6431  abianfplem  6438  oacl  6502  omcl  6503  oecl  6504  oa0r  6505  om0r  6506  om1r  6509  oe1m  6511  oaordi  6512  oawordri  6516  oawordeulem  6520  oalimcl  6526  oaass  6527  oarec  6528  omordi  6532  omwordri  6538  omlimcl  6544  odi  6545  omass  6546  omeulem1  6548  oen0  6552  oeordi  6553  oewordri  6558  oeworde  6559  oeoalem  6562  oeoelem  6564  nnawordex  6603  omabs  6613  omsmolem  6619  ercnv  6649  iserd  6654  eqerlem  6660  eqer  6661  ecdmn0  6670  erth  6672  erdisj  6675  qsss  6688  ecid  6692  qsid  6693  iiner  6699  qsel  6706  erovlem  6722  ecopovsym  6728  ecopovtrn  6729  ecopover  6730  mapprc  6744  fnmap  6747  fnpm  6748  mapval2  6765  pmsspw  6770  mapsn  6777  mapsncnv  6782  ixpconstg  6793  ixpprc  6805  uniixp  6807  ixpin  6809  ixpiin  6810  resixpfo  6822  elixpsn  6823  ixpsnf1o  6824  boxriin  6826  boxcutc  6827  bren  6839  brdomg  6840  domen  6843  domeng  6844  idssen  6874  ener  6876  domtr  6882  ensn1g  6894  en1  6896  en1b  6897  fundmen  6902  fundmeng  6903  mapsnen  6906  unen  6911  domdifsn  6913  xpsnen  6914  xpsneng  6915  xpcomeng  6922  xpassen  6924  xpdom2  6925  xpdom2g  6926  domunsncan  6930  omxpenlem  6931  pw2f1o  6935  fopwdom  6938  sbthlem10  6948  sbth  6949  sbthcl  6951  domunsn  6979  fodomr  6980  pwdom  6981  canth2  6982  canth2g  6983  domssex  6990  xpf1o  6991  mapen  6993  mapunen  6998  map2xp  6999  mapdom2  7000  mapdom3  7001  ssenen  7003  infensuc  7007  nneneq  7012  php  7013  php2  7014  php3  7015  sucdom2  7025  1sdom  7033  unxpdomlem2  7036  unxpdomlem3  7037  isinf  7044  fineqvlem  7045  fineqv  7046  pssnn  7049  ssfi  7051  dif1enOLD  7058  dif1en  7059  findcard  7065  findcard2  7066  findcard2s  7067  ac6sfi  7069  frfi  7070  fimax2g  7071  unbnn2  7082  isfinite2  7083  xpfi  7096  domunfican  7097  fiint  7101  fodomfi  7103  fodomfib  7104  iunfi  7112  pwfilem  7118  ixpfi2  7122  fissuni  7128  fipreima  7129  finsschain  7130  fival  7134  ssfii  7140  fi0  7141  fiin  7143  dffi2  7144  fipwuni  7147  fisn  7148  elfiun  7151  dffi3  7152  fifo  7153  marypha1lem  7154  dfsup2  7163  dfsup2OLD  7164  ordiso2  7198  oismo  7223  hartogslem1  7225  hartogs  7227  wofib  7228  wemappo  7232  wemapso2lem  7233  card2on  7236  brwdom  7249  brwdomn0  7251  brwdom2  7255  wdomtr  7257  wdompwdom  7260  canthwdom  7261  xpwdomg  7267  unxpwdom2  7270  ixpiunwdom  7273  elirrv  7279  zfregfr  7284  inf0  7290  inf3lema  7293  inf3lemd  7296  inf3lem1  7297  inf3lem2  7298  inf3lem3  7299  inf3lem5  7301  inf3lem6  7302  inf3lem7  7303  inf3  7304  infeq5  7306  omex  7312  dfom3  7316  dfom5  7319  infdifsn  7325  cantnfdm  7333  cantnfval  7337  cantnfval2  7338  cantnflt  7341  cantnff  7343  oemapso  7352  cantnflem1  7359  wemapwe  7368  cnfcom  7371  cnfcom3clem  7376  epfrs  7381  tcvalg  7391  tctr  7393  tcmin  7394  r1sdom  7414  r1val1  7426  tz9.12lem1  7427  tz9.12lem3  7429  tz9.13  7431  tz9.13g  7432  rankf  7434  unir1  7453  rankvalg  7457  rankonidlem  7468  r1val2  7477  bndrank  7481  ranklim  7484  r1pwOLD  7486  rankunb  7490  rankuni2b  7493  rankuni  7503  rankval4  7507  rankxplim  7517  rankxplim3  7519  rankxpsuc  7520  tcrank  7522  cp  7529  bnd2  7531  kardex  7532  karden  7533  cardf2  7544  tskwe  7551  cardlim  7573  harcard  7579  cardiun  7583  pm54.43  7601  r0weon  7608  infxpenlem  7609  infxpenc2lem2  7615  fseqenlem1  7619  fseqenlem2  7620  fseqen  7622  dfac8alem  7624  dfac8clem  7627  ac10ct  7629  ween  7630  acnlem  7643  finacn  7645  acndom  7646  acndom2  7649  wdomfil  7656  infpwfien  7657  alephon  7664  alephcard  7665  alephordi  7669  cardaleph  7684  alephval3  7705  iunfictbso  7709  aceq3lem  7715  dfac3  7716  dfac4  7717  dfac5lem1  7718  dfac5lem2  7719  dfac5lem3  7720  dfac5lem4  7721  dfac5lem5  7722  dfac5  7723  dfac2a  7724  dfac2  7725  dfac8  7729  dfac9  7730  dfac10b  7733  acacni  7734  dfacacn  7735  dfac13  7736  kmlem1  7744  kmlem2  7745  kmlem9  7752  kmlem10  7753  kmlem11  7754  kmlem12  7755  kmlem13  7756  cdafn  7763  pwsdompw  7798  infmap2  7812  ackbij1lem5  7818  ackbij1lem8  7821  ackbij2lem3  7835  ackbij2  7837  cflm  7844  cardcf  7846  cfeq0  7850  cfsuc  7851  cff1  7852  cfflb  7853  cfval2  7854  cflim2  7857  cfss  7859  cfslb2n  7862  cofsmo  7863  cfsmolem  7864  cfcoflem  7866  coftr  7867  sornom  7871  infpssr  7902  fin4en1  7903  fin23lem11  7911  enfin2i  7915  fin23lem26  7919  fin23lem14  7927  fin23lem16  7929  fin23lem17  7932  fin23lem21  7933  fin23lem32  7938  fin23lem34  7940  fin23lem39  7944  compsscnvlem  7964  compssiso  7968  isf34lem4  7971  enfin1ai  7978  isfin1-3  7980  fin67  7989  dffin7-2  7992  fin1a2lem7  8000  fin1a2lem10  8003  fin1a2lem12  8005  fin1a2lem13  8006  fin12  8007  itunitc1  8014  itunitc  8015  ituniiun  8016  hsmexlem2  8021  hsmexlem4  8023  hsmex  8026  axcc2lem  8030  axcc3  8032  acncc  8034  fin41  8038  dominf  8039  dcomex  8041  axdc2lem  8042  axdc3lem  8044  axdc3lem2  8045  axdc3lem4  8047  axdc4lem  8049  axcclem  8051  ac9  8078  ac6s  8079  ac6sg  8083  ac9s  8088  numthcor  8089  zorn2lem1  8091  zorn2lem4  8094  zorn2lem7  8097  zorng  8099  zornn0g  8100  ttukeylem5  8108  ttukeylem6  8109  ttukeylem7  8110  axdclem  8114  axdclem2  8115  fodomg  8118  fodomb  8119  brdom3  8121  brdom5  8122  brdom4  8123  brdom7disj  8124  brdom6disj  8125  iunfo  8129  ondomon  8153  cardmin  8154  alephval2  8162  dominfac  8163  fpwwe2lem1  8221  fpwwe2lem8  8227  fpwwe2lem11  8230  fpwwe2lem12  8231  fpwwe2lem13  8232  fpwwe2  8233  fpwwe  8236  canthwe  8241  canthp1lem1  8242  pwfseqlem1  8248  pwfseqlem2  8249  pwfseqlem3  8250  pwfseqlem4a  8251  pwfseqlem5  8253  pwxpndom2  8255  gchac  8263  gch2  8269  inawinalem  8279  winainflem  8283  winalim2  8286  winafp  8287  gchina  8289  wunfi  8311  intwun  8325  wunex2  8328  uniwun  8330  eltsk2g  8341  inttsk  8364  inar1  8365  rankcf  8367  tskcard  8371  tskuni  8373  gruun  8396  intgru  8404  ingru  8405  wfgru  8406  grudomon  8407  gruina  8408  grur1a  8409  grur1  8410  grutsk  8412  axgroth5  8414  axgroth2  8415  grothpw  8416  grothpwex  8417  axgroth6  8418  grothomex  8419  grothac  8420  axgroth3  8421  grothprim  8424  grothtsk  8425  inaprc  8426  nqereu  8521  nqerf  8522  dmrecnq  8560  ltaddnq  8566  genpnnp  8597  genpnmax  8599  genpcl  8600  nqpr  8606  addclprlem1  8608  mulclprlem  8611  distrlem4pr  8618  1idpr  8621  prlem934  8625  ltaddpr  8626  ltexprlem3  8630  ltexprlem4  8631  ltexprlem6  8633  ltexprlem7  8634  prlem936  8639  reclem2pr  8640  reclem3pr  8641  mulasssr  8680  ltsosr  8684  0idsr  8687  1idsr  8688  ltasr  8690  recexsrlem  8693  mulgt0sr  8695  supsrlem  8701  ltresr  8730  axmulass  8747  axrrecex  8753  axpre-lttri  8755  wuncn  8760  renfdisj  8853  wloglei  9273  lbinfm  9675  supmul1  9687  supmullem1  9688  supmullem2  9689  supmul  9690  dfinfmr  9699  infmsup  9700  infmrgelb  9702  infmrlb  9703  dfnn2  9727  dflt2  10449  xrinfmss2  10595  infmxrgelb  10619  xrinfm0  10621  fzpr  10806  uzrdgfni  10987  axdc4uzlem  11010  axdc4uz  11011  seqval  11023  seqfeq4  11061  serle  11067  seqof  11069  hashxplem  11350  hashmap  11352  hashpw  11353  hashfun  11354  hashbclem  11355  hashfacen  11357  hashf1lem1  11358  hashf1lem2  11359  hashf1  11360  fz1isolem  11364  ccatfn  11392  wrdexb  11414  wrdind  11442  shftfval  11530  shftfib  11532  shftfn  11533  2shfti  11540  sqrlem6  11698  rexfiuz  11796  rlimdm  11990  fclim  11992  climshft  12015  fsum2dlem  12198  fsumcom2  12202  fsum0diag2  12210  fsumabs  12224  fsumrlim  12234  fsumo1  12235  fsumiun  12244  isumltss  12269  supcvg  12276  xpnnenOLD  12450  rpnnen2lem11  12465  algrf  12705  isprm2lem  12727  isprm2  12728  prmind2  12731  iserodd  12850  4sqlem12  12965  vdwmc  12987  vdwlem10  12999  vdwlem13  13002  ramtlecl  13009  hashbc0  13014  ramval  13017  ramcl2lem  13018  ramub2  13023  0ram  13029  ram0  13031  ramub1lem1  13035  ramub1lem2  13036  ramub1  13037  restfn  13291  elrest  13294  restsspw  13298  prdsval  13317  prdsle  13323  prdsless  13324  prdsleval  13338  pwsle  13353  imasaddfnlem  13392  imasvscafn  13401  imasleval  13405  xpsc0  13424  xpsc1  13425  xpsfrnel2  13429  ismre  13454  fnmre  13455  ismred  13466  mremre  13468  fnmrc  13471  mrcfval  13472  mrisval  13494  mreexexlem4d  13511  isacs2  13517  mreacs  13522  acsfn  13523  acsfn1  13525  acsfn2  13527  cidffn  13542  comfeq  13571  invsym2  13627  oppcsect2  13639  brssc  13653  sscpwex  13654  isssc  13659  issubc  13674  isfuncd  13701  cofucl  13724  funcres2b  13733  funcpropd  13736  setcmon  13881  catcval  13890  fnxpc  13912  xpcval  13913  xpccatid  13924  curf2ndf  13983  drsdirfi  14034  isdrs2  14035  clatl  14182  odupos  14201  oduposb  14202  oduglb  14205  odulub  14207  posglbd  14215  ipoval  14219  ipolerval  14221  fpwipodrs  14229  ipodrsima  14230  isacs5lem  14234  psdmrn  14278  psssdm2  14286  submacs  14404  pwsdiagmhm  14407  gsumwspan  14430  mulgpropd  14562  subgacs  14614  nsgacs  14615  eqgfval  14627  eqgval  14628  gicsubgen  14704  gaid  14715  gaorb  14723  orbsta  14729  symgval  14733  symgbas  14734  symgplusg  14738  sylow1lem2  14872  sylow2alem1  14890  sylow2alem2  14891  sylow2a  14892  sylow2blem1  14893  sylow2blem2  14894  sylow2blem3  14895  sylow3lem1  14900  sylow3lem3  14902  sylow3lem6  14905  efgval  14988  efgval2  14995  efgrelexlemb  15021  efgcpbllema  15025  efgcpbllemb  15026  vrgpfval  15037  frgpuplem  15043  divsabl  15119  frgpnabllem1  15123  gsumval3  15153  gsumzaddlem  15165  gsumzadd  15166  gsum2d  15185  gsum2d2  15187  gsumcom2  15188  gsumxp  15189  dprdfadd  15217  dprdres  15225  subgdmdprd  15231  dprd2dlem1  15238  dprd2d2  15241  ablfac1eulem  15269  pgpfac1lem5  15276  opprsubg  15380  subrgmre  15531  subsubrg2  15534  subrgpropd  15541  lss1d  15682  lssintcl  15683  lssmre  15685  lssacs  15686  pwsdiaglmhm  15776  islbs3  15870  lbsextlem4  15876  drngnidl  15943  lidldvgen  15969  psrbaglefi  16080  mplcoe1  16171  mplcoe2  16173  ltbval  16175  ltbwe  16176  opsrle  16179  opsrtoslem1  16187  opsrtoslem2  16188  evlslem4  16207  coe1mul2  16308  coe1tm  16311  znleval  16470  cssmre  16555  thlle  16559  pjfval2  16571  istopon  16625  tgval2  16656  bastg  16666  tgdom  16678  distop  16695  indistopon  16700  fctop  16703  cctop  16705  ppttop  16706  epttop  16708  fncld  16721  cldss2  16729  ntreq0  16776  discld  16788  mretopd  16791  toponmre  16792  neisspw  16806  opnnei  16819  tgrest  16852  resttopon  16854  restco  16857  restdis  16871  ordtbas2  16883  ordtcnv  16893  ordtrest2  16896  pnfnei  16912  mnfnei  16913  iscnp2  16931  subbascn  16946  cnntr  16966  cnrest2  16976  cnpresti  16978  cnprest  16979  cnprest2  16980  ist1-3  17039  hausnei2  17043  isnrm2  17048  dishaus  17072  cmpcovf  17080  fincmp  17082  cmpsublem  17088  cmpsub  17089  cmpcld  17091  uncmp  17092  fiuncmp  17093  hauscmplem  17095  cmpfi  17097  dfcon2  17107  consuba  17108  cnconn  17110  uncon  17117  t1conperf  17124  is1stc2  17130  1stcfb  17133  2ndcsb  17137  2ndc1stc  17139  1stcrest  17141  2ndcctbss  17143  2ndcdisj  17144  2ndcomap  17146  2ndcsep  17147  dis2ndc  17148  llyi  17162  nllyi  17163  nlly2i  17164  llynlly  17165  subislly  17169  restnlly  17170  restlly  17171  islly2  17172  llyrest  17173  llyidm  17176  nllyidm  17177  hausllycmp  17182  cldllycmp  17183  lly1stc  17184  dislly  17185  hausmapdom  17188  kgenf  17198  iskgen3  17206  llycmpkgen2  17207  1stckgenlem  17210  1stckgen  17211  kgencn2  17214  txuni2  17222  txbas  17224  eltx  17225  ptpjpre1  17228  ptuni2  17233  ptpjcn  17267  ptpjopn  17268  ptclsg  17271  dfac14  17274  xkoccn  17275  txcnp  17276  txcnmpt  17280  prdstopn  17284  txrest  17287  txdis  17288  txindis  17290  txdis1cn  17291  txlly  17292  txnlly  17293  pthaus  17294  txcmplem1  17297  txcmplem2  17298  hausdiag  17301  txlm  17304  tx1stc  17306  tx2ndc  17307  txkgen  17308  xkopt  17311  xkococnlem  17315  xkococn  17316  cnmpt1st  17324  cnmpt2nd  17325  xkofvcn  17340  xkoinjcn  17343  txcon  17345  qtoptop2  17352  qtopuni  17355  basqtop  17364  tgqtop  17365  hmphdis  17449  indishmph  17451  txhmeo  17456  pt1hmeo  17459  ptuncnv  17460  ptunhmeo  17461  xpstopnlem1  17462  ptcmpfi  17466  xkohmeo  17468  isfbas  17486  isfbas2  17492  fbssfi  17494  trfbas2  17500  isfild  17515  snfil  17521  elfg  17528  fgcl  17535  filcon  17540  fbasrn  17541  filuni  17542  trfil2  17544  cfinfil  17550  csdfil  17551  supfil  17552  zfbas  17553  isufil2  17565  filssufilg  17568  acufl  17574  filufint  17577  uffix  17578  ufinffr  17586  ufildr  17588  fin1aufil  17589  rnelfmlem  17609  rnelfm  17610  fmfnfmlem3  17613  fmfnfmlem4  17614  fmfnfm  17615  ufldom  17619  flimrest  17640  hauspwpwf1  17644  txflf  17663  fclsrest  17681  fclscmp  17687  alexsubb  17702  alexsubALTlem1  17703  alexsubALTlem2  17704  alexsubALTlem3  17705  alexsubALTlem4  17706  alexsubALT  17707  ptcmplem2  17709  ptcmplem3  17710  ptcmplem4  17711  ptcmplem5  17712  tmdgsum  17740  symgtgp  17746  cldsubg  17755  tgpconcomp  17757  divstgplem  17765  divstgphaus  17767  prdstmdd  17768  tsmsval2  17774  tsmssubm  17787  imasdsf1olem  17899  xpsdsval  17907  xmetec  17942  prdsbl  17999  stdbdxmet  18023  met1stc  18029  prdsxmslem2  18037  dscopn  18058  xrtgioo  18274  xrsblre  18279  icccmplem1  18289  icccmplem2  18290  fsumcn  18336  fsum2cn  18337  cnllycmp  18416  isphtpc  18454  pi1blem  18499  iscmet3  18681  metcld2  18694  bcthlem4  18711  minveclem3b  18754  ovolfiniun  18822  ovoliunlem1  18823  ovoliunlem2  18824  finiunmbl  18863  volfiniun  18866  iundisj2  18868  uniioombllem3  18902  vitalilem2  18926  vitalilem3  18927  vitali  18930  mbfimaopnlem  18972  itg1addlem4  19016  mbfi1fseqlem4  19035  mbfi1fseqlem6  19037  itgfsum  19143  ellimc2  19189  limcflf  19193  perfdvf  19215  dvres  19223  dvres2  19224  dvnff  19234  dvcj  19261  dvrec  19266  dvmptfsum  19284  dvef  19289  rolle  19299  dvivthlem1  19317  dvfsumle  19330  dvfsumabs  19332  dvfsumlem2  19336  dvfsumlem3  19337  ftc1cn  19352  mpfind  19390  pf1ind  19400  vieta1lem2  19653  elqaalem2  19662  ulmdv  19742  logfac  19916  xrlimcnp  20225  jensenlem1  20243  jensenlem2  20244  jensen  20245  wilthlem2  20269  prmorcht  20378  lgsquadlem1  20555  lgsquadlem2  20556  dchrisumlema  20599  dchrisumlem3  20602  ex-natded9.26  20794  nvss  21109  vsfval  21151  h2hlm  21520  axhcompl-zf  21538  hlim2  21731  hhcmpl  21739  hhcms  21742  shex  21751  isch2  21763  helch  21783  hhsscms  21816  occl  21843  chintcli  21870  dfch2  21946  spanuni  22083  spansni  22096  elnlfn  22468  nmopun  22554  nlelchi  22601  cnlnssadj  22620  adjbd1o  22625  branmfn  22645  pjnmopi  22688  hmopidmchi  22691  abrexss  23001  ballotlem2  23008  ballotlemsf1o  23033  ballotlemirc  23051  dmgmseqn0  23068  derangenlem  23074  subfacp1lem1  23082  subfacp1lem3  23085  subfacp1lem4  23086  subfacp1lem5  23087  erdszelem7  23100  erdszelem8  23101  erdsze2lem2  23107  kur14lem9  23117  ptpcon  23136  indispcon  23137  conpcon  23138  cnllyscon  23148  rellyscon  23154  cvmsss2  23177  cvmcov2  23178  cvmliftlem15  23201  cvmlift2lem1  23205  cvmlift2lem12  23217  umgraex  23247  eupath  23277  ghomgrplem  23368  relexpindlem  23408  rtrclreclem.trans  23415  dfrtrcl2  23417  untsucf  23428  dftr6  23478  coepr  23480  dffr5  23481  dfso2  23482  dfpo2  23483  br8  23484  br6  23485  br4  23486  dfres3  23487  cnvco1  23488  cnvco2  23489  fundmpss  23491  fprb  23498  dfdm5  23501  dfrn5  23502  setinds  23503  dfon2lem1  23508  dfon2lem3  23510  dfon2lem6  23513  dfon2lem7  23514  dfon2lem8  23515  dfon2  23517  rdgprc  23520  dfrdg2  23521  predreseq  23548  predpo  23553  predbrg  23555  setlikespec  23556  predep  23561  preddowncl  23565  preduz  23569  predfz  23572  tz6.26  23574  trpredrec  23610  poseq  23622  soseq  23623  wfrlem5  23629  wfrlem10  23634  wfrlem12  23636  wfrlem13  23637  wfrlem14  23638  wfrlem16  23640  tfrALTlem  23645  frrlem5  23654  frrlem11  23662  axsltsolem1  23690  axfelem18  23732  axfelem22  23736  txpss3v  23794  brtxp  23796  brtxp2  23797  pprodss4v  23800  brpprod  23801  brpprod3a  23802  brpprod3b  23803  brsset  23805  idsset  23806  dfon3  23808  brtxpsd  23810  brbigcup  23814  dfbigcup2  23815  fobigcup  23816  elfix  23819  elfix2  23820  dffix2  23821  fixcnv  23824  limitssson  23827  dfom5b  23828  elfuns  23829  elfunsg  23830  elsingles  23832  fnsingle  23833  fvsingle  23834  dfiota3  23837  brimage  23840  brimageg  23841  funimage  23842  fnimage  23843  imageval  23844  brcart  23846  brdomaing  23849  brrangeg  23850  brimg  23851  brapply  23852  brcup  23853  brcap  23854  brsuccf  23855  funpartfun  23856  funpartfv  23858  fullfunfv  23860  brrestrict  23862  dfrdg4  23863  tfrqfree  23864  altopelaltxp  23885  altxpsspw  23886  brsegle  24106  fvline  24142  liness  24143  ellines  24150  bpoly2  24167  bpoly3  24168  rankung  24171  ranksng  24172  rankelg  24173  rankpwg  24174  rankeq1o  24176  elhf2g  24181  hfext  24188  onsucconi  24251  tpssg  24298  fatesg  24322  eqvinopb  24331  copsexgb  24332  elo  24407  stcat  24410  splint  24414  domfldrefc  24423  ranfldrefc  24424  domrngref  24426  domintrefb  24429  restidsing  24442  prj1b  24445  prj3  24446  eloi  24452  elintabg  24456  domintrefc  24492  inttpemp  24506  mapmapmap  24515  injsurinj  24516  npincppr  24526  repcpwti  24528  cbcpcp  24529  cbicp  24533  prjmapcp2  24537  dstr  24538  iscst4  24544  islatalg  24550  domrancur1c  24569  mnlmxl2  24636  defse3  24639  inpc  24644  inposet  24645  tolat  24653  toplat  24657  dfdir2  24658  prodeq3ii  24675  fprodser  24687  symgfo  24735  svs2  24854  inttop2  24882  sallnei  24896  nsn  24897  dmhmph  24900  rnhmph  24901  intopcoaconlem3b  24905  intopcoaconlem3  24906  qusp  24909  efilcp  24919  fgsb2  24922  bwt2  24959  dmrngcmp  25118  dualded  25150  ishomd  25157  vtarsuelt  25262  fnctartar  25274  fnctartar2  25275  dfiunv2  25283  prismorcset2  25285  domcatfun  25292  codcatfun  25301  idcatfun  25308  empklst  25376  fnckle  25412  pfsubkl  25414  pgapspf2  25420  isconcl5a  25468  isconcl5ab  25469  bosser  25534  pdiveql  25535  abhp2  25542  bhp2a  25543  cnvresimaOLD  25593  trer  25594  finminlem  25598  gtinf  25601  fneer  25655  fnessref  25660  refssfne  25661  islocfin  25663  comppfsc  25674  neibastop1  25675  neibastop2lem  25676  neibastop3  25678  topmeet  25680  topjoin  25681  neifg  25687  tailfb  25693  filnetlem2  25695  filnetlem3  25696  filnetlem4  25697  cover2g  25726  f1opr  25758  inixp  25766  indexdom  25780  frinfm  25783  sdclem2  25819  sdclem1  25820  fdc  25822  isbndx  25873  prdstotbnd  25885  heibor1lem  25900  heiborlem1  25902  heiborlem3  25904  heiborlem4  25905  heiborlem5  25906  heiborlem6  25907  heiborlem8  25909  heiborlem10  25911  ismrer1  25929  riscer  25986  divrngidl  26020  intidl  26021  isfldidl  26060  ispridlc  26062  prtlem10  26100  prtlem13  26103  prtlem16  26104  prtlem19  26113  prter2  26116  prter3  26117  ralxpmap  26128  elrfi  26136  ismrcd1  26140  ismrcd2  26141  istopclsd  26142  ismrc  26143  mrefg2  26149  isnacs3  26152  mzpclall  26172  mzpincl  26179  mzpsubst  26193  mzpcompact2lem  26196  mzpcompact2  26197  eldioph2lem1  26206  eldioph2lem2  26207  eldiophss  26221  diophrex  26222  rexrabdioph  26242  2rexfrabdioph  26244  3rexfrabdioph  26245  4rexfrabdioph  26246  6rexfrabdioph  26247  7rexfrabdioph  26248  rabren3dioph  26265  fphpd  26266  rencldnfilem  26270  pellexlem5  26285  pellex  26287  rmxypairf1o  26363  monotuz  26393  monotoddzzfi  26394  oddcomabszz  26396  2nn0ind  26397  zindbi  26398  mzpcong  26426  rmydioph  26474  rmxdioph  26476  expdiophlem2  26482  setindtr  26484  setindtrs  26485  dford3lem2  26487  ttac  26496  pw2f1ocnv  26497  wepwsolem  26505  inisegn0  26507  dnnumch1  26508  fnwe2val  26513  fnwe2lem2  26515  aomclem1  26518  aomclem2  26519  aomclem6  26523  dfac11  26527  kelac2lem  26529  dfac21  26531  islssfg2  26536  lmhmlnmsplit  26552  pwssplit3  26557  filnm  26559  pwslnmlem1  26561  pwslnm  26563  dsmmval  26567  frlmlbs  26616  unxpwdom3  26623  enfixsn  26624  dfacbasgrp  26640  islindf4  26675  lmisfree  26679  lnr2i  26687  lnrfg  26690  hbtlem6  26700  rngunsnply  26745  pmtrfval  26760  symggen  26778  gsumcom3  26821  acsfn1p  26874  sdrgacs  26876  idomsubgmo  26881  fgraphxp  26897  expgrowth  26919  2sbc6g  26983  iotain  26985  compel  27008  ipo0  27020  ifr0  27021  fnchoice  27068  stoweidlem31  27115  stoweidlem57  27141  stoweidlem62  27146  onfrALTlem5  27360  onfrALTlem4  27361  onfrALTlem3  27362  opelopab4  27370  a9e2nd  27377  trsspwALT  27642  trsspwALT2  27643  trsspwALT3  27644  pwtrVD  27648  pwtrOLD  27649  unipwrVD  27658  unipwr  27659  onfrALTlem5VD  27711  onfrALTlem4VD  27712  onfrALTlem3VD  27713  relopabVD  27727  a9e2ndVD  27734  sspwimp  27744  sspwimpVD  27745  sspwimpcf  27746  sspwimpcfVD  27747  sspwimpALT  27751  sspwimpALT2  27755  a9e2ndALT  27757  bnj23  27793  bnj62  27795  bnj156  27805  bnj219  27810  bnj610  27825  bnj918  27845  bnj927  27849  bnj976  27858  bnj1098  27864  bnj1379  27912  bnj110  27939  bnj98  27948  bnj154  27959  bnj155  27960  bnj535  27971  bnj556  27981  bnj557  27982  bnj581  27989  bnj591  27992  bnj594  27993  bnj580  27994  bnj607  27997  bnj609  27998  bnj600  28000  bnj849  28006  bnj893  28009  bnj908  28012  bnj934  28016  bnj944  28019  bnj964  28024  bnj966  28025  bnj969  28027  bnj970  28028  bnj910  28029  bnj986  28035  bnj999  28038  bnj1018  28043  bnj907  28046  bnj1039  28050  bnj1040  28051  bnj1052  28054  bnj1123  28065  bnj1030  28066  bnj1133  28068  bnj1128  28069  bnj1145  28072  bnj1204  28091  bnj1373  28109  bnj1417  28120  bnj1421  28121  bnj1498  28140  eqlkr2  28457  glbconxN  28734  pmapglbx  29125  pmapglb  29126  pclclN  29247  pclfinN  29256  polval2N  29262  pclfinclN  29306  osumcllem10N  29321  pexmidlem7N  29332  cdleme31sdnN  29743  cdlemefr44  29781  cdleme48fv  29855  cdleme46fvaw  29857  cdleme48bw  29858  cdleme46fsvlpq  29861  cdlemeg46fvcl  29862  cdlemeg49le  29867  cdlemeg46fjgN  29877  cdlemeg46fjv  29879  cdleme48d  29891  cdlemeg49lebilem  29895  cdleme50eq  29897  cdleme50f  29898  cdlemg2jlemOLDN  29949  cdlemg2klem  29951  cdlemk40  30273  cdlemk56  30327  diaglbN  30412  dvhlveclem  30465  dib1dim  30522  dibglbN  30523  diblss  30527  diblsmopel  30528  dicelvalN  30535  diclspsn  30551  cdlemn7  30560  dihordlem7  30571  dihopelvalcpre  30605  xihopellsmN  30611  dihopellsm  30612  dih1  30643  dihmeetlem1N  30647  dihglblem5apreN  30648  dihmeetlem2N  30656  dihglbcpreN  30657  dihmeetlem4preN  30663  dihmeetlem13N  30676  dih1dimatlem  30686  dihatlat  30691  dihjatcclem4  30778  lcdlss  30976
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 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-v 2765
  Copyright terms: Public domain W3C validator