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

Theorem vex 2793
Description: All set variables are sets (see isset 2794). 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 2285 . 2  |-  x  =  x
2 df-v 2792 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2392 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 200 1  |-  x  e. 
_V
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686   _Vcvv 2790
This theorem is referenced by:  isset  2794  ralv  2803  rexv  2804  reuv  2805  rmov  2806  rabab  2807  sbhypf  2835  ceqex  2900  ralab  2928  rexab  2930  moeq3  2944  mo2icl  2946  reu8  2963  sbc2or  3001  csbvarg  3110  csbiebg  3122  sbcnestgf  3130  sbnfc2  3143  ddif  3310  csbing  3378  dfun2  3406  dfin2  3407  vn0  3464  eqv  3472  abvor0  3474  sbss  3565  csbifg  3595  ifexg  3626  elpwg  3634  dftp2  3681  prnzg  3748  snssg  3756  difprsn  3758  sneqrg  3784  preq12bg  3793  pwpr  3825  pwtp  3826  pwv  3828  unipr  3843  uniprg  3844  unisng  3846  elintg  3872  elintrabg  3877  intss1  3879  ssint  3880  intmin  3884  intss  3885  intssuni  3886  intmin4  3893  intab  3894  intun  3896  intpr  3897  intprg  3898  uniintsn  3901  iinconst  3916  iuniin  3917  iinss1  3919  dfiin2g  3938  ssiinf  3953  iinss  3955  iinss2  3956  0iin  3962  iinab  3965  iinun2  3970  iundif2  3971  iindif2  3973  iinin2  3974  iinuni  3987  sspwuni  3989  iinpw  3992  iunpwss  3993  brab1  4070  csbopabg  4096  mptv  4114  trint  4130  trintss  4131  vprc  4154  inex1g  4159  ssexg  4162  intex  4169  inuni  4175  axpweq  4189  pwexg  4196  pwuni  4208  axpr  4215  zfpair2  4217  elALT  4220  rext  4224  sspwb  4225  unipw  4226  ssextss  4229  nnullss  4237  exss  4238  opth  4247  opthg  4248  copsexg  4254  copsex4g  4257  moop2  4263  euotd  4269  opelopabsbOLD  4275  opelopabsb  4277  pwin  4299  pwunss  4300  pwssun  4301  pwundifOLD  4303  epelg  4308  epel  4310  dfid3  4312  pofun  4332  epse  4378  wefrc  4389  tron  4417  onfr  4433  sucel  4467  suctr  4477  uniexg  4519  unexb  4522  snnex  4526  uniuni  4529  eusvnf  4531  eusvnfb  4532  reusv6OLD  4547  iunpw  4572  onint  4588  ordpwsuc  4608  unon  4624  ordunisuc  4625  onuninsuci  4633  orduninsuc  4636  limsssuc  4643  limuni3  4645  tfinds  4652  tfindsg  4653  tfindsg2  4654  tfinds2  4656  dfom2  4660  peano5  4681  finds  4684  findsg  4685  finds2  4686  0nelxp  4719  opelxp  4721  opeliunxp  4742  elvv  4750  elvvv  4751  elvvuni  4752  xpsspw  4799  xpsspwOLD  4800  relopabi  4813  opabid2  4817  difopab  4819  xpiindi  4823  ralxpf  4832  relop  4836  cnvco  4867  dfrn2  4870  dfdm4  4874  dmss  4880  dmin  4888  dmiun  4889  dmuni  4890  dm0  4894  dmi  4895  reldm0  4898  elreldm  4905  elrnmpt1  4930  dmrnssfld  4940  dmcoss  4946  dmcosseq  4948  opelresg  4964  resieq  4967  dmres  4978  elres  4992  relssres  4994  resopab  4998  resiexg  4999  iss  5000  dfres2  5004  dfima2  5016  csbima12g  5024  imadmrn  5026  imai  5029  elimasng  5041  args  5043  epini  5045  iniseg  5046  dffr3  5047  dfse2  5048  exse2  5049  cotr  5057  issref  5058  cnvsym  5059  intasym  5060  asymref  5061  asymref2  5062  intirr  5063  brcodir  5064  codir  5065  qfto  5066  poirr2  5069  cnvopab  5085  cnv0  5086  cnvi  5087  cnvdif  5089  rniun  5093  dminss  5097  imainss  5098  ssrnres  5118  rninxp  5119  dminxp  5120  cnvcnv3  5125  dfrel2  5126  dmsnn0  5140  dmsnopg  5146  cnvcnvsn  5152  dmsnsnsn  5153  cnvsng  5160  elxp4  5162  elxp5  5163  cnvresima  5164  dfco2  5174  dfco2a  5175  cores  5178  resco  5179  imaco  5180  rnco  5181  coiun  5184  co02  5188  coi1  5190  coass  5193  relssdmrn  5195  unielrel  5199  unixp0  5208  ressn  5213  cnviin  5214  cnvpo  5215  cnvso  5216  uniabio  5231  iotaval  5232  sniota  5248  csbiotag  5250  dffun2  5267  dffun7  5282  dffun8  5283  dffun9  5284  funopg  5288  funssres  5296  funun  5298  funcnvsn  5299  funcnv2  5311  funcnv  5312  funcnv3  5313  fun2cnv  5314  funcnvuni  5319  imadif  5329  isarep1  5333  2elresin  5357  fnres  5362  fcnvres  5420  fabexg  5424  fconstg  5430  fun11iun  5495  f1osng  5516  dffv3  5523  fv3  5543  fvres  5544  nfunsn  5560  funimass4  5575  ssimaexg  5587  dffv2  5594  dmfco  5595  fvopab6  5623  fndmdif  5631  iinpreima  5657  fvelrn  5663  dff3  5675  dffo4  5678  exfo  5680  f1ompt  5684  fmptco  5693  fsng  5699  dfmpt  5703  fnressn  5707  fressnfv  5709  fvsng  5716  zfrep6  5750  funfvima3  5757  idref  5761  fvclss  5762  fvresex  5764  abrexco  5768  opabex3  5771  imaiun  5773  dff13  5785  foeqcnvco  5806  f1eqcocnv  5807  fliftcnv  5812  isocnv2  5830  isomin  5836  isoini  5837  isofr  5841  isose  5842  f1oweALT  5853  wemoiso  5857  wemoiso2  5858  knatar  5859  oprabid  5884  csbovg  5891  eloprabga  5936  mpt2v  5939  caovmo  6059  f1opw  6074  ofmres  6118  op1stg  6134  op2ndg  6135  1stval2  6139  2ndval2  6140  fo1st  6141  fo2nd  6142  f1stres  6143  f2ndres  6144  fo1stres  6145  fo2ndres  6146  1st2val  6147  2nd2val  6148  xp1st  6151  xp2nd  6152  sbcopeq1a  6174  csbopeq1a  6175  eloprabi  6188  mpt2mptsx  6189  dmmpt2ssx  6191  fmpt2x  6192  ovmptss  6202  fmpt2co  6204  df1st2  6207  df2nd2  6208  1stconst  6209  2ndconst  6210  curry1  6212  curry2  6215  fparlem1  6220  fparlem2  6221  fpar  6224  fsplit  6225  frxp  6227  xporderlem  6228  soxp  6230  fnwelem  6232  fnse  6234  reldmtpos  6244  dmtpos  6248  rntpos  6249  ovtpos  6251  dftpos3  6254  dftpos4  6255  tpostpos  6256  porpss  6283  sorpss  6284  sorpsscmpl  6290  opiota  6292  opabiotafun  6293  opabiota  6295  riotav  6311  csbriotag  6319  onovuni  6361  smogt  6386  tfrlem3  6395  tfrlem8  6402  tfrlem9a  6404  tfrlem16  6411  tz7.44lem1  6420  rdg0g  6442  rdglim2  6447  tz7.48-1  6457  seqomlem1  6464  seqomlem2  6465  abianfplem  6472  oacl  6536  omcl  6537  oecl  6538  oa0r  6539  om0r  6540  om1r  6543  oe1m  6545  oaordi  6546  oawordri  6550  oawordeulem  6554  oalimcl  6560  oaass  6561  oarec  6562  omordi  6566  omwordri  6572  omlimcl  6578  odi  6579  omass  6580  omeulem1  6582  oen0  6586  oeordi  6587  oewordri  6592  oeworde  6593  oeoalem  6596  oeoelem  6598  nnawordex  6637  omabs  6647  omsmolem  6653  ercnv  6683  iserd  6688  eqerlem  6694  eqer  6695  ecdmn0  6704  erth  6706  erdisj  6709  qsss  6722  ecid  6726  qsid  6727  iiner  6733  qsel  6740  erovlem  6756  ecopovsym  6762  ecopovtrn  6763  ecopover  6764  mapprc  6778  fnmap  6781  fnpm  6782  mapval2  6799  pmsspw  6804  mapsn  6811  mapsncnv  6816  ixpconstg  6827  ixpprc  6839  uniixp  6841  ixpin  6843  ixpiin  6844  resixpfo  6856  elixpsn  6857  ixpsnf1o  6858  boxriin  6860  boxcutc  6861  bren  6873  brdomg  6874  domen  6877  domeng  6878  idssen  6908  ener  6910  domtr  6916  ensn1g  6928  en1  6930  en1b  6931  fundmen  6936  fundmeng  6937  mapsnen  6940  unen  6945  domdifsn  6947  xpsnen  6948  xpsneng  6949  xpcomeng  6956  xpassen  6958  xpdom2  6959  xpdom2g  6960  domunsncan  6964  omxpenlem  6965  pw2f1o  6969  fopwdom  6972  sbthlem10  6982  sbth  6983  sbthcl  6985  domunsn  7013  fodomr  7014  pwdom  7015  canth2  7016  canth2g  7017  domssex  7024  xpf1o  7025  mapen  7027  mapunen  7032  map2xp  7033  mapdom2  7034  mapdom3  7035  ssenen  7037  infensuc  7041  nneneq  7046  php  7047  php2  7048  php3  7049  sucdom2  7059  1sdom  7067  unxpdomlem2  7070  unxpdomlem3  7071  isinf  7078  fineqvlem  7079  fineqv  7080  pssnn  7083  ssfi  7085  dif1enOLD  7092  dif1en  7093  findcard  7099  findcard2  7100  findcard2s  7101  ac6sfi  7103  frfi  7104  fimax2g  7105  unbnn2  7116  isfinite2  7117  xpfi  7130  domunfican  7131  fiint  7135  fodomfi  7137  fodomfib  7138  iunfi  7146  pwfilem  7152  ixpfi2  7156  fissuni  7162  fipreima  7163  finsschain  7164  fival  7168  ssfii  7174  fi0  7175  fiin  7177  dffi2  7178  fipwuni  7181  fisn  7182  elfiun  7185  dffi3  7186  fifo  7187  marypha1lem  7188  dfsup2  7197  dfsup2OLD  7198  ordiso2  7232  oismo  7257  hartogslem1  7259  hartogs  7261  wofib  7262  wemappo  7266  wemapso2lem  7267  card2on  7270  brwdom  7283  brwdomn0  7285  brwdom2  7289  wdomtr  7291  wdompwdom  7294  canthwdom  7295  xpwdomg  7301  unxpwdom2  7304  ixpiunwdom  7307  elirrv  7313  zfregfr  7318  inf0  7324  inf3lema  7327  inf3lemd  7330  inf3lem1  7331  inf3lem2  7332  inf3lem3  7333  inf3lem5  7335  inf3lem6  7336  inf3lem7  7337  inf3  7338  infeq5  7340  omex  7346  dfom3  7350  dfom5  7353  infdifsn  7359  cantnfdm  7367  cantnfval  7371  cantnfval2  7372  cantnflt  7375  cantnff  7377  oemapso  7386  cantnflem1  7393  wemapwe  7402  cnfcom  7405  cnfcom3clem  7410  epfrs  7415  tcvalg  7425  tctr  7427  tcmin  7428  r1sdom  7448  r1val1  7460  tz9.12lem1  7461  tz9.12lem3  7463  tz9.13  7465  tz9.13g  7466  rankf  7468  unir1  7487  rankvalg  7491  rankonidlem  7502  r1val2  7511  bndrank  7515  ranklim  7518  r1pwOLD  7520  rankunb  7524  rankuni2b  7527  rankuni  7537  rankval4  7541  rankxplim  7551  rankxplim3  7553  rankxpsuc  7554  tcrank  7556  cp  7563  bnd2  7565  kardex  7566  karden  7567  cardf2  7578  tskwe  7585  cardlim  7607  harcard  7613  cardiun  7617  pm54.43  7635  r0weon  7642  infxpenlem  7643  infxpenc2lem2  7649  fseqenlem1  7653  fseqenlem2  7654  fseqen  7656  dfac8alem  7658  dfac8clem  7661  ac10ct  7663  ween  7664  acnlem  7677  finacn  7679  acndom  7680  acndom2  7683  wdomfil  7690  infpwfien  7691  alephon  7698  alephcard  7699  alephordi  7703  cardaleph  7718  alephval3  7739  iunfictbso  7743  aceq3lem  7749  dfac3  7750  dfac4  7751  dfac5lem1  7752  dfac5lem2  7753  dfac5lem3  7754  dfac5lem4  7755  dfac5lem5  7756  dfac5  7757  dfac2a  7758  dfac2  7759  dfac8  7763  dfac9  7764  dfac10b  7767  acacni  7768  dfacacn  7769  dfac13  7770  kmlem1  7778  kmlem2  7779  kmlem9  7786  kmlem10  7787  kmlem11  7788  kmlem12  7789  kmlem13  7790  cdafn  7797  pwsdompw  7832  infmap2  7846  ackbij1lem5  7852  ackbij1lem8  7855  ackbij2lem3  7869  ackbij2  7871  cflm  7878  cardcf  7880  cfeq0  7884  cfsuc  7885  cff1  7886  cfflb  7887  cfval2  7888  cflim2  7891  cfss  7893  cfslb2n  7896  cofsmo  7897  cfsmolem  7898  cfcoflem  7900  coftr  7901  sornom  7905  infpssr  7936  fin4en1  7937  fin23lem11  7945  enfin2i  7949  fin23lem26  7953  fin23lem14  7961  fin23lem16  7963  fin23lem17  7966  fin23lem21  7967  fin23lem32  7972  fin23lem34  7974  fin23lem39  7978  compsscnvlem  7998  compssiso  8002  isf34lem4  8005  enfin1ai  8012  isfin1-3  8014  fin67  8023  dffin7-2  8026  fin1a2lem7  8034  fin1a2lem10  8037  fin1a2lem12  8039  fin1a2lem13  8040  fin12  8041  itunitc1  8048  itunitc  8049  ituniiun  8050  hsmexlem2  8055  hsmexlem4  8057  hsmex  8060  axcc2lem  8064  axcc3  8066  acncc  8068  fin41  8072  dominf  8073  dcomex  8075  axdc2lem  8076  axdc3lem  8078  axdc3lem2  8079  axdc3lem4  8081  axdc4lem  8083  axcclem  8085  ac9  8112  ac6s  8113  ac6sg  8117  ac9s  8122  numthcor  8123  zorn2lem1  8125  zorn2lem4  8128  zorn2lem7  8131  zorng  8133  zornn0g  8134  ttukeylem5  8142  ttukeylem6  8143  ttukeylem7  8144  axdclem  8148  axdclem2  8149  fodomg  8152  fodomb  8153  brdom3  8155  brdom5  8156  brdom4  8157  brdom7disj  8158  brdom6disj  8159  iunfo  8163  ondomon  8187  cardmin  8188  alephval2  8196  dominfac  8197  fpwwe2lem1  8255  fpwwe2lem8  8261  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  fpwwe  8270  canthwe  8275  canthp1lem1  8276  pwfseqlem1  8282  pwfseqlem2  8283  pwfseqlem3  8284  pwfseqlem4a  8285  pwfseqlem5  8287  pwxpndom2  8289  gchac  8297  gch2  8303  inawinalem  8313  winainflem  8317  winalim2  8320  winafp  8321  gchina  8323  wunfi  8345  intwun  8359  wunex2  8362  uniwun  8364  eltsk2g  8375  inttsk  8398  inar1  8399  rankcf  8401  tskcard  8405  tskuni  8407  gruun  8430  intgru  8438  ingru  8439  wfgru  8440  grudomon  8441  gruina  8442  grur1a  8443  grur1  8444  grutsk  8446  axgroth5  8448  axgroth2  8449  grothpw  8450  grothpwex  8451  axgroth6  8452  grothomex  8453  grothac  8454  axgroth3  8455  grothprim  8458  grothtsk  8459  inaprc  8460  nqereu  8555  nqerf  8556  dmrecnq  8594  ltaddnq  8600  genpnnp  8631  genpnmax  8633  genpcl  8634  nqpr  8640  addclprlem1  8642  mulclprlem  8645  distrlem4pr  8652  1idpr  8655  prlem934  8659  ltaddpr  8660  ltexprlem3  8664  ltexprlem4  8665  ltexprlem6  8667  ltexprlem7  8668  prlem936  8673  reclem2pr  8674  reclem3pr  8675  mulasssr  8714  ltsosr  8718  0idsr  8721  1idsr  8722  ltasr  8724  recexsrlem  8727  mulgt0sr  8729  supsrlem  8735  ltresr  8764  axmulass  8781  axrrecex  8787  axpre-lttri  8789  wuncn  8794  renfdisj  8887  wloglei  9307  lbinfm  9709  supmul1  9721  supmullem1  9722  supmullem2  9723  supmul  9724  dfinfmr  9733  infmsup  9734  infmrgelb  9736  infmrlb  9737  dfnn2  9761  dflt2  10484  xrinfmss2  10631  infmxrgelb  10655  xrinfm0  10657  fzpr  10842  uzrdgfni  11023  axdc4uzlem  11046  axdc4uz  11047  seqval  11059  seqfeq4  11097  serle  11103  seqof  11105  hashxplem  11387  hashmap  11389  hashpw  11390  hashfun  11391  hashbclem  11392  hashfacen  11394  hashf1lem1  11395  hashf1lem2  11396  hashf1  11397  fz1isolem  11401  ccatfn  11429  wrdexb  11451  wrdind  11479  shftfval  11567  shftfib  11569  shftfn  11570  2shfti  11577  sqrlem6  11735  rexfiuz  11833  rlimdm  12027  fclim  12029  climshft  12052  fsum2dlem  12235  fsumcom2  12239  fsum0diag2  12247  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  incexclem  12297  isumltss  12309  supcvg  12316  xpnnenOLD  12490  rpnnen2lem11  12505  algrf  12745  isprm2lem  12767  isprm2  12768  prmind2  12771  iserodd  12890  4sqlem12  13005  vdwmc  13027  vdwlem10  13039  vdwlem13  13042  ramtlecl  13049  hashbc0  13054  ramval  13057  ramcl2lem  13058  ramub2  13063  0ram  13069  ram0  13071  ramub1lem1  13075  ramub1lem2  13076  ramub1  13077  restfn  13331  elrest  13334  restsspw  13338  prdsval  13357  prdsle  13363  prdsless  13364  prdsleval  13378  pwsle  13393  imasaddfnlem  13432  imasvscafn  13441  imasleval  13445  xpsc0  13464  xpsc1  13465  xpsfrnel2  13469  ismre  13494  fnmre  13495  ismred  13506  mremre  13508  fnmrc  13511  mrcfval  13512  mrisval  13534  mreexexlem4d  13551  isacs2  13557  mreacs  13562  acsfn  13563  acsfn1  13565  acsfn2  13567  cidffn  13582  comfeq  13611  invsym2  13667  oppcsect2  13679  brssc  13693  sscpwex  13694  isssc  13699  issubc  13714  isfuncd  13741  cofucl  13764  funcres2b  13773  funcpropd  13776  setcmon  13921  catcval  13930  fnxpc  13952  xpcval  13953  xpccatid  13964  curf2ndf  14023  drsdirfi  14074  isdrs2  14075  clatl  14222  odupos  14241  oduposb  14242  oduglb  14245  odulub  14247  posglbd  14255  ipoval  14259  ipolerval  14261  fpwipodrs  14269  ipodrsima  14270  isacs5lem  14274  psdmrn  14318  psssdm2  14326  submacs  14444  pwsdiagmhm  14447  gsumwspan  14470  mulgpropd  14602  subgacs  14654  nsgacs  14655  eqgfval  14667  eqgval  14668  gicsubgen  14744  gaid  14755  gaorb  14763  orbsta  14769  symgval  14773  symgbas  14774  symgplusg  14778  sylow1lem2  14912  sylow2alem1  14930  sylow2alem2  14931  sylow2a  14932  sylow2blem1  14933  sylow2blem2  14934  sylow2blem3  14935  sylow3lem1  14940  sylow3lem3  14942  sylow3lem6  14945  efgval  15028  efgval2  15035  efgrelexlemb  15061  efgcpbllema  15065  efgcpbllemb  15066  vrgpfval  15077  frgpuplem  15083  divsabl  15159  frgpnabllem1  15163  gsumval3  15193  gsumzaddlem  15205  gsumzadd  15206  gsum2d  15225  gsum2d2  15227  gsumcom2  15228  gsumxp  15229  dprdfadd  15257  dprdres  15265  subgdmdprd  15271  dprd2dlem1  15278  dprd2d2  15281  ablfac1eulem  15309  pgpfac1lem5  15316  opprsubg  15420  subrgmre  15571  subsubrg2  15574  subrgpropd  15581  lss1d  15722  lssintcl  15723  lssmre  15725  lssacs  15726  pwsdiaglmhm  15816  islbs3  15910  lbsextlem4  15916  drngnidl  15983  lidldvgen  16009  psrbaglefi  16120  mplcoe1  16211  mplcoe2  16213  ltbval  16215  ltbwe  16216  opsrle  16219  opsrtoslem1  16227  opsrtoslem2  16228  evlslem4  16247  coe1mul2  16348  coe1tm  16351  znleval  16510  cssmre  16595  thlle  16599  pjfval2  16611  istopon  16665  tgval2  16696  bastg  16706  tgdom  16718  distop  16735  indistopon  16740  fctop  16743  cctop  16745  ppttop  16746  epttop  16748  fncld  16761  cldss2  16769  ntreq0  16816  discld  16828  mretopd  16831  toponmre  16832  neisspw  16846  opnnei  16859  tgrest  16892  resttopon  16894  restco  16897  restdis  16911  ordtbas2  16923  ordtcnv  16933  ordtrest2  16936  pnfnei  16952  mnfnei  16953  iscnp2  16971  subbascn  16986  cnntr  17006  cnrest2  17016  cnpresti  17018  cnprest  17019  cnprest2  17020  ist1-3  17079  hausnei2  17083  isnrm2  17088  dishaus  17112  cmpcovf  17120  fincmp  17122  cmpsublem  17128  cmpsub  17129  cmpcld  17131  uncmp  17132  fiuncmp  17133  hauscmplem  17135  cmpfi  17137  dfcon2  17147  consuba  17148  cnconn  17150  uncon  17157  t1conperf  17164  is1stc2  17170  1stcfb  17173  2ndcsb  17177  2ndc1stc  17179  1stcrest  17181  2ndcctbss  17183  2ndcdisj  17184  2ndcomap  17186  2ndcsep  17187  dis2ndc  17188  llyi  17202  nllyi  17203  nlly2i  17204  llynlly  17205  subislly  17209  restnlly  17210  restlly  17211  islly2  17212  llyrest  17213  llyidm  17216  nllyidm  17217  hausllycmp  17222  cldllycmp  17223  lly1stc  17224  dislly  17225  hausmapdom  17228  kgenf  17238  iskgen3  17246  llycmpkgen2  17247  1stckgenlem  17250  1stckgen  17251  kgencn2  17254  txuni2  17262  txbas  17264  eltx  17265  ptpjpre1  17268  ptuni2  17273  ptpjcn  17307  ptpjopn  17308  ptclsg  17311  dfac14  17314  xkoccn  17315  txcnp  17316  txcnmpt  17320  prdstopn  17324  txrest  17327  txdis  17328  txindis  17330  txdis1cn  17331  txlly  17332  txnlly  17333  pthaus  17334  txcmplem1  17337  txcmplem2  17338  hausdiag  17341  txlm  17344  tx1stc  17346  tx2ndc  17347  txkgen  17348  xkopt  17351  xkococnlem  17355  xkococn  17356  cnmpt1st  17364  cnmpt2nd  17365  xkofvcn  17380  xkoinjcn  17383  txcon  17385  qtoptop2  17392  qtopuni  17395  basqtop  17404  tgqtop  17405  hmphdis  17489  indishmph  17491  txhmeo  17496  pt1hmeo  17499  ptuncnv  17500  ptunhmeo  17501  xpstopnlem1  17502  ptcmpfi  17506  xkohmeo  17508  isfbas  17526  isfbas2  17532  fbssfi  17534  trfbas2  17540  isfild  17555  snfil  17561  elfg  17568  fgcl  17575  filcon  17580  fbasrn  17581  filuni  17582  trfil2  17584  cfinfil  17590  csdfil  17591  supfil  17592  zfbas  17593  isufil2  17605  filssufilg  17608  acufl  17614  filufint  17617  uffix  17618  ufinffr  17626  ufildr  17628  fin1aufil  17629  rnelfmlem  17649  rnelfm  17650  fmfnfmlem3  17653  fmfnfmlem4  17654  fmfnfm  17655  ufldom  17659  flimrest  17680  hauspwpwf1  17684  txflf  17703  fclsrest  17721  fclscmp  17727  alexsubb  17742  alexsubALTlem1  17743  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  alexsubALT  17747  ptcmplem2  17749  ptcmplem3  17750  ptcmplem4  17751  ptcmplem5  17752  tmdgsum  17780  symgtgp  17786  cldsubg  17795  tgpconcomp  17797  divstgplem  17805  divstgphaus  17807  prdstmdd  17808  tsmsval2  17814  tsmssubm  17827  imasdsf1olem  17939  xpsdsval  17947  xmetec  17982  prdsbl  18039  stdbdxmet  18063  met1stc  18069  prdsxmslem2  18077  dscopn  18098  xrtgioo  18314  xrsblre  18319  icccmplem1  18329  icccmplem2  18330  fsumcn  18376  fsum2cn  18377  cnllycmp  18456  isphtpc  18494  pi1blem  18539  iscmet3  18721  metcld2  18734  bcthlem4  18751  minveclem3b  18794  ovolfiniun  18862  ovoliunlem1  18863  ovoliunlem2  18864  finiunmbl  18903  volfiniun  18906  iundisj2  18908  uniioombllem3  18942  vitalilem2  18966  vitalilem3  18967  vitali  18970  mbfimaopnlem  19012  itg1addlem4  19056  mbfi1fseqlem4  19075  mbfi1fseqlem6  19077  itgfsum  19183  ellimc2  19229  limcflf  19233  perfdvf  19255  dvres  19263  dvres2  19264  dvnff  19274  dvcj  19301  dvrec  19306  dvmptfsum  19324  dvef  19329  rolle  19339  dvivthlem1  19357  dvfsumle  19370  dvfsumabs  19372  dvfsumlem2  19376  dvfsumlem3  19377  ftc1cn  19392  mpfind  19430  pf1ind  19440  vieta1lem2  19693  elqaalem2  19702  ulmdv  19782  logfac  19956  xrlimcnp  20265  jensenlem1  20283  jensenlem2  20284  jensen  20285  wilthlem2  20309  prmorcht  20418  lgsquadlem1  20595  lgsquadlem2  20596  dchrisumlema  20639  dchrisumlem3  20642  ex-natded9.26  20808  nvss  21151  vsfval  21193  h2hlm  21562  axhcompl-zf  21580  hlim2  21773  hhcmpl  21781  hhcms  21784  shex  21793  isch2  21805  helch  21825  hhsscms  21858  occl  21885  chintcli  21912  dfch2  21988  spanuni  22125  spansni  22138  elnlfn  22510  nmopun  22596  nlelchi  22643  cnlnssadj  22662  adjbd1o  22667  branmfn  22687  pjnmopi  22730  hmopidmchi  22733  abrexss  23042  ballotlem2  23049  ballotlemsf1o  23074  ballotlemirc  23092  iuninc  23160  suppss2f  23203  fmptdF  23223  fmptcof2  23231  funcnvmptOLD  23236  funcnvmpt  23237  tpr2rico  23298  ctex  23338  disjabrex  23361  disjabrexf  23362  disjpreima  23363  iundisj2fi  23366  iundisj2f  23368  disjdsct  23371  ishashinf  23391  esumel  23428  esum0  23430  esumc  23432  esumcst  23438  esumpfinvalf  23446  hasheuni  23455  sigaex  23472  sigaval  23473  isrnsigaOLD  23475  pwsiga  23493  sigainb  23499  insiga  23500  dmsigagen  23507  measbase  23530  ismeas  23532  isrnmeas  23533  measiuns  23546  measdivcstOLD  23553  measdivcst  23554  cntmeas  23555  mbfmco2  23572  mbfmcnt  23575  br2base  23576  coinfliplem  23681  dmgmseqn0  23698  derangenlem  23704  subfacp1lem1  23712  subfacp1lem3  23715  subfacp1lem4  23716  subfacp1lem5  23717  erdszelem7  23730  erdszelem8  23731  erdsze2lem2  23737  kur14lem9  23747  ptpcon  23766  indispcon  23767  conpcon  23768  cnllyscon  23778  rellyscon  23784  cvmsss2  23807  cvmcov2  23808  cvmliftlem15  23831  cvmlift2lem1  23835  cvmlift2lem12  23847  umgraex  23877  eupath  23907  ghomgrplem  23998  relexpindlem  24038  rtrclreclem.trans  24045  dfrtrcl2  24047  untsucf  24058  dftr6  24109  coepr  24111  dffr5  24112  dfso2  24113  dfpo2  24114  br8  24115  br6  24116  br4  24117  dfres3  24118  cnvco1  24119  cnvco2  24120  eldm3  24121  fundmpss  24124  fprb  24131  dfdm5  24134  dfrn5  24135  setinds  24136  dfon2lem1  24141  dfon2lem3  24143  dfon2lem6  24146  dfon2lem7  24147  dfon2lem8  24148  dfon2  24150  rdgprc  24153  dfrdg2  24154  predreseq  24181  predpo  24186  predbrg  24188  setlikespec  24189  predep  24194  preddowncl  24198  preduz  24202  predfz  24205  tz6.26  24207  trpredrec  24243  poseq  24255  soseq  24256  wfrlem5  24262  wfrlem10  24267  wfrlem12  24269  wfrlem13  24270  wfrlem14  24271  wfrlem16  24273  tfrALTlem  24278  frrlem5  24287  frrlem11  24295  sltsolem1  24324  nofulllem5  24362  txpss3v  24420  brtxp  24422  brtxp2  24423  pprodss4v  24426  brpprod  24427  brpprod3a  24428  brpprod3b  24429  brsset  24431  idsset  24432  dfon3  24434  brtxpsd  24436  brbigcup  24440  dfbigcup2  24441  fobigcup  24442  elfix  24445  elfix2  24446  dffix2  24447  fixcnv  24450  limitssson  24453  dfom5b  24454  dffun10  24455  elfuns  24456  elfunsg  24457  elsingles  24459  fnsingle  24460  fvsingle  24461  dfiota3  24464  brimage  24467  brimageg  24468  funimage  24469  fnimage  24470  imageval  24471  brcart  24473  brdomaing  24476  brrangeg  24477  brimg  24478  brapply  24479  brcup  24480  brcap  24481  brsuccf  24482  funpartfun  24483  funpartfv  24485  fullfunfv  24487  brrestrict  24489  dfrdg4  24490  tfrqfree  24491  altopelaltxp  24512  altxpsspw  24513  brsegle  24733  fvline  24769  liness  24770  ellines  24777  bpoly2  24794  bpoly3  24795  rankung  24798  ranksng  24799  rankelg  24800  rankpwg  24801  rankeq1o  24803  elhf2g  24808  hfext  24815  onsucconi  24878  supaddc  24927  supadd  24928  itg2addnclem  24933  itg2addnc  24935  areacirclem6  24941  tpssg  24943  fatesg  24967  eqvinopb  24976  copsexgb  24977  elo  25052  stcat  25055  splint  25059  domfldrefc  25068  ranfldrefc  25069  domrngref  25071  domintrefb  25074  restidsing  25087  prj1b  25090  prj3  25091  eloi  25097  elintabg  25101  domintrefc  25136  inttpemp  25150  mapmapmap  25159  injsurinj  25160  npincppr  25170  repfuntw  25171  repcpwti  25172  cbcpcp  25173  cbicp  25177  prjmapcp2  25181  dstr  25182  iscst4  25188  islatalg  25194  domrancur1c  25213  mnlmxl2  25280  defse3  25283  inpc  25288  inposet  25289  tolat  25297  toplat  25301  dfdir2  25302  prodeq3ii  25319  fprodser  25331  symgfo  25379  svs2  25498  inttop2  25526  sallnei  25540  nsn  25541  dmhmph  25544  rnhmph  25545  intopcoaconlem3b  25549  intopcoaconlem3  25550  qusp  25553  efilcp  25563  fgsb2  25566  bwt2  25603  dmrngcmp  25762  dualded  25794  ishomd  25801  vtarsuelt  25906  fnctartar  25918  fnctartar2  25919  dfiunv2  25927  prismorcset2  25929  domcatfun  25936  codcatfun  25945  idcatfun  25952  empklst  26020  fnckle  26056  pfsubkl  26058  pgapspf2  26064  isconcl5a  26112  isconcl5ab  26113  bosser  26178  pdiveql  26179  abhp2  26186  bhp2a  26187  cnvresimaOLD  26237  trer  26238  finminlem  26242  gtinf  26245  fneer  26299  fnessref  26304  refssfne  26305  islocfin  26307  comppfsc  26318  neibastop1  26319  neibastop2lem  26320  neibastop3  26322  topmeet  26324  topjoin  26325  neifg  26331  tailfb  26337  filnetlem2  26339  filnetlem3  26340  filnetlem4  26341  cover2g  26370  f1opr  26402  inixp  26410  indexdom  26424  frinfm  26427  sdclem2  26463  sdclem1  26464  fdc  26466  isbndx  26517  prdstotbnd  26529  heibor1lem  26544  heiborlem1  26546  heiborlem3  26548  heiborlem4  26549  heiborlem5  26550  heiborlem6  26551  heiborlem8  26553  heiborlem10  26555  ismrer1  26573  riscer  26630  divrngidl  26664  intidl  26665  isfldidl  26704  ispridlc  26706  prtlem10  26744  prtlem13  26747  prtlem16  26748  prtlem19  26757  prter2  26760  prter3  26761  ralxpmap  26772  elrfi  26780  ismrcd1  26784  ismrcd2  26785  istopclsd  26786  ismrc  26787  mrefg2  26793  isnacs3  26796  mzpclall  26816  mzpincl  26823  mzpsubst  26837  mzpcompact2lem  26840  mzpcompact2  26841  eldioph2lem1  26850  eldioph2lem2  26851  eldiophss  26865  diophrex  26866  rexrabdioph  26886  2rexfrabdioph  26888  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  rabren3dioph  26909  fphpd  26910  rencldnfilem  26914  pellexlem5  26929  pellex  26931  rmxypairf1o  27007  monotuz  27037  monotoddzzfi  27038  oddcomabszz  27040  2nn0ind  27041  zindbi  27042  mzpcong  27070  rmydioph  27118  rmxdioph  27120  expdiophlem2  27126  setindtr  27128  setindtrs  27129  dford3lem2  27131  ttac  27140  pw2f1ocnv  27141  wepwsolem  27149  inisegn0  27151  dnnumch1  27152  fnwe2val  27157  fnwe2lem2  27159  aomclem1  27162  aomclem2  27163  aomclem6  27167  dfac11  27171  kelac2lem  27173  dfac21  27175  islssfg2  27180  lmhmlnmsplit  27196  pwssplit3  27201  filnm  27203  pwslnmlem1  27205  pwslnm  27207  dsmmval  27211  frlmlbs  27260  unxpwdom3  27267  enfixsn  27268  dfacbasgrp  27284  islindf4  27319  lmisfree  27323  lnr2i  27331  lnrfg  27334  hbtlem6  27344  rngunsnply  27389  pmtrfval  27404  symggen  27422  gsumcom3  27465  acsfn1p  27518  sdrgacs  27520  idomsubgmo  27525  fgraphxp  27541  expgrowth  27563  2sbc6g  27626  iotain  27628  compel  27651  ipo0  27663  ifr0  27664  fnchoice  27711  infrglb  27733  stoweidlem31  27791  stoweidlem57  27817  stoweidlem62  27822  stirlinglem13  27846  funressnfv  28002  dfdfat2  28005  csbafv12g  28011  tz6.12-afv  28046  csbaovg  28051  isusgra0  28117  usgraexmpl  28144  isuvtx  28171  uvtx01vtx  28175  frgra3vlem1  28189  frgra3vlem2  28190  3vfriswmgralem  28193  onfrALTlem5  28363  onfrALTlem4  28364  onfrALTlem3  28365  opelopab4  28373  a9e2nd  28380  trsspwALT  28665  trsspwALT2  28666  trsspwALT3  28667  pwtrVD  28671  pwtrOLD  28672  unipwrVD  28681  unipwr  28682  onfrALTlem5VD  28734  onfrALTlem4VD  28735  onfrALTlem3VD  28736  relopabVD  28750  a9e2ndVD  28757  sspwimp  28767  sspwimpVD  28768  sspwimpcf  28769  sspwimpcfVD  28770  sspwimpALT  28774  sspwimpALT2  28778  a9e2ndALT  28780  bnj23  28817  bnj62  28819  bnj156  28829  bnj219  28834  bnj610  28849  bnj918  28869  bnj927  28873  bnj976  28882  bnj1098  28888  bnj1379  28936  bnj110  28963  bnj98  28972  bnj154  28983  bnj155  28984  bnj535  28995  bnj556  29005  bnj557  29006  bnj581  29013  bnj591  29016  bnj594  29017  bnj580  29018  bnj607  29021  bnj609  29022  bnj600  29024  bnj849  29030  bnj893  29033  bnj908  29036  bnj934  29040  bnj944  29043  bnj964  29048  bnj966  29049  bnj969  29051  bnj970  29052  bnj910  29053  bnj986  29059  bnj999  29062  bnj1018  29067  bnj907  29070  bnj1039  29074  bnj1040  29075  bnj1052  29078  bnj1123  29089  bnj1030  29090  bnj1133  29092  bnj1128  29093  bnj1145  29096  bnj1204  29115  bnj1373  29133  bnj1417  29144  bnj1421  29145  bnj1498  29164  eqlkr2  29363  glbconxN  29640  pmapglbx  30031  pmapglb  30032  pclclN  30153  pclfinN  30162  polval2N  30168  pclfinclN  30212  osumcllem10N  30227  pexmidlem7N  30238  cdleme31sdnN  30649  cdlemefr44  30687  cdleme48fv  30761  cdleme46fvaw  30763  cdleme48bw  30764  cdleme46fsvlpq  30767  cdlemeg46fvcl  30768  cdlemeg49le  30773  cdlemeg46fjgN  30783  cdlemeg46fjv  30785  cdleme48d  30797  cdlemeg49lebilem  30801  cdleme50eq  30803  cdleme50f  30804  cdlemg2jlemOLDN  30855  cdlemg2klem  30857  cdlemk40  31179  cdlemk56  31233  diaglbN  31318  dvhlveclem  31371  dib1dim  31428  dibglbN  31429  diblss  31433  diblsmopel  31434  dicelvalN  31441  diclspsn  31457  cdlemn7  31466  dihordlem7  31477  dihopelvalcpre  31511  xihopellsmN  31517  dihopellsm  31518  dih1  31549  dihmeetlem1N  31553  dihglblem5apreN  31554  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetlem4preN  31569  dihmeetlem13N  31582  dih1dimatlem  31592  dihatlat  31597  dihjatcclem4  31684  lcdlss  31882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-v 2792
  Copyright terms: Public domain W3C validator