Theorem nfv 1915

Description: If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Definition change. (Revised by Wolf Lammen, 12-Sep-2021.)

Assertion

Ref	Expression
nfv	⊢ Ⅎ𝑥𝜑

Distinct variable group:   𝜑,𝑥

Proof of Theorem nfv

Step	Hyp	Ref	Expression
1		ax5ea 1914	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
2	1	nfi 1789	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfvd  1916  cbvaldw  2342  cbval2v  2347  dvelimhw  2349  pm11.53  2350  19.12vv  2351  eeanv  2353  eeeanv  2354  ee4anv  2355  sbnf2  2362  exsb  2363  2exsb  2364  sbbibvv  2366  cbvsbvf  2367  cleljustALT2  2369  spimv  2394  spimev  2396  chvarv  2400  cbvalv  2404  cbvexv  2405  cbvald  2411  cbvaldva  2413  cbvexdva  2414  cbval2  2415  axc16i  2440  dvelimnf  2457  sbel2x  2478  sbiedv  2508  2sbiev  2509  sbid2v  2513  sbhb  2525  2sb8e  2534  nfmod2  2558  nfmodv  2559  mof  2563  mo4f  2567  euf  2576  sb8eulem  2598  cbvmow  2603  sbmo  2614  moexexvw  2628  moexexv  2639  2mo  2648  2mosOLD  2650  2eu6  2657  axextmo  2712  nulmo  2713  abbib  2805  cleqh  2865  nfcv  2898  nfeqd  2909  nfeld  2910  nfabdw  2920  nfabd  2921  dvelimdc  2923  nfcvf  2925  cleqf  2927  r19.29af  3245  rexbidvALT  3251  rexbidvaALT  3252  2ralbida  3259  r19.12  3285  reean  3286  cbvrexsvw  3288  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbvrexsvwOLD  3291  sbralieOLD  3324  cbvralf  3330  cbvralv  3334  cbvrexv  3335  cbvralsv  3336  cbvrexsv  3337  cbvrmow  3375  cbvreu  3391  cbvrmov  3393  cbvreuv  3394  cbvrabwOLD  3435  cbvrab  3439  cbvexeqsetf  3455  ceqsex2  3493  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  spc2ed  3555  rspct  3562  rspc  3564  rspce  3565  eqvincf  3604  elrab3t  3645  ralab2  3655  rexab2  3657  mob2  3673  mob  3675  reu2  3683  rmo4f  3693  reu2eqd  3694  cdeqab1  3730  nfcdeq  3735  sbcco  3766  cbvsbcv  3776  elrabsf  3786  sbc2iegf  3815  reu8nf  3827  rmo2  3837  rmo3  3839  rmoanimALT  3845  nfcsb1d  3871  nfcsbd  3874  csbiebt  3878  csbie2t  3887  cbvrabcsfw  3890  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  cbvralv2  3895  cbvrexv2  3896  rspc2vd  3897  dfssf  3924  rabss3d  4033  eqrrabd  4038  uniiunlem  4039  ab0orv  4335  ab0orvALT  4336  sbcnestgw  4375  sbcnestg  4380  sbnfc2  4391  r19.3rzvOLD  4457  r19.28zv  4459  r19.27zv  4464  2reu4lem  4476  nfifd  4509  reusngf  4631  reusng  4634  rexreusng  4636  reuprg0  4659  rabsnifsb  4679  euabsn  4683  nfunid  4869  eluniab  4877  nfint  4912  iuneqconst  4958  disjiun  5086  disjxun  5096  nfopabd  5166  cbvopab  5170  cbvopab1  5172  cbvopab1g  5173  cbvopab2  5174  cbvopab1s  5175  mpteq12da  5181  mpteq12f  5183  cbvmptf  5198  cbvmptfg  5199  axrep1  5225  axrep2  5227  axrep3  5228  axrep4OLD  5231  axrep5  5232  zfrepclf  5236  reusv2lem3  5345  reusv2lem4  5346  reusv2  5348  reusv3  5350  alxfr  5352  ralxfrALT  5360  axprlem3OLD  5373  axprlem4OLD  5374  axprlem5OLD  5375  copsex2t  5440  iunopeqop  5469  rexopabb  5476  opelopabaf  5492  nfso  5539  pofun  5550  isso2i  5569  nffr  5597  opeliunxp  5691  opeliun2xp  5692  opeliunxp2  5787  ralxpf  5795  dfdmf  5845  dfrnf  5899  elrnmpt1  5909  dfrel4  6149  reuop  6251  frpoinsg  6301  frpoins2g  6303  wfis2g  6313  nfiotadw  6451  nfiotad  6453  cbviotaw  6455  cbviota  6457  cbviotav  6458  sb8iota  6459  iota2d  6480  iota2  6481  dffun6f  6507  imadif  6576  isarep1  6581  isarep2  6582  fv3  6852  tz6.12f  6859  funimassd  6900  fvelimad  6901  feqmptdf  6904  fimarab  6908  opabiotafun  6914  funfv2f  6923  fvmptd  6948  fvmptd2f  6957  fvmptdv  6958  fvmptt  6961  fvopab5  6974  eqfnfv2f  6980  ralrnmptw  7039  ralrnmpt  7041  dffo3f  7051  f1ompt  7056  fompt  7063  ffnfv  7064  ffnfvf  7065  f1ossf1o  7073  fmptco  7074  elabrex  7188  elabrexg  7189  dff13f  7201  fsnex  7229  fliftfun  7258  cbvriotaw  7324  cbvriota  7328  cbvriotav  7329  riota2  7340  riotaeqimp  7341  riota5f  7343  oprabv  7418  nfoprab  7422  mpoeq123  7430  cbvoprab1  7445  cbvoprab2  7446  cbvoprab12  7447  cbvoprab3  7449  cbvmpox  7451  ralrnmpo  7497  ovmpodx  7509  ovmpodf  7514  ovmpodv  7515  ov3  7521  ovmpt3rab1  7616  ofrfval2  7643  onminex  7747  tfis  7797  tfis2  7799  tfisi  7801  tfinds  7802  tfindes  7805  findes  7842  fiun  7887  f1iun  7888  abrexex2g  7908  opabex3d  7909  opabex3rd  7910  opabex3  7911  dfoprab4f  8000  fmpox  8011  offval22  8030  ovmptss  8035  ralxpes  8078  ralxp3  8080  ralxp3es  8081  frpoins3xpg  8082  frpoins3xp3g  8083  opeliunxp2f  8152  tposoprab  8204  fvmpocurryd  8213  nffrecs  8225  tfr3  8330  nfrdg  8345  tz7.48-1  8374  tz7.49  8376  naddsuc2  8629  eqerlem  8671  erovlem  8752  mptelixpg  8875  boxcutc  8881  dom2lem  8931  xpf1o  9069  mapxpen  9073  findcard2  9091  pssnn  9095  nneneq  9132  ac6sfi  9186  fiint  9229  indexfi  9262  wdom2d  9487  ixpiunwdom  9497  cantnflem1  9600  nfttrcld  9621  setinds2  9662  frinsg  9665  frins2  9668  r1val1  9700  rankuni2b  9767  scottexs  9801  scott0s  9802  dfac8clem  9944  acni2  9958  aceq1  10029  dfac5lem5  10039  kmlem15  10077  infpssrlem4  10218  fin23lem27  10240  hsmexlem2  10339  hsmexlem4  10341  axcc3  10350  domtriomlem  10354  axdc3lem2  10363  axdc3lem4  10365  axdc4lem  10367  ac6c4  10393  zorn2lem4  10411  zorn2lem5  10412  iunfo  10451  iundom2g  10452  uniimadomf  10457  konigthlem  10481  axrepndlem2  10506  axunnd  10509  axpowndlem2  10511  axpowndlem4  10513  axregndlem2  10516  axacndlem5  10524  zfcndrep  10527  zfcndinf  10531  pwfseqlem4a  10574  pwfseqlem4  10575  tskuni  10696  gruiin  10723  reclem2pr  10961  dedekind  11298  dedekindle  11299  fimaxre3  12090  nn0ind-raph  12594  uzind4s  12823  nnwof  12829  lbzbi  12851  fzrevral  13530  rabssnn0fi  13911  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  fsuppmapnn0fiubex  13917  seqof2  13985  reuccatpfxs1  14672  cotr2g  14901  rlim2  15421  ello1mpt  15446  climeu  15480  o1compt  15512  summolem2a  15640  zsum  15643  sumss  15649  sumss2  15651  fsumcvg2  15652  fsumclf  15663  fsumsplitf  15667  fsumsplit1  15670  fsum2dlem  15695  fsum00  15723  o1fsum  15738  nfcprod1  15833  nfcprod  15834  prodmolem2a  15859  zprod  15862  fprod  15866  fprodntriv  15867  prodss  15872  fprodn0  15904  fprod2dlem  15905  fprodsplitf  15913  fprodsplit1f  15915  fprodle  15921  fprodmodd  15922  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  coprmprod  16590  coprmproddvdslem  16591  prmind2  16614  iserodd  16765  pcmpt  16822  pcmptdvds  16824  prmolefac  16976  mreexexd  17573  catpropd  17634  invfuc  17903  natpropd  17905  fucpropd  17906  initoeu2  17942  acsmapd  18479  nfchnd  18536  symgval  19302  gsumsnd  19883  gsumsnf  19884  gsumunsnfd  19888  gsummptf1o  19894  gsummpt1n0  19896  gsum2d2lem  19904  gsumcom2  19906  gsummptnn0fz  19917  dprd2d2  19977  rngqiprngimf1  21257  gsummoncoe1  22254  gsumply1eq  22255  mdetralt2  22555  mdetunilem2  22559  madugsum  22589  gsummatr01lem4  22604  cpmatmcllem  22664  cayleyhamilton1  22838  neiptopnei  23078  neiptopreu  23079  neitr  23126  fiuncmp  23350  iunconnlem  23373  iunconn  23374  2ndcdisj  23402  dissnlocfin  23475  elptr2  23520  ptbasfi  23527  ptcld  23559  ptcldmpt  23560  ptclsg  23561  ptcnplem  23567  ptcnp  23568  cnmpt11  23609  cnmpt21  23617  cnmptcom  23624  imasnopn  23636  imasncld  23637  imasncls  23638  xkocnv  23760  elmptrab  23773  isfildlem  23803  alexsubALTlem3  23995  cnextfvval  24011  utopsnneiplem  24193  isucn2  24224  cfilucfil  24505  blval2  24508  restmetu  24516  ovoliunlem3  25463  ovoliun  25464  ovoliun2  25465  ovoliunnul  25466  finiunmbl  25503  volfiniun  25506  iundisj  25507  iunmbl  25512  voliun  25513  iunmbl2  25516  mbfeqalem1  25600  mbfsup  25623  mbfinf  25624  mbflim  25627  itg2splitlem  25707  itg2split  25708  isibl2  25725  cbvitg  25735  itgeqa  25773  itgss3  25774  itgfsum  25786  itgabs  25794  itggt0  25803  itgcn  25804  limcmpt  25842  limciun  25853  dvmptfsum  25937  dvlipcn  25957  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem4  25994  dvfsumrlim  25996  dvfsum2  25999  itgsubst  26014  coeeq2  26205  dgrle  26206  ulmss  26364  leibpi  26910  rlimcnp  26933  rlimcnp2  26934  o1cxp  26943  lgamgulmlem2  26998  lgamgulmlem6  27002  fsumdvdscom  27153  lgseisenlem2  27345  2sqmo  27406  2sqreulem4  27423  dchrisumlema  27457  dchrisumlem2  27459  dchrisumlem3  27460  nosupbnd1  27684  nosupbnd2  27686  noinfbnd1  27699  noinfbnd2  27701  bdayiun  27913  bdaypw2n0bndlem  28461  istrkg2ld  28534  mpteleeOLD  28970  gropd  29106  grstructd  29107  clwwlknonclwlknonf1o  30439  dlwwlknondlwlknonf1o  30442  ex-natded9.26  30496  isch3  31318  atom1d  32430  chirred  32472  sbc2iedf  32541  rspc2daf  32542  19.9d2r  32546  opreu2reuALT  32553  mo5f  32565  reuxfrdf  32567  foresf1o  32581  elabreximdv  32588  iinabrex  32646  cbvdisjf  32648  disjorf  32656  disjabrex  32659  iundisjf  32666  disjunsn  32671  brabgaf  32686  ac6sf2  32702  dfimafnf  32716  2ndresdju  32729  fmptcof2  32737  acunirnmpt2  32740  acunirnmpt2f  32741  aciunf1lem  32742  aciunf1  32743  ofpreima  32745  funcnv5mpt  32748  funcnv4mpt  32749  fnpreimac  32751  padct  32799  f1od2  32800  fpwrelmap  32814  xrofsup  32849  iundisjfi  32878  nnindf  32902  nn0min  32903  fprodex01  32908  fsumiunle  32912  prodindf  32946  gsummpt2d  33134  gsummptf1od  33140  gsummptfsf1o  33145  gsumhashmul  33152  gsumwrd2dccat  33162  isarchiofld  33283  elrgspnsubrunlem2  33332  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem3  33498  nsgqusf1o  33499  elrspunidl  33511  elrspunsn  33512  deg1prod  33666  ply1gsumz  33682  ig1pmindeg  33685  mplvrpmga  33712  esplylem  33726  esplyfv1  33729  esplyind  33733  vieta  33738  exsslsb  33755  ply1degltdimlem  33781  fedgmullem2  33789  evls1fldgencl  33829  irngnzply1  33850  extdgfialglem2  33852  ply1annidllem  33860  algextdeglem6  33881  constrfin  33905  reff  33998  locfinreflem  33999  cmpcref  34009  zarclsiin  34030  zarcls  34033  zarcmplem  34040  ordtconnlem1  34083  qqhval2  34141  esumeq12dva  34191  esumeq2dv  34197  esumrnmpt  34211  esumpad  34214  esumpad2  34215  esumadd  34216  gsumesum  34218  esumlub  34219  esumsnf  34223  esumpr  34225  esumrnmpt2  34227  esumfzf  34228  esumfsup  34229  esumpcvgval  34237  esumpmono  34238  esumcocn  34239  hasheuni  34244  esumcvg  34245  esumgect  34249  esum2dlem  34251  esum2d  34252  esumiun  34253  ldsysgenld  34319  sigapildsyslem  34320  sigapildsys  34321  ldgenpisyslem1  34322  fiunelros  34333  measvunilem  34371  measvunilem0  34372  measvuni  34373  measiun  34377  measinblem  34379  voliune  34388  volfiniune  34389  volmeas  34390  ddemeas  34395  oms0  34456  omssubadd  34459  carsgclctunlem1  34476  carsggect  34477  omsmeas  34482  eulerpartlemgvv  34535  dstrvprob  34631  ballotlemodife  34657  reprsuc  34774  reprdifc  34786  breprexplema  34789  breprexplemc  34791  circlemethhgt  34802  hgt750lemd  34807  bnj919  34925  bnj1146  34949  bnj1379  34988  bnj1385  34990  bnj1400  34993  bnj1534  35011  bnj1542  35015  bnj110  35016  bnj121  35028  bnj124  35029  bnj130  35032  bnj207  35039  bnj571  35064  bnj605  35065  bnj580  35071  bnj607  35074  bnj611  35076  bnj873  35082  bnj849  35083  bnj900  35087  bnj916  35091  bnj1000  35099  bnj964  35101  bnj981  35108  bnj985v  35111  bnj985  35112  bnj1014  35119  bnj1123  35144  bnj1128  35148  bnj1228  35169  bnj1204  35170  bnj1279  35176  bnj1307  35181  bnj1321  35185  bnj1388  35191  bnj1398  35192  bnj1408  35194  bnj1417  35199  bnj1444  35201  bnj1445  35202  bnj1446  35203  bnj1449  35206  bnj1467  35212  bnj1489  35214  bnj1312  35216  bnj1497  35218  bnj1518  35222  bnj1525  35227  bnj1529  35228  dvelimalcased  35233  dvelimexcased  35235  axsepg2  35240  axsepg2ALT  35241  fineqvrep  35272  onvf1odlem2  35300  cvmcov  35459  untsucf  35906  dfon2lem1  35977  dfon2lem3  35979  finminlem  36514  weiunpo  36661  weiunso  36662  weiunfr  36663  weiunse  36664  regsfromregtr  36670  regsfromsetind  36671  bj-nexdvt  36901  bj-cbvaldv  37002  bj-cbval2vv  37004  bj-cbvex2vv  37005  bj-cbvaldvav  37006  bj-cbvexdvav  37007  ax11-pm2  37039  bj-dvelimdv  37054  bj-nfeel2  37057  bj-ceqsalv  37097  bj-vtocl  37119  bj-inrab2  37131  currysetlem  37148  currysetlem1  37150  bj-opabco  37395  mptsnunlem  37545  exlimim  37549  exellim  37551  topdifinfindis  37553  topdifinffinlem  37554  icorempo  37558  isbasisrelowllem1  37562  isbasisrelowllem2  37563  relowlssretop  37570  finxpreclem2  37597  finxpreclem6  37603  fvineqsneu  37618  fvineqsneq  37619  wl-euequf  37781  wl-sb8eut  37785  wl-issetft  37789  phpreu  37807  matunitlindflem2  37820  ptrest  37822  ptrecube  37823  poimirlem2  37825  poimirlem23  37846  poimirlem24  37847  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  heicant  37858  mbfposadd  37870  itgabsnc  37892  itggt0cn  37893  ftc1anclem5  37900  upixp  37932  indexa  37936  indexdom  37937  filbcmb  37943  sdclem2  37945  sdclem1  37946  fdc1  37949  totbndbnd  37992  sbcalf  38317  sbcexf  38318  scottexf  38371  scott0f  38372  eqrelf  38456  ralrmo3  38562  fsumshftd  39234  riotasv2d  39239  riotasv2s  39240  riotasv3d  39242  glbconxN  39660  pmapglbx  40051  pmapglb2xN  40054  cdleme26ee  40642  cdleme31sn  40662  cdleme31sn1  40663  cdlemefr29exN  40684  cdlemefs32sn1aw  40696  cdleme43fsv1snlem  40702  cdleme41sn3a  40715  cdleme32fva  40719  cdleme32d  40726  cdleme32f  40728  cdleme40m  40749  cdleme40n  40750  cdleme42b  40760  cdlemk36  41195  cdlemk38  41197  cdlemkid  41218  cdlemk19x  41225  cdlemk11t  41228  dihvalcqpre  41517  mapdheq  42010  hdmap1eq  42083  hdmapval2lem  42113  lcmineqlem9  42313  lcmineqlem12  42316  aks4d1p1p2  42346  mndmolinv  42371  primrootsunit1  42373  primrootsunit  42374  primrootspoweq0  42382  aks6d1c1p5  42388  aks6d1c3  42399  aks6d1c4  42400  aks6d1c1rh  42401  aks6d1c2lem4  42403  aks6d1c2  42406  deg1gprod  42416  sticksstones1  42422  sticksstones11  42432  sticksstones16  42438  sticksstones22  42444  aks6d1c6lem2  42447  aks6d1c6isolem1  42450  aks6d1c6isolem2  42451  bcled  42454  bcle2d  42455  aks6d1c7lem3  42458  aks6d1c7  42460  rhmqusspan  42461  grpods  42470  unitscyglem1  42471  unitscyglem2  42472  unitscyglem3  42473  unitscyglem4  42474  unitscyglem5  42475  nfa1w  42939  mzpexpmpt  43008  eq0rabdioph  43039  rexrabdioph  43057  rexfrabdioph  43058  elnn0rabdioph  43066  dvdsrabdioph  43073  fphpd  43079  monotuz  43204  monotoddzz  43206  oddcomabszz  43207  setindtr  43287  dford4  43292  wdom2d2  43298  aomclem6  43322  aomclem8  43324  flcidc  43433  areaquad  43479  unielss  43481  onsucf1lem  43532  oaun3lem1  43637  nadd1suc  43655  rababg  43836  ss2iundv  43922  cbviuneq12dv  43924  gneispace  44396  mnringvald  44475  mnringmulrcld  44490  nfscott  44501  scottabf  44502  scottab  44503  mnuprdlem4  44537  ismnushort  44563  binomcxplemdvsum  44617  binomcxplemnotnn0  44618  aaanv  44650  pm11.57  44651  pm11.58  44652  pm11.59  44653  pm11.71  44659  pm14.12  44683  ssralv2  44793  tratrb  44798  iunconnlem2  45196  modelaxreplem3  45242  modelaxrep  45243  permaxrep  45268  evth2f  45281  elunif  45282  fvelrnbf  45284  evthf  45293  fnchoice  45295  sumpair  45301  rfcnnnub  45302  refsum2cn  45304  uzwo4  45319  fiiuncl  45331  fiunicl  45333  elintdv  45345  ssd  45346  cbvmpo2  45362  cbvmpo1  45363  eliin2f  45369  eliuniin2  45385  cbvrabv2  45392  suprnmpt  45439  disjf1  45448  disjrnmpt2  45453  disjf1o  45456  disjinfi  45457  choicefi  45465  iunmapsn  45482  axccdom  45487  dmrelrnrel  45491  axccd  45494  fmptf  45504  rnmptlb  45508  rnmptbddlem  45509  rnmptbd2lem  45513  rnmptbdlem  45520  rnmptbd  45521  fmptff  45534  upbdrech  45574  ssfiunibd  45578  supxrgere  45599  iuneqfzuzlem  45600  supxrgelem  45603  supxrge  45604  suplesup  45605  infrpge  45617  xralrple2  45620  infxr  45632  infxrunb2  45633  infleinf  45637  xrralrecnnle  45648  xrralrecnnge  45655  supxrunb3  45664  supxrleubrnmpt  45671  infleinf2  45679  unb2ltle  45680  rexabslelem  45683  rexabsle  45684  allbutfiinf  45685  suprleubrnmpt  45687  infrnmptle  45688  infxrunb3rnmpt  45693  uzublem  45695  uzub  45696  supminfrnmpt  45710  infxrpnf  45711  supxrleubrnmptf  45716  infxrgelbrnmpt  45719  infrpgernmpt  45730  supminfxr2  45734  monoordxr  45747  monoord2xr  45749  caucvgbf  45754  cvgcaule  45756  rexanuz2nf  45757  iccshift  45785  iooshift  45789  iooiinicc  45809  iooiinioc  45823  fsummulc1f  45838  fsumnncl  45839  fsumf1of  45841  fsumiunss  45842  fsumreclf  45843  fsumlessf  45844  fsumsermpt  45846  fmul01  45847  fmuldfeqlem1  45849  fmuldfeq  45850  fmul01lt1lem1  45851  fmul01lt1lem2  45852  fmul01lt1  45853  fprodsplit1  45860  fprodexp  45861  fprodabs2  45862  mccllem  45864  mccl  45865  fprodcnlem  45866  fprodcn  45867  climexp  45872  climsuse  45875  climrecf  45876  climinff  45878  climaddf  45882  mullimc  45883  ellimcabssub0  45884  islptre  45886  climf  45889  mullimcf  45890  rexlim2d  45892  idlimc  45893  limcperiod  45895  limcrecl  45896  sumnnodd  45897  islpcn  45904  limsupre  45906  limcleqr  45909  neglimc  45912  addlimc  45913  0ellimcdiv  45914  limclner  45916  climsubmpt  45925  climreclf  45929  climf2  45931  fnlimcnv  45932  climeldmeqmpt  45933  clim2f2  45935  climfveqmpt  45936  fnlimfvre  45939  allbutfifvre  45940  climleltrp  45941  fnlimf  45943  fnlimabslt  45944  climfveqmpt3  45947  climeldmeqf  45948  limsupref  45950  limsupbnd1f  45951  climbddf  45952  climeqf  45953  climeldmeqmpt3  45954  limsuplesup  45964  limsuppnfd  45967  limsupub  45969  limsupres  45970  climinf2lem  45971  climinf2  45972  limsuppnf  45976  limsupubuzlem  45977  limsupubuz  45978  climinf2mpt  45979  climinfmpt  45980  climinf3  45981  limsupmnflem  45985  limsupmnf  45986  limsupequz  45988  limsupre2  45990  limsupmnfuzlem  45991  limsupmnfuz  45992  limsupequzmptf  45996  limsupre3lem  45997  limsupre3  45998  limsupre3uzlem  46000  limsupre3uz  46001  limsupreuz  46002  limsupvaluz2  46003  limsupreuzmpt  46004  supcnvlimsup  46005  climuzlem  46008  climuz  46009  climisp  46011  lmbr3  46012  climrescn  46013  climxrrelem  46014  climxrre  46015  liminfcl  46028  liminfval2  46033  limsup10exlem  46037  liminflelimsuplem  46040  limsupgtlem  46042  limsupgt  46043  climliminflimsupd  46066  liminfreuzlem  46067  liminfreuz  46068  liminfltlem  46069  liminflt  46070  limsupub2  46077  xlimpnfxnegmnf  46079  liminflbuz2  46080  liminfpnfuz  46081  liminflimsupxrre  46082  xlimmnfvlem1  46097  xlimmnfvlem2  46098  xlimmnfv  46099  xlimpnfvlem1  46101  xlimpnfvlem2  46102  xlimpnfv  46103  xlimmnf  46106  xlimpnf  46107  xlimmnfmpt  46108  xlimpnfmpt  46109  climxlim2lem  46110  dfxlim2  46113  cncfshift  46139  icccncfext  46152  cncficcgt0  46153  cncfiooicc  46159  cncfioobd  46162  fprodcncf  46165  fprodsubrecnncnvlem  46172  fprodaddrecnncnvlem  46174  dvmptmulf  46202  dvnmptdivc  46203  dvnmul  46208  dvmptfprodlem  46209  dvmptfprod  46210  dvnprodlem1  46211  dvnprodlem2  46212  iblsplitf  46235  iblspltprt  46238  itgioocnicc  46242  iblcncfioo  46243  itgspltprt  46244  itgperiod  46246  stoweidlem3  46268  stoweidlem14  46279  stoweidlem17  46282  stoweidlem19  46284  stoweidlem20  46285  stoweidlem26  46291  stoweidlem27  46292  stoweidlem28  46293  stoweidlem29  46294  stoweidlem31  46296  stoweidlem34  46299  stoweidlem35  46300  stoweidlem36  46301  stoweidlem39  46304  stoweidlem42  46307  stoweidlem43  46308  stoweidlem44  46309  stoweidlem46  46311  stoweidlem48  46313  stoweidlem49  46314  stoweidlem50  46315  stoweidlem51  46316  stoweidlem52  46317  stoweidlem53  46318  stoweidlem54  46319  stoweidlem56  46321  stoweidlem57  46322  stoweidlem59  46324  stoweidlem60  46325  stoweidlem61  46326  stoweidlem62  46327  stoweid  46328  wallispilem3  46332  stirlinglem13  46351  stirling  46354  fourierdlem16  46388  fourierdlem21  46393  fourierdlem22  46394  fourierdlem31  46403  fourierdlem39  46411  fourierdlem48  46419  fourierdlem51  46422  fourierdlem53  46424  fourierdlem68  46439  fourierdlem69  46440  fourierdlem71  46442  fourierdlem73  46444  fourierdlem77  46448  fourierdlem80  46451  fourierdlem81  46452  fourierdlem82  46453  fourierdlem83  46454  fourierdlem86  46457  fourierdlem87  46458  fourierdlem89  46460  fourierdlem91  46462  fourierdlem93  46464  fourierdlem94  46465  fourierdlem103  46474  fourierdlem104  46475  fourierdlem112  46483  fourierdlem113  46484  elaa2  46499  etransclem18  46517  etransclem22  46521  etransclem23  46522  etransclem32  46531  etransclem35  46534  etransclem44  46543  etransclem46  46545  etransclem48  46547  rrndistlt  46555  ioorrnopnlem  46569  saliuncl  46588  saliincl  46592  intsaluni  46594  salexct  46599  subsaliuncl  46623  sge00  46641  sge0revalmpt  46643  sge0sn  46644  sge0f1o  46647  sge0gerp  46660  sge0pnffigt  46661  sge0lefi  46663  sge0ltfirp  46665  sge0resrnlem  46668  sge0resplit  46671  sge0lempt  46675  sge0iunmptlemfi  46678  sge0p1  46679  sge0iunmptlemre  46680  sge0fodjrnlem  46681  sge0iunmpt  46683  sge0rpcpnf  46686  sge0ltfirpmpt2  46691  sge0isum  46692  sge0xp  46694  sge0ad2en  46696  sge0isummpt2  46697  sge0xaddlem1  46698  sge0xaddlem2  46699  sge0xadd  46700  sge0pnffsumgt  46707  sge0gtfsumgt  46708  sge0uzfsumgt  46709  sge0seq  46711  sge0reuz  46712  sge0reuzb  46713  iundjiun  46725  meadjiunlem  46730  meadjiun  46731  ismeannd  46732  voliunsge0lem  46737  meaiuninclem  46745  meaiunincf  46748  meaiuninc3v  46749  meaiuninc3  46750  meaiininclem  46751  meaiininc  46752  meaiininc2  46753  caragenfiiuncl  46780  omeiunltfirp  46784  carageniuncllem1  46786  carageniuncllem2  46787  caratheodorylem2  46792  0ome  46794  isomenndlem  46795  hoicvrrex  46821  ovnsupge0  46822  ovnlecvr  46823  ovnlerp  46827  ovncvrrp  46829  ovn0lem  46830  ovnsubaddlem1  46835  ovnsubaddlem2  46836  hoidmvcl  46847  hsphoidmvle2  46850  hsphoidmvle  46851  hoidmvval0  46852  sge0hsphoire  46854  hoidmvval0b  46855  hoidmv1lelem1  46856  hoidmv1lelem2  46857  hoidmv1lelem3  46858  hoidmvlelem1  46860  hoidmvlelem2  46861  hoidmvlelem3  46862  hoidmvlelem4  46863  hoidmvlelem5  46864  hoidmvle  46865  ovnhoilem1  46866  ovnhoilem2  46867  ovnhoi  46868  ovnlecvr2  46875  hspdifhsp  46881  hoidifhspdmvle  46885  hoiqssbllem3  46889  hspmbllem1  46891  hspmbllem2  46892  opnvonmbllem1  46897  opnvonmbllem2  46898  ovnsubadd2lem  46910  ovolval5lem1  46917  ovnovollem1  46921  ovnovollem2  46922  hoimbl2  46930  vonhoire  46937  iinhoiicclem  46938  iinhoiicc  46939  iunhoiioolem  46940  iunhoiioo  46941  vonioolem1  46945  vonioolem2  46946  vonioo  46947  vonicclem1  46948  vonicclem2  46949  vonicc  46950  vonn0ioo2  46955  vonn0icc2  46957  vonct  46958  pimltmnf2f  46962  pimgtpnf2f  46970  salpreimagelt  46972  salpreimalegt  46974  pimltpnf2f  46977  pimgtmnf2  46979  pimdecfgtioc  46980  pimincfltioc  46981  pimdecfgtioo  46982  pimincfltioo  46983  preimageiingt  46985  preimaleiinlt  46986  salpreimagtge  46990  salpreimaltle  46991  salpreimalelt  46994  salpreimagtlt  46995  issmff  46999  sssmf  47003  mbfresmf  47004  cnfsmf  47005  incsmflem  47006  incsmf  47007  smfsssmf  47008  issmflelem  47009  issmfle  47010  smfconst  47014  issmfgtlem  47020  issmfgt  47021  smfpimltxrmptf  47023  smfmbfcex  47025  smfaddlem1  47028  smfaddlem2  47029  smfadd  47030  decsmflem  47031  decsmf  47032  smfpreimagtf  47033  issmfgelem  47034  issmfge  47035  smflimlem2  47037  smflimlem4  47039  smflim  47042  smfpimgtxr  47045  smfpimgtxrmptf  47049  smfpimioo  47052  smfresal  47053  smfrec  47054  smfres  47055  smfmullem2  47057  smfmullem4  47059  smfmul  47060  smfpimbor1lem2  47064  smf2id  47066  smfco  47067  smflim2  47071  smfpimcc  47073  smflimmpt  47075  smfsuplem1  47076  smfsuplem3  47078  smfsup  47079  smfsupmpt  47080  smfsupxr  47081  smfinflem  47082  smfinf  47083  smfinfmpt  47084  smflimsuplem3  47087  smflimsuplem4  47088  smflimsuplem5  47089  smflimsuplem7  47091  smflimsuplem8  47092  smflimsup  47093  smflimsupmpt  47094  smfliminflem  47095  smfliminf  47096  smfliminfmpt  47097  smfpimne2  47105  fsupdm  47107  smfsupdmmbllem  47109  smfsupdmmbl  47110  finfdm  47111  smfinfdmmbllem  47113  smfinfdmmbl  47114  or2expropbilem1  47299  or2expropbilem2  47300  or2expropbi  47301  cfsetsnfsetf  47325  cfsetsnfsetfo  47327  rexsb  47366  reuf1odnf  47374  2reu8i  47380  ffnafv  47438  tz6.12c-afv2  47509  f1oresf1o2  47558  iccelpart  47700  iccpartdisj  47704  dfich2  47725  ichbi12i  47727  ichnfimlem  47730  ich2exprop  47738  ichnreuop  47739  ichreuopeq  47740  sprsymrelfo  47764  reupr  47789  reuopreuprim  47793  mogoldbb  48052  2zrngagrp  48516  2zrngmmgm  48519  cbvmpox2  48603  ovmpordx  48607  1arymaptfo  48910  2arymaptfo  48921  mo0sn  49082  iinfssclem3  49322  iinfssc  49323  iinfsubc  49324  infsubc2  49327  iinfconstbas  49332  isthincd2lem1  49691  nfintd  49939  nfiund  49940  nfiundg  49941  iunord  49942  spcdvw  49945  nfsetrecs  49952  setrec1lem2  49954  setrec1  49957  setrec2fun  49958  pgindnf  49982  pgind  49983  aacllem  50067