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

Theorem vex 3112
Description: All setvar variables are sets (see isset 3113). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
vex

Proof of Theorem vex
StepHypRef Expression
1 equid 1791 . 2
2 df-v 3111 . . 3
32abeq2i 2584 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109
This theorem is referenced by:  isset  3113  eqvisset  3117  ralv  3123  rexv  3124  reuv  3125  rmov  3126  rabab  3127  sbhypf  3156  ralab  3260  rexab  3262  moeq3  3276  reu8  3295  sbc2or  3336  csbiebg  3457  ddif  3635  dfun2  3732  dfin2  3733  vn0  3792  eqv  3801  abvor0  3803  sbcnestgf  3839  csbvarg  3848  sbnfc2  3854  csbun  3857  csbin  3860  csbingOLD  3861  sbss  3939  csbif  3991  csbifgOLD  3992  ifexg  4011  selpw  4019  ssnid  4058  dftp2  4075  prnzg  4150  snssg  4163  difprsnss  4165  sneqrg  4199  preq12bg  4209  prel12g  4210  pwpr  4245  pwtp  4246  pwv  4248  unipr  4262  uniprg  4263  unisng  4265  elintg  4294  elintrabg  4299  intss1  4301  ssint  4302  intmin  4306  intssOLD  4308  intssuni  4309  intmin4  4316  intab  4317  intun  4319  intpr  4320  intprg  4321  uniintsn  4324  iinconst  4340  iuniin  4341  iinss1  4343  dfiin2g  4363  dfiunv2  4366  ssiinf  4379  iinss  4381  iinss2  4382  0iin  4388  iinab  4391  iinun2  4396  iundif2  4397  iindif2  4399  iinin2  4400  iinuni  4414  iinpw  4419  brab1  4497  mptv  4544  trint  4560  trintss  4561  vprc  4590  inex1g  4595  ssexg  4598  intex  4608  inuni  4614  axpweq  4629  pwexg  4636  eusvnf  4647  reusv6OLD  4663  axpr  4690  zfpair2  4692  elALT  4695  sspwb  4701  nnullss  4714  exss  4715  opth  4726  opthg  4727  copsexg  4737  copsexgOLD  4738  copsex4g  4741  moop2  4747  euotd  4753  opelopabsbALT  4761  opelopabsb  4762  csbopab  4784  csbopabgALT  4785  pwssun  4791  epelg  4797  epel  4799  dfid3  4801  pofun  4821  epse  4867  wefrc  4878  tron  4906  onfr  4922  sucel  4956  suctr  4966  0nelxp  5032  opelxp  5034  opeliunxp  5056  elvv  5063  elvvv  5064  elvvuni  5065  xpsspw  5121  xpsspwOLD  5122  relopabi  5133  opabid2  5137  difopab  5139  xpiindi  5143  ralxpf  5154  relop  5158  cnvco  5193  dfrn2  5196  dfdm4  5200  dmss  5207  dmin  5215  dmiun  5216  dmuni  5217  dm0  5221  dmi  5222  reldm0  5225  elreldm  5232  elrnmpt1  5256  dmrnssfld  5266  dmcoss  5267  dmcosseq  5269  opelresg  5286  resieq  5289  dmres  5299  elres  5314  relssres  5316  resopab  5325  iss  5326  dfres2  5331  restidsing  5335  dfima2  5344  imadmrn  5352  imai  5354  csbima12  5359  csbima12gOLD  5360  elimasng  5368  args  5370  epini  5372  iniseg  5373  dffr3  5374  dfse2  5375  cotrg  5383  issref  5385  cnvsym  5386  intasym  5387  asymref  5388  asymref2  5389  intirr  5390  brcodir  5391  codir  5392  qfto  5393  poirr2  5396  cnvopab  5412  cnv0  5414  cnvi  5415  cnvdif  5417  rniun  5421  dminss  5425  imainss  5426  inimasn  5428  xpdifid  5440  ssrnres  5450  rninxp  5451  dminxp  5452  cnvcnv3  5461  dfrel2  5462  dmsnn0  5478  dmsnopg  5484  cnvcnvsn  5490  dmsnsnsn  5491  cnvsng  5499  cnvresima  5501  dfco2  5511  dfco2a  5512  cores  5515  resco  5516  imaco  5517  rnco  5518  coiun  5522  co02  5526  coi1  5528  coass  5531  relssdmrn  5533  unielrel  5537  unixp0  5546  ressn  5548  cnviin  5549  cnvpo  5550  cnvso  5551  uniabio  5566  iotaval  5567  sniota  5583  csbiota  5585  csbiotagOLD  5586  dffun2  5603  dffun7  5619  dffun8  5620  dffun9  5621  funopg  5625  funssres  5633  funun  5635  funcnvsn  5638  funcnv2  5652  funcnv  5653  funcnv3  5654  fun2cnv  5655  imadif  5668  isarep1  5672  2elresin  5697  fnres  5702  fcnvres  5767  fconstg  5777  f1osng  5859  dffv3  5867  fv3  5884  fvres  5885  nfunsn  5902  funimass4  5924  opabiotafun  5934  opabiota  5936  ssimaexg  5939  dffv2  5946  dmfco  5947  fvopab6  5980  fndmdif  5991  iinpreima  6017  fvn0ssdmfun  6022  fvelrn  6024  dff3  6044  dffo4  6047  exfo  6049  f1ompt  6053  fmptco  6064  fsng  6070  dfmpt  6076  fnressn  6083  fressnfv  6085  fvsng  6105  fnprb  6129  fnprOLD  6130  funfvima3  6149  idref  6153  fvclss  6154  abrexco  6156  imaiun  6157  dff13  6166  foeqcnvco  6203  f1eqcocnv  6204  fliftcnv  6209  isocnv2  6227  isomin  6233  isoini  6234  isofr  6238  isose  6239  knatar  6253  riotav  6262  csbriota  6269  oprabid  6323  csbov123  6330  csbovgOLD  6332  0neqopab  6341  oprabv  6345  eloprabga  6389  mpt2v  6392  caovmo  6512  f1opw  6529  porpss  6584  sorpss  6585  uniexg  6597  unexb  6600  snnex  6606  uniuni  6609  onint  6630  unon  6666  ordunisuc  6667  onuninsuci  6675  orduninsuc  6678  limsssuc  6685  limuni3  6687  tfinds  6694  tfindsg  6695  tfindsg2  6696  tfinds2  6698  dfom2  6702  peano5  6723  finds  6726  findsg  6727  finds2  6728  resiexg  6736  exse2  6739  elxp4  6744  elxp5  6745  f1oexbi  6750  funcnvuni  6753  fun11iun  6760  zfrep6  6768  fvresex  6773  opabex3d  6778  opabex3  6779  f1oweALT  6784  wemoiso  6785  wemoiso2  6786  ofmres  6796  op1stg  6812  op2ndg  6813  1stval2  6817  2ndval2  6818  fo1st  6820  fo2nd  6821  f1stres  6822  f2ndres  6823  fo1stres  6824  fo2ndres  6825  1st2val  6826  2nd2val  6827  xp1st  6830  xp2nd  6831  sbcopeq1a  6852  csbopeq1a  6853  opiota  6859  eloprabi  6862  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  fmpt2co  6883  df1st2  6886  df2nd2  6887  1stconst  6888  2ndconst  6889  curry1  6892  curry2  6895  fparlem1  6900  fparlem2  6901  fpar  6904  fsplit  6905  fo2ndf  6907  f1o2ndf1  6908  frxp  6910  xporderlem  6911  soxp  6913  fnwelem  6915  fnse  6917  suppvalbr  6922  cnvimadfsn  6927  suppimacnv  6929  reldmtpos  6982  dmtpos  6986  rntpos  6987  ovtpos  6989  dftpos3  6992  dftpos4  6993  tpostpos  6994  onovuni  7032  smogt  7057  tfrlem3  7066  tfrlem5  7068  tfrlem8  7072  tfrlem9a  7074  tfrlem16  7081  tz7.44lem1  7090  rdg0g  7112  rdglim2  7117  tz7.48-1  7127  seqomlem1  7134  seqomlem2  7135  oacl  7204  omcl  7205  oecl  7206  oa0r  7207  om0r  7208  om1r  7211  oe1m  7213  oaordi  7214  oawordri  7218  oawordeulem  7222  oalimcl  7228  oaass  7229  oarec  7230  omordi  7234  omwordri  7240  omlimcl  7246  odi  7247  omass  7248  omeulem1  7250  oen0  7254  oeordi  7255  oewordri  7260  oeworde  7261  oeoalem  7264  oeoelem  7266  nnawordex  7305  omabs  7315  omsmolem  7321  ercnv  7351  iserd  7356  eqerlem  7362  eqer  7363  ecdmn0  7373  erth  7375  erdisj  7378  qsss  7391  ecid  7395  qsid  7396  iiner  7402  qsel  7409  erovlem  7426  ecopovsym  7432  ecopovtrn  7433  ecopover  7434  mapprc  7443  fnmap  7446  fnpm  7447  mapval2  7468  mapsn  7480  mapsncnv  7485  ralxpmap  7488  ixpconstg  7498  ixpprc  7510  ixpin  7514  ixpiin  7515  resixpfo  7527  elixpsn  7528  ixpsnf1o  7529  boxriin  7531  boxcutc  7532  bren  7545  brdomg  7546  domen  7549  domeng  7550  idssen  7580  ener  7582  domtr  7588  ensn1g  7600  en1  7602  en1b  7603  fundmen  7609  fundmeng  7610  mapsnen  7613  unen  7618  domdifsn  7620  xpsnen  7621  xpsneng  7622  xpcomeng  7629  xpassen  7631  xpdom2  7632  xpdom2g  7633  domunsncan  7637  omxpenlem  7638  pw2f1o  7642  enfixsn  7646  sbthlem10  7656  sbth  7657  sbthcl  7659  domunsn  7687  fodomr  7688  pwdom  7689  canth2  7690  canth2g  7691  domssex  7698  xpf1o  7699  mapen  7701  mapunen  7706  map2xp  7707  mapdom2  7708  mapdom3  7709  ssenen  7711  infensuc  7715  nneneq  7720  php  7721  php2  7722  php3  7723  sucdom2  7734  1sdom  7742  unxpdomlem2  7745  unxpdomlem3  7746  isinf  7753  fineqv  7755  pssnn  7758  ssfi  7760  dif1enOLD  7772  dif1en  7773  findcard  7779  findcard2  7780  findcard2s  7781  ac6sfi  7784  frfi  7785  fimax2g  7786  unbnn2  7797  isfinite2  7798  xpfi  7811  domunfican  7813  fiint  7817  fodomfi  7819  fodomfib  7820  iunfi  7828  pwfilem  7834  ixpfi2  7838  fissuni  7845  fipreima  7846  finsschain  7847  ssfii  7899  fi0  7900  fiin  7902  dffi2  7903  fipwuni  7906  fisn  7907  elfiun  7910  dffi3  7911  fifo  7912  marypha1lem  7913  dfsup2  7922  dfsup2OLD  7923  ordiso2  7961  oismo  7986  hartogslem1  7988  hartogs  7990  wofib  7991  wemappo  7995  wemapsolem  7996  card2on  8001  brwdom  8014  brwdomn0  8016  brwdom2  8020  wdomtr  8022  wdompwdom  8025  canthwdom  8026  xpwdomg  8032  unxpwdom2  8035  ixpiunwdom  8038  zfregfr  8050  inf0  8059  inf3lema  8062  inf3lemd  8065  inf3lem1  8066  inf3lem2  8067  inf3lem3  8068  inf3lem5  8070  inf3lem6  8071  inf3lem7  8072  inf3  8073  infeq5  8075  omex  8081  dfom3  8085  dfom5  8088  infdifsn  8094  cantnffvalOLD  8103  cantnfval2  8109  cantnflt  8112  oemapso  8122  cantnflem1  8129  cantnfvalOLD  8138  cantnfval2OLD  8139  cantnfltOLD  8142  cantnflem1OLD  8152  wemapwe  8160  wemapweOLD  8161  cnfcom  8165  cnfcom3clem  8170  cnfcomOLD  8173  cnfcom3clemOLD  8178  epfrs  8183  tcvalg  8190  tctr  8192  tcmin  8193  r1sdom  8213  r1val1  8225  tz9.12lem3  8228  tz9.13  8230  tz9.13g  8231  rankf  8233  unir1  8252  rankvalg  8256  rankonidlem  8267  r1val2  8276  bndrank  8280  ranklim  8283  r1pwOLD  8285  rankunb  8289  rankuni2b  8292  rankuni  8302  rankval4  8306  rankxplim  8318  rankxplim3  8320  rankxpsuc  8321  tcrank  8323  cp  8330  bnd2  8332  kardex  8333  karden  8334  cardf2  8345  tskwe  8352  cardlim  8374  harcard  8380  cardiun  8384  pm54.43  8402  r0weon  8411  infxpenlem  8412  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  fseqenlem1  8426  fseqenlem2  8427  fseqen  8429  dfac8alem  8431  dfac8clem  8434  ac10ct  8436  ween  8437  acnlem  8450  finacn  8452  acndom  8453  acndom2  8456  wdomfil  8463  infpwfien  8464  alephon  8471  alephcard  8472  alephordi  8476  cardaleph  8491  alephval3  8512  iunfictbso  8516  aceq3lem  8522  dfac3  8523  dfac4  8524  dfac5lem1  8525  dfac5lem2  8526  dfac5lem3  8527  dfac5lem4  8528  dfac5lem5  8529  dfac5  8530  dfac2a  8531  dfac2  8532  dfac8  8536  dfac9  8537  dfac10b  8540  acacni  8541  dfacacn  8542  dfac13  8543  kmlem1  8551  kmlem2  8552  kmlem9  8559  kmlem10  8560  kmlem11  8561  kmlem12  8562  kmlem13  8563  cdafn  8570  pwsdompw  8605  infmap2  8619  ackbij1lem5  8625  ackbij1lem8  8628  ackbij2  8644  cflm  8651  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cfflb  8660  cflim2  8664  cfss  8666  cfslb2n  8669  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  coftr  8674  sornom  8678  infpssr  8709  fin4en1  8710  enfin2i  8722  fin23lem26  8726  fin23lem14  8734  fin23lem16  8736  fin23lem17  8739  fin23lem21  8740  fin23lem32  8745  fin23lem34  8747  fin23lem39  8751  compssiso  8775  isf34lem4  8778  enfin1ai  8785  isfin1-3  8787  fin67  8796  dffin7-2  8799  fin1a2lem7  8807  fin1a2lem10  8810  fin1a2lem12  8812  fin1a2lem13  8813  fin12  8814  itunitc1  8821  itunitc  8822  ituniiun  8823  hsmexlem2  8828  hsmexlem4  8830  hsmex  8833  axcc2lem  8837  axcc3  8839  acncc  8841  fin41  8845  dominf  8846  dcomex  8848  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  ac9  8884  ac6s  8885  ac6sg  8889  ac9s  8894  numthcor  8895  zorn2lem1  8897  zorn2lem4  8900  zorn2lem7  8903  zorng  8905  zornn0g  8906  ttukeylem5  8914  ttukeylem6  8915  ttukeylem7  8916  axdclem  8920  axdclem2  8921  fodomg  8924  fodomb  8925  brdom3  8927  brdom5  8928  brdom4  8929  brdom7disj  8930  brdom6disj  8931  iunfo  8935  ondomon  8959  cardmin  8960  alephval2  8968  dominfac  8969  fpwwe2lem8  9036  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  fpwwe  9045  canthwe  9050  canthp1lem1  9051  pwfseqlem1  9057  pwfseqlem2  9058  pwfseqlem3  9059  pwfseqlem4a  9060  pwfseqlem5  9062  pwxpndom2  9064  gch2  9074  gchac  9080  inawinalem  9088  winainflem  9092  winalim2  9095  winafp  9096  gchina  9098  wunfi  9120  intwun  9134  wunex2  9137  uniwun  9139  eltsk2g  9150  inttsk  9173  inar1  9174  rankcf  9176  tskcard  9180  tskuni  9182  gruun  9205  intgru  9213  ingru  9214  wfgru  9215  grudomon  9216  gruina  9217  grur1a  9218  grur1  9219  grutsk  9221  axgroth2  9224  grothpw  9225  grothpwex  9226  axgroth6  9227  grothomex  9228  grothac  9229  axgroth3  9230  grothprim  9233  grothtsk  9234  inaprc  9235  nqereu  9328  nqerf  9329  dmrecnq  9367  ltaddnq  9373  genpnnp  9404  genpnmax  9406  genpcl  9407  nqpr  9413  addclprlem1  9415  mulclprlem  9418  distrlem4pr  9425  1idpr  9428  prlem934  9432  ltaddpr  9433  ltexprlem3  9437  ltexprlem4  9438  ltexprlem6  9440  ltexprlem7  9441  prlem936  9446  reclem2pr  9447  reclem3pr  9448  mulasssr  9488  ltsosr  9492  0idsr  9495  1idsr  9496  ltasr  9498  recexsrlem  9501  mulgt0sr  9503  supsrlem  9509  ltresr  9538  axmulass  9555  axrrecex  9561  axpre-lttri  9563  wloglei  10110  lbinfm  10521  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  dfnn2  10574  dflt2  11383  xrinfmss2  11531  infmxrgelb  11555  xrinfm0  11557  fzpr  11764  uzrdgfni  12069  axdc4uzlem  12092  axdc4uz  12093  mptnn0fsuppd  12104  seqval  12118  seqfeq4  12156  serle  12162  seqof  12164  hash1snb  12479  hashxplem  12491  hashmap  12493  hashpw  12494  hashfun  12495  hashbclem  12501  hashfacen  12503  hashf1lem1  12504  hashf1lem2  12505  hashf1  12506  fz1isolem  12510  hash2prde  12516  hash2prb  12517  hash2prd  12518  hash2prv  12525  hash2sspr  12526  brfi1uzind  12532  wrdexb  12558  ccatfn  12591  wrdind  12702  wrd2ind  12703  shftfval  12903  shftfib  12905  shftfn  12906  2shfti  12913  sqrlem6  13081  rexfiuz  13180  rlimdm  13374  fclim  13376  climshft  13399  fsumsplitsnun  13570  fsum2dlem  13585  fsumcom2  13589  fsum0diag2  13598  modfsummods  13607  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  incexclem  13648  isumltss  13660  supcvg  13667  ntrivcvg  13706  fprodfac  13777  fprod2dlem  13784  fprodcom2  13788  xpnnenOLD  13943  rpnnen2lem11  13958  algrf  14202  isprm2lem  14224  isprm2  14225  prmind2  14228  iserodd  14359  4sqlem12  14474  vdwlem10  14508  vdwlem13  14511  ramtlecl  14518  hashbc0  14523  ramval  14526  ramcl2lem  14527  ramub2  14532  0ram  14538  ram0  14540  ramub1lem1  14544  ramub1lem2  14545  ramub1  14546  restfn  14822  elrest  14825  prdsval  14852  prdsle  14859  prdsless  14860  prdsleval  14874  pwsle  14889  imasaddfnlem  14925  imasvscafn  14934  imasleval  14938  xpsc0  14957  xpsc1  14958  xpsfrnel2  14962  ismre  14987  fnmre  14988  fnmrc  15004  mrcfval  15005  mrisval  15027  mreexexlem4d  15044  isacs2  15050  mreacs  15055  acsfn  15056  acsfn1  15058  acsfn2  15060  cidffn  15075  comfeq  15101  invsym2  15157  oppcsect2  15169  brssc  15183  sscpwex  15184  isssc  15189  issubc  15204  isfuncd  15234  cofucl  15257  funcres2b  15266  funcpropd  15269  setcmon  15414  catcval  15423  xpcval  15446  xpccatid  15457  curf2ndf  15516  drsdirfi  15567  isdrs2  15568  joinfval  15631  joindmss  15637  meetfval  15645  meetdmss  15651  clatl  15746  odupos  15765  oduposb  15766  oduglb  15769  odulub  15771  posglbd  15780  ipoval  15784  ipolerval  15786  fpwipodrs  15794  ipodrsima  15795  isacs5lem  15799  psdmrn  15837  psssdm2  15845  mrcmndind  15997  pwsdiagmhm  16000  gsumwspan  16014  mulgpropd  16175  eqgfval  16249  eqgval  16250  gicsubgen  16326  gaid  16337  gaorb  16345  orbsta  16351  symgval  16404  symgbas  16405  symgplusg  16414  symg1bas  16421  gsmsymgrfix  16453  symgfixf1  16462  pmtrfval  16475  pmtrrn2  16485  symggen  16495  pmtrprfvalrn  16513  sylow1lem2  16619  sylow2alem1  16637  sylow2alem2  16638  sylow2a  16639  sylow2blem1  16640  sylow2blem2  16641  sylow2blem3  16642  sylow3lem1  16647  sylow3lem6  16652  efgval  16735  efgval2  16742  efgrelexlemb  16768  efgcpbllema  16772  efgcpbllemb  16773  vrgpfval  16784  frgpuplem  16790  qusabl  16871  abln0  16873  frgpnabllem1  16877  gsumval3OLD  16908  gsumval3lem2  16910  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  gsum2d2  17002  gsumcom2  17003  gsumxp  17004  gsumxpOLD  17006  telgsums  17022  dprdfadd  17060  dprdfaddOLD  17067  dprd2dlem1  17090  dprd2d2  17093  ablfac1eulem  17123  ringn0  17249  opprsubg  17285  subrgpropd  17463  lss1d  17609  pwsdiaglmhm  17703  pwssplit3  17707  lbsextlem4  17807  drngnidl  17877  lidldvgen  17903  psrbaglefi  18023  psrbaglefiOLD  18024  mplcoe1  18127  mplcoe5lem  18130  mplcoe5  18131  mplcoe2OLD  18133  ltbval  18136  ltbwe  18137  opsrle  18140  opsrtoslem1  18148  opsrtoslem2  18149  evlslem4OLD  18173  evlslem4  18174  mpfind  18205  coe1mul2  18310  coe1tm  18314  coe1fzgsumdlem  18343  pf1ind  18391  evl1gsumdlem  18392  znleval  18593  cssmre  18724  thlle  18728  pjfval2  18740  dsmmval  18765  islindf4  18873  lmisfree  18877  gsumcom3  18901  mat1dimelbas  18973  mat1f1o  18980  scmatscm  19015  mat1scmat  19041  mdetdiaglem  19100  mdetunilem7  19120  mdetunilem9  19122  madugsum  19145  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  istopon  19426  bastg  19467  tgdom  19480  distop  19497  indistopon  19502  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  fncld  19523  mretopd  19593  toponmre  19594  opnnei  19621  tgrest  19660  resttopon  19662  restco  19665  neitr  19681  ordtbas2  19692  ordtcnv  19702  ordtrest2  19705  pnfnei  19721  mnfnei  19722  iscnp2  19740  subbascn  19755  cnrest2  19787  cnpresti  19789  cnprest  19790  cnprest2  19791  ist1-3  19850  hausnei2  19854  fincmp  19893  cmpsublem  19899  cmpsub  19900  uncmp  19903  fiuncmp  19904  hauscmplem  19906  bwth  19910  bwthOLD  19911  dfcon2  19920  consuba  19921  cnconn  19923  uncon  19930  t1conperf  19937  1stcfb  19946  2ndcsb  19950  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  2ndcsep  19960  dis2ndc  19961  subislly  19982  restlly  19984  islly2  19985  hausllycmp  19995  cldllycmp  19996  lly1stc  19997  dislly  19998  hausmapdom  20001  dissnlocfin  20030  comppfsc  20033  kgenf  20042  iskgen3  20050  llycmpkgen2  20051  1stckgenlem  20054  1stckgen  20055  kgencn2  20058  txuni2  20066  txbas  20068  eltx  20069  ptpjpre1  20072  ptpjcn  20112  ptpjopn  20113  ptclsg  20116  dfac14  20119  xkoccn  20120  txcnp  20121  txcnmpt  20125  txrest  20132  txindis  20135  txlly  20137  txnlly  20138  pthaus  20139  txcmplem1  20142  txcmplem2  20143  hausdiag  20146  txlm  20149  tx1stc  20151  tx2ndc  20152  txkgen  20153  xkopt  20156  xkococnlem  20160  xkococn  20161  cnmpt1st  20169  cnmpt2nd  20170  xkofvcn  20185  xkoinjcn  20188  txcon  20190  imasnopn  20191  imasncld  20192  imasncls  20193  basqtop  20212  tgqtop  20213  hmphdis  20297  indishmph  20299  txhmeo  20304  pt1hmeo  20307  ptuncnv  20308  ptunhmeo  20309  xpstopnlem1  20310  ptcmpfi  20314  xkohmeo  20316  isfbas  20330  fbssfi  20338  trfbas2  20344  snfil  20365  fgcl  20379  filcon  20384  fbasrn  20385  trfil2  20388  cfinfil  20394  csdfil  20395  supfil  20396  zfbas  20397  isufil2  20409  acufl  20418  filufint  20421  fin1aufil  20433  rnelfmlem  20453  rnelfm  20454  fmfnfmlem3  20457  fmfnfmlem4  20458  fmfnfm  20459  ufldom  20463  flimrest  20484  hauspwpwf1  20488  txflf  20507  fclsrest  20525  fclscmp  20531  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem2  20553  ptcmplem3  20554  ptcmplem4  20555  cnextf  20566  cnextcn  20567  tmdgsum  20594  symgtgp  20600  cldsubg  20609  tgpconcomp  20611  qustgplem  20619  qustgphaus  20621  prdstmdd  20622  tsmsval2  20628  tsmssubm  20644  ustfn  20704  ustfilxp  20715  ustn0  20723  restutopopn  20741  ustuqtop0  20743  ustuqtop1  20744  ustuqtop2  20745  ustuqtop3  20746  ustuqtop4  20747  utopsnneiplem  20750  utopreg  20755  ucnimalem  20783  ucnima  20784  fmucndlem  20794  neipcfilu  20799  imasdsf1olem  20876  xpsdsval  20884  xmetec  20937  prdsbl  20994  stdbdxmet  21018  met1stc  21024  prdsxmslem2  21032  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  metustexhalfOLD  21066  metustexhalf  21067  metustfbasOLD  21068  metustfbas  21069  blval2  21078  metuel2  21082  metustblOLD  21083  metustbl  21084  restmetu  21090  xrtgioo  21311  xrsblre  21316  icccmplem1  21327  icccmplem2  21328  fsumcn  21374  fsum2cn  21375  cnllycmp  21456  isphtpc  21494  pi1blem  21539  iscmet3  21732  metcld2  21745  bcthlem4  21766  minveclem3b  21843  ovolfiniun  21912  ovoliunlem1  21913  ovoliunlem2  21914  finiunmbl  21954  volfiniun  21957  iundisj2  21959  uniioombllem3  21994  vitalilem2  22018  vitalilem3  22019  mbfimaopnlem  22062  itg1addlem4  22106  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  itgfsum  22233  ellimc2  22281  limcflf  22285  perfdvf  22307  dvres  22315  dvres2  22316  dvnff  22326  dvcj  22353  dvrec  22358  dvmptfsum  22376  dvef  22381  rolle  22391  dvivthlem1  22409  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem3  22429  ftc1cn  22444  vieta1lem2  22707  elqaalem2  22716  ulmdv  22798  logfac  22985  xrlimcnp  23298  jensenlem1  23316  jensenlem2  23317  wilthlem2  23343  prmorcht  23452  lgsquadlem1  23629  lgsquadlem2  23630  dchrisumlem3  23676  istrkg2ld  23858  ishpg  24128  umgraex  24323  isusgra0  24347  usgraop  24350  usgrac  24351  edgss  24352  usgra2edg  24382  usgrarnedg  24384  usgraedg4  24387  usgraedgreu  24388  usgraexmpl  24401  usgrafis  24415  nbgraf1olem5  24445  nb3graprlem1  24451  cusgrarn  24459  cusgrasize  24478  cusgrafilem1  24479  cusgrafilem2  24480  isuvtx  24488  wlkcompim  24526  wlkelwrd  24530  wlkntrllem2  24562  wlkntrl  24564  constr1trl  24590  2pthon  24604  dfconngra1  24671  wlkiswwlk2  24697  wwlkn0s  24705  wlknwwlknsur  24712  wlkiswwlksur  24719  clwlkcompim  24764  erclwwlkref  24813  erclwwlksym  24814  erclwwlktr  24815  erclwwlknref  24825  erclwwlknsym  24826  erclwwlkntr  24827  eclclwwlkn0  24831  eclclwwlkn1  24832  clwlkfoclwwlk  24845  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  usg2wlkonot  24883  usg2wotspth  24884  2wot2wont  24886  2spontn0vne  24887  2spot2iun2spont  24891  0egra0rgra  24936  rusgrasn  24945  rusgranumwlkb0  24953  eupath  24981  frisusgranb  24997  frgra3vlem1  25000  frgra3vlem2  25001  3vfriswmgralem  25004  2pthfrgra  25011  frg2woteq  25060  2spotiundisj  25062  usg2spot2nb  25065  frgraregord013  25118  friendship  25122  ex-natded9.26  25140  nvss  25486  vsfval  25528  h2hlm  25897  axhcompl-zf  25915  hlim2  26109  hhcmpl  26117  hhcms  26120  isch2  26141  helch  26161  hhsscms  26195  occl  26222  chintcli  26249  spanuni  26462  spansni  26475  elnlfn  26847  nmopun  26933  nlelchi  26980  cnlnssadj  26999  adjbd1o  27004  branmfn  27024  pjnmopi  27067  hmopidmchi  27070  foresf1o  27403  rabfodom  27404  abrexss  27410  iuninc  27428  disjabrex  27443  disjabrexf  27444  disjpreima  27445  disjxpin  27447  iundisj2f  27449  fcoinvbr  27461  br8d  27463  suppss2f  27477  fmptdF  27495  fmptcof2  27502  ofpreima  27507  funcnvmptOLD  27509  funcnvmpt  27510  dfcnv2  27517  1stpreima  27524  2ndpreima  27525  ctex  27531  resf1o  27553  fpwrelmapffslem  27555  xrge0infss  27580  iundisj2fi  27602  oduprs  27644  odutos  27651  tosglblem  27657  gsumle  27770  gsummpt2co  27771  gsumvsca1  27773  gsumvsca2  27774  fimaproj  27836  locfinreflem  27843  locfinref  27844  cmpcref  27853  ldlfcntref  27857  pstmxmet  27876  tpr2rico  27894  prsdm  27896  prsrn  27897  ordtcnvNEW  27902  ordtrest2NEW  27905  ordtconlem1  27906  esum0  28060  esumc  28062  esumcst  28071  esumfsup  28076  esumpfinvalf  28082  hasheuni  28091  sigaex  28109  isrnsigaOLD  28112  pwsiga  28130  sigainb  28136  insiga  28137  dmsigagen  28144  measbase  28168  ismeas  28170  isrnmeas  28171  measiuns  28188  measdivcstOLD  28195  measdivcst  28196  cntmeas  28197  ddemeas  28208  mbfmco2  28236  mbfmcnt  28239  br2base  28240  dya2iocrfn  28250  dya2iocct  28251  dya2iocnrect  28252  dya2iocucvr  28255  sxbrsigalem2  28257  oms0  28266  omsmon  28267  eulerpartlemb  28307  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemr  28313  eulerpartlemgvv  28315  eulerpartlemgh  28317  eulerpartlemgs2  28319  eulerpartlemn  28320  sseqf  28331  ballotlemsf1o  28452  ballotlemirc  28470  derangenlem  28615  subfacp1lem1  28623  subfacp1lem3  28626  subfacp1lem4  28627  subfacp1lem5  28628  erdszelem8  28642  erdsze2lem2  28648  kur14lem9  28658  ptpcon  28678  indispcon  28679  conpcon  28680  cnllyscon  28690  cvmsss2  28719  cvmcov2  28720  cvmliftlem15  28743  cvmlift2lem1  28747  cvmlift2lem12  28759  mrsubvrs  28882  msubff1  28916  mclsrcl  28921  mclsppslem  28943  ghomgrplem  29029  relexpindlem  29062  rtrclreclem.trans  29069  dfrtrcl2  29071  untsucf  29082  dfid4  29103  shftvalg  29115  dftr6  29179  coepr  29181  dffr5  29182  dfso2  29183  dfpo2  29184  br8  29185  br6  29186  br4  29187  dfres3  29188  cnvco1  29189  cnvco2  29190  eldm3  29191  pocnv  29193  socnv  29194  fundmpss  29196  fprb  29203  dfdm5  29206  dfrn5  29207  opelco3  29208  elima4  29209  setinds  29210  dfon2lem1  29215  dfon2lem3  29217  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  rdgprc  29227  dfrdg2  29228  dfpred3g  29255  predreseq  29259  predpo  29264  predbrg  29266  setlikespec  29267  predep  29272  preddowncl  29276  preduz  29280  predfz  29283  tz6.26  29285  trpredrec  29321  poseq  29333  soseq  29334  wfrlem5  29347  wfrlem10  29352  wfrlem12  29354  wfrlem13  29355  wzel  29380  wsuclem  29381  frrlem5  29391  frrlem11  29399  sltsolem1  29428  nofulllem5  29466  txpss3v  29528  brtxp  29530  brtxp2  29531  pprodss4v  29534  brpprod  29535  brpprod3a  29536  brpprod3b  29537  brsset  29539  idsset  29540  dfon3  29542  brtxpsd  29544  brbigcup  29548  dfbigcup2  29549  fobigcup  29550  elfix  29553  elfix2  29554  dffix2  29555  fixcnv  29558  dfom5b  29562  sscoid  29563  dffun10  29564  elfuns  29565  elfunsg  29566  elsingles  29568  fnsingle  29569  fvsingle  29570  dfiota3  29573  brimage  29576  brimageg  29577  funimage  29578  fnimage  29579  imageval  29580  brcart  29582  brdomaing  29585  brrangeg  29586  brimg  29587  brapply  29588  brcup  29589  brcap  29590  brsuccf  29591  funpartlem  29592  funpartfun  29593  funpartfv  29595  fullfunfv  29597  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  dfint3  29602  imagesset  29603  brlb  29605  altopelaltxp  29626  altxpsspw  29627  brsegle  29758  fvline  29794  liness  29795  ellines  29802  bpoly2  29819  bpoly3  29820  rankung  29823  ranksng  29824  rankelg  29825  rankpwg  29826  rankeq1o  29828  elhf2g  29833  hfext  29840  onsucconi  29902  finixpnum  30038  fin2solem  30039  fin2so  30040  supaddc  30041  supadd  30042  ptrest  30048  heicant  30049  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfresfi  30061  ftc1cnnc  30089  ftc1anclem6  30095  areacirclem5  30111  trer  30134  finminlem  30136  gtinf  30137  fneer  30171  fnessref  30175  refssfne  30176  neibastop1  30177  tailfb  30195  filnetlem2  30197  filnetlem3  30198  filnetlem4  30199  cover2g  30205  f1opr  30215  inixp  30219  indexdom  30225  frinfm  30226  sdclem2  30235  sdclem1  30236  fdc  30238  isbndx  30278  prdstotbnd  30290  heibor1lem  30305  heiborlem1  30307  heiborlem3  30309  heiborlem4  30310  heiborlem5  30311  heiborlem6  30312  heiborlem8  30314  heiborlem10  30316  ismrer1  30334  riscer  30391  divrngidl  30425  intidl  30426  isfldidl  30465  ispridlc  30467  sbccom2  30530  sbccom2f  30531  ac6s6  30580  ac6s6f  30581  prtlem10  30606  prtlem13  30609  prtlem16  30610  prtlem19  30619  prter2  30622  prter3  30623  elrfi  30626  ismrcd2  30631  istopclsd  30632  ismrc  30633  mrefg2  30639  isnacs3  30642  mzpclall  30659  mzpincl  30666  mzpsubst  30681  mzpcompact2lem  30684  mzpcompact2  30685  eldioph2lem1  30693  eldioph2lem2  30694  eldiophss  30708  diophrex  30709  rexrabdioph  30727  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  rabren3dioph  30749  fphpd  30750  rencldnfilem  30754  pellexlem5  30769  pellex  30771  rmxypairf1o  30847  monotuz  30877  monotoddzzfi  30878  oddcomabszz  30880  2nn0ind  30881  zindbi  30882  mzpcong  30910  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  setindtr  30966  setindtrs  30967  dford3lem2  30969  ttac  30978  pw2f1ocnv  30979  wepwsolem  30987  inisegn0  30989  dnnumch1  30990  fnwe2val  30995  fnwe2lem2  30997  aomclem1  31000  aomclem2  31001  aomclem6  31005  dfac11  31008  kelac2lem  31010  dfac21  31012  islssfg2  31017  lmhmlnmsplit  31033  pwslnmlem1  31038  pwslnm  31040  unxpwdom3  31041  dfacbasgrp  31057  lnr2i  31065  lnrfg  31068  rngunsnply  31122  acsfn1p  31148  idomsubgmo  31155  fgraphxp  31171  areaquad  31184  lcmgcdlem  31212  nzss  31222  expgrowth  31240  2sbc6g  31322  iotain  31324  compel  31347  ipo0  31358  ifr0  31359  fnchoice  31404  suprnmpt  31451  fzisoeu  31500  upbdrech  31505  infrglb  31584  fprodcllemf  31591  ellimcabssub0  31623  constlimc  31630  cncfiooicclem1  31696  fprodcncf  31704  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem31  31813  stoweidlem57  31839  stirlinglem13  31868  fourierdlem42  31931  fourierdlem80  31969  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  etransclem46  32063  funressnfv  32213  dfdfat2  32216  csbafv12g  32222  tz6.12-afv  32258  rlimdmafv  32262  csbaovg  32265  fsummmodsndifre  32347  fsummmodsnunz  32348  usgvincvadeu  32405  usgvincvadeuALT  32408  usgedgnlp  32410  usgfis  32446  usgfisALT  32450  tpres  32554  cicsym  32588  initoid  32611  termoid  32612  equivestrcsetc  32658  c0snmgmhm  32720  rngcvalOLD  32769  ringcvalOLD  32815  opeliun2xp  32922  dmmpt2ssx2  32926  gsumpr  32950  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  ply1mulgsum  32990  dflinc2  33011  lcosslsp  33039  lmod1zr  33094  lmodn0  33096  lvecpsslmod  33108  onfrALTlem5  33314  onfrALTlem4  33315  onfrALTlem3  33316  opelopab4  33324  ax6e2nd  33331  trsspwALT  33616  trsspwALT2  33617  trsspwALT3  33618  pwtrVD  33624  unipwrVD  33632  unipwr  33633  onfrALTlem5VD  33685  onfrALTlem4VD  33686  onfrALTlem3VD  33687  relopabVD  33701  ax6e2ndVD  33708  sspwimp  33718  sspwimpVD  33719  sspwimpcf  33720  sspwimpcfVD  33721  sspwimpALT  33725  sspwimpALT2  33728  ax6e2ndALT  33730  bnj23  33771  bnj62  33773  bnj219  33788  bnj610  33804  bnj918  33824  bnj927  33827  bnj976  33836  bnj1098  33842  bnj1379  33889  bnj110  33916  bnj98  33925  bnj154  33936  bnj155  33937  bnj535  33948  bnj556  33958  bnj557  33959  bnj591  33969  bnj594  33970  bnj580  33971  bnj607  33974  bnj609  33975  bnj600  33977  bnj849  33983  bnj893  33986  bnj908  33989  bnj934  33993  bnj944  33996  bnj964  34001  bnj966  34002  bnj969  34004  bnj970  34005  bnj910  34006  bnj986  34012  bnj999  34015  bnj1018  34020  bnj907  34023  bnj1039  34027  bnj1040  34028  bnj1052  34031  bnj1123  34042  bnj1030  34043  bnj1133  34045  bnj1128  34046  bnj1145  34049  bnj1204  34068  bnj1373  34086  bnj1417  34097  bnj1421  34098  bj-sbeq  34468  bj-sbel1  34472  bj-snsetex  34521  bj-snglc  34527  bj-0nelsngl  34529  bj-snglex  34531  bj-taginv  34544  bj-df-v  34583  renegclALT  34694  eqlkr2  34825  glbconxN  35102  pmapglbx  35493  pmapglb  35494  pclclN  35615  pclfinN  35624  polval2N  35630  pclfinclN  35674  osumcllem10N  35689  pexmidlem7N  35700  cdleme31sdnN  36113  cdlemefr44  36151  cdleme48fv  36225  cdleme46fvaw  36227  cdleme48bw  36228  cdleme46fsvlpq  36231  cdlemeg46fvcl  36232  cdlemeg49le  36237  cdlemeg46fjgN  36247  cdlemeg46fjv  36249  cdleme48d  36261  cdlemeg49lebilem  36265  cdleme50eq  36267  cdleme50f  36268  cdlemg2jlemOLDN  36319  cdlemg2klem  36321  cdlemk40  36643  cdlemk56  36697  diaglbN  36782  dvhlveclem  36835  dib1dim  36892  dibglbN  36893  diblss  36897  diblsmopel  36898  dicelvalN  36905  diclspsn  36921  cdlemn7  36930  dihordlem7  36941  dihopelvalcpre  36975  xihopellsmN  36981  dihopellsm  36982  dih1  37013  dihmeetlem1N  37017  dihglblem5apreN  37018  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetlem4preN  37033  dihmeetlem13N  37046  dih1dimatlem  37056  dihatlat  37061  dihjatcclem4  37148  pwinfi  37749  cllem0  37751  superficl  37752  superuncl  37753  ssficl  37754  ssuncl  37755  ssdifcl  37756  sssymdifcl  37757  elimaint  37764  elintima  37765  intima0  37767  trficl  37779  trclubg  37785  cotr2g  37786  dfhe3  37799  snhesn  37809  psshepw  37811  frege55lem2c  37944  frege55c  37945  frege72  37963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator