Theorem nfv 1916

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 1915	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
2	1	nfi 1790	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfvd  1917  cbvaldw  2343  cbval2v  2348  dvelimhw  2350  pm11.53  2351  19.12vv  2352  eeanv  2354  eeeanv  2355  ee4anv  2356  sbnf2  2363  exsb  2364  2exsb  2365  sbbibvv  2367  cbvsbvf  2368  cleljustALT2  2370  spimv  2395  spimev  2397  chvarv  2401  cbvalv  2405  cbvexv  2406  cbvald  2412  cbvaldva  2414  cbvexdva  2415  cbval2  2416  axc16i  2441  dvelimnf  2458  sbel2x  2479  sbiedv  2509  2sbiev  2510  sbid2v  2514  sbhb  2526  2sb8e  2535  nfmod2  2559  nfmodv  2560  mof  2564  mo4f  2568  euf  2577  sb8eulem  2599  cbvmow  2604  sbmo  2615  moexexvw  2629  moexexv  2640  2mo  2649  2mosOLD  2651  2eu6  2658  axextmo  2713  nulmo  2714  abbib  2806  cleqh  2866  nfcv  2899  nfeqd  2910  nfeld  2911  nfabdw  2921  nfabd  2922  dvelimdc  2924  nfcvf  2926  cleqf  2928  r19.29af  3247  rexbidvALT  3253  rexbidvaALT  3254  2ralbida  3261  r19.12  3287  reean  3288  cbvrexsvw  3290  cbvralsvwOLD  3291  sbralieOLD  3318  cbvralf  3323  cbvralv  3327  cbvrexv  3328  cbvralsv  3329  cbvrexsv  3330  cbvrmow  3368  cbvreu  3382  cbvrmov  3384  cbvreuv  3385  cbvrabwOLD  3426  cbvrab  3429  cbvexeqsetf  3445  ceqsex2  3482  vtocl2gaf  3523  vtocl2gafOLD  3524  vtocl3gaf  3525  vtocl3gafOLD  3526  spc2ed  3544  rspct  3551  rspc  3553  rspce  3554  eqvincf  3593  elrab3t  3634  ralab2  3644  rexab2  3646  mob2  3662  mob  3664  reu2  3672  rmo4f  3682  reu2eqd  3683  cdeqab1  3719  nfcdeq  3724  sbcco  3755  cbvsbcv  3765  elrabsf  3775  sbc2iegf  3804  reu8nf  3816  rmo2  3826  rmo3  3828  rmoanimALT  3834  nfcsb1d  3860  nfcsbd  3863  csbiebt  3867  csbie2t  3876  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  cbvralv2  3884  cbvrexv2  3885  rspc2vd  3886  dfssf  3913  rabss3d  4022  eqrrabd  4027  uniiunlem  4028  ab0orv  4324  ab0orvALT  4325  sbcnestgw  4364  sbcnestg  4369  sbnfc2  4380  r19.3rzvOLD  4445  r19.28zv  4447  r19.27zv  4452  2reu4lem  4464  nfifd  4497  reusngf  4619  reusng  4622  rexreusng  4624  reuprg0  4647  rabsnifsb  4667  euabsn  4671  nfunid  4857  eluniab  4865  nfint  4900  iuneqconst  4946  disjiun  5074  disjxun  5084  nfopabd  5154  cbvopab  5158  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  mpteq12da  5169  mpteq12f  5171  cbvmptf  5186  cbvmptfg  5187  axrep1  5213  axrep2  5215  axrep3  5216  axrep4OLD  5219  axrep5  5220  zfrepclf  5226  reusv2lem3  5335  reusv2lem4  5336  reusv2  5338  reusv3  5340  alxfr  5342  ralxfrALT  5350  axprlem3OLD  5364  axprlem4OLD  5365  axprlem5OLD  5366  copsex2t  5438  iunopeqop  5467  rexopabb  5474  opelopabaf  5490  nfso  5537  pofun  5548  isso2i  5567  nffr  5595  opeliunxp  5689  opeliun2xp  5690  opeliunxp2  5785  ralxpf  5793  dfdmf  5843  dfrnf  5897  elrnmpt1  5907  dfrel4  6147  reuop  6249  frpoinsg  6299  frpoins2g  6301  wfis2g  6311  nfiotadw  6449  nfiotad  6451  cbviotaw  6453  cbviota  6455  cbviotav  6456  sb8iota  6457  iota2d  6478  iota2  6479  dffun6f  6505  imadif  6574  isarep1  6579  isarep2  6580  fv3  6850  tz6.12f  6857  funimassd  6898  fvelimad  6899  feqmptdf  6902  fimarab  6906  opabiotafun  6912  funfv2f  6921  fvmptd  6947  fvmptd2f  6956  fvmptdv  6957  fvmptt  6960  fvopab5  6973  eqfnfv2f  6979  ralrnmptw  7038  ralrnmpt  7040  dffo3f  7050  f1ompt  7055  fompt  7062  ffnfv  7063  ffnfvf  7064  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  8029  ovmptss  8034  ralxpes  8077  ralxp3  8079  ralxp3es  8080  frpoins3xpg  8081  frpoins3xp3g  8082  opeliunxp2f  8151  tposoprab  8203  fvmpocurryd  8212  nffrecs  8224  tfr3  8329  nfrdg  8344  tz7.48-1  8373  tz7.49  8375  naddsuc2  8628  eqerlem  8670  erovlem  8751  mptelixpg  8874  boxcutc  8880  dom2lem  8930  xpf1o  9068  mapxpen  9072  findcard2  9090  pssnn  9094  nneneq  9131  ac6sfi  9185  fiint  9228  indexfi  9261  wdom2d  9486  ixpiunwdom  9496  cantnflem1  9599  nfttrcld  9620  setinds2  9661  frinsg  9664  frins2  9667  r1val1  9699  rankuni2b  9766  scottexs  9800  scott0s  9801  dfac8clem  9943  acni2  9957  aceq1  10028  dfac5lem5  10038  kmlem15  10076  infpssrlem4  10217  fin23lem27  10239  hsmexlem2  10338  hsmexlem4  10340  axcc3  10349  domtriomlem  10353  axdc3lem2  10362  axdc3lem4  10364  axdc4lem  10366  ac6c4  10392  zorn2lem4  10410  zorn2lem5  10411  iunfo  10450  iundom2g  10451  uniimadomf  10456  konigthlem  10480  axrepndlem2  10505  axunnd  10508  axpowndlem2  10510  axpowndlem4  10512  axregndlem2  10515  axacndlem5  10523  zfcndrep  10526  zfcndinf  10530  pwfseqlem4a  10573  pwfseqlem4  10574  tskuni  10695  gruiin  10722  reclem2pr  10960  dedekind  11298  dedekindle  11299  fimaxre3  12091  nn0ind-raph  12618  uzind4s  12847  nnwof  12853  lbzbi  12875  fzrevral  13555  rabssnn0fi  13937  fsuppmapnn0fiublem  13941  fsuppmapnn0fiub  13942  fsuppmapnn0fiubex  13943  seqof2  14011  reuccatpfxs1  14698  cotr2g  14927  rlim2  15447  ello1mpt  15472  climeu  15506  o1compt  15538  summolem2a  15666  zsum  15669  sumss  15675  sumss2  15677  fsumcvg2  15678  fsumclf  15689  fsumsplitf  15693  fsumsplit1  15696  fsum2dlem  15721  fsum00  15750  o1fsum  15765  nfcprod1  15862  nfcprod  15863  prodmolem2a  15888  zprod  15891  fprod  15895  fprodntriv  15896  prodss  15901  fprodn0  15933  fprod2dlem  15934  fprodsplitf  15942  fprodsplit1f  15944  fprodle  15950  fprodmodd  15951  lcmfunsnlem1  16595  lcmfunsnlem2lem1  16596  lcmfunsnlem2  16598  coprmprod  16619  coprmproddvdslem  16620  prmind2  16643  iserodd  16795  pcmpt  16852  pcmptdvds  16854  prmolefac  17006  mreexexd  17603  catpropd  17664  invfuc  17933  natpropd  17935  fucpropd  17936  initoeu2  17972  acsmapd  18509  nfchnd  18566  symgval  19335  gsumsnd  19916  gsumsnf  19917  gsumunsnfd  19921  gsummptf1o  19927  gsummpt1n0  19929  gsum2d2lem  19937  gsumcom2  19939  gsummptnn0fz  19950  dprd2d2  20010  rngqiprngimf1  21288  gsummoncoe1  22281  gsumply1eq  22282  mdetralt2  22582  mdetunilem2  22586  madugsum  22616  gsummatr01lem4  22631  cpmatmcllem  22691  cayleyhamilton1  22865  neiptopnei  23105  neiptopreu  23106  neitr  23153  fiuncmp  23377  iunconnlem  23400  iunconn  23401  2ndcdisj  23429  dissnlocfin  23502  elptr2  23547  ptbasfi  23554  ptcld  23586  ptcldmpt  23587  ptclsg  23588  ptcnplem  23594  ptcnp  23595  cnmpt11  23636  cnmpt21  23644  cnmptcom  23651  imasnopn  23663  imasncld  23664  imasncls  23665  xkocnv  23787  elmptrab  23800  isfildlem  23830  alexsubALTlem3  24022  cnextfvval  24038  utopsnneiplem  24220  isucn2  24251  cfilucfil  24532  blval2  24535  restmetu  24543  ovoliunlem3  25479  ovoliun  25480  ovoliun2  25481  ovoliunnul  25482  finiunmbl  25519  volfiniun  25522  iundisj  25523  iunmbl  25528  voliun  25529  iunmbl2  25532  mbfeqalem1  25616  mbfsup  25639  mbfinf  25640  mbflim  25643  itg2splitlem  25723  itg2split  25724  isibl2  25741  cbvitg  25751  itgeqa  25789  itgss3  25790  itgfsum  25802  itgabs  25810  itggt0  25819  itgcn  25820  limcmpt  25858  limciun  25869  dvmptfsum  25950  dvlipcn  25969  dvfsumlem2  26002  dvfsumlem4  26004  dvfsumrlim  26006  dvfsum2  26009  itgsubst  26024  coeeq2  26215  dgrle  26216  ulmss  26373  leibpi  26917  rlimcnp  26940  rlimcnp2  26941  o1cxp  26950  lgamgulmlem2  27005  lgamgulmlem6  27009  fsumdvdscom  27160  lgseisenlem2  27351  2sqmo  27412  2sqreulem4  27429  dchrisumlema  27463  dchrisumlem2  27465  dchrisumlem3  27466  nosupbnd1  27690  nosupbnd2  27692  noinfbnd1  27705  noinfbnd2  27707  bdayiun  27919  bdaypw2n0bndlem  28467  istrkg2ld  28540  mpteleeOLD  28976  gropd  29112  grstructd  29113  clwwlknonclwlknonf1o  30445  dlwwlknondlwlknonf1o  30448  ex-natded9.26  30502  isch3  31325  atom1d  32437  chirred  32479  sbc2iedf  32547  rspc2daf  32548  19.9d2r  32552  opreu2reuALT  32559  mo5f  32571  reuxfrdf  32573  foresf1o  32587  elabreximdv  32594  iinabrex  32652  cbvdisjf  32654  disjorf  32662  disjabrex  32665  iundisjf  32672  disjunsn  32677  brabgaf  32692  ac6sf2  32708  dfimafnf  32722  2ndresdju  32735  fmptcof2  32743  acunirnmpt2  32746  acunirnmpt2f  32747  aciunf1lem  32748  aciunf1  32749  ofpreima  32751  funcnv5mpt  32753  funcnv4mpt  32754  fnpreimac  32756  f1od2  32805  fpwrelmap  32819  xrofsup  32853  iundisjfi  32882  nnindf  32906  nn0min  32907  fprodex01  32911  fsumiunle  32915  prodindf  32935  gsummpt2d  33123  gsummptf1od  33129  gsummptfsf1o  33134  gsumhashmul  33141  suppgsumssiun  33146  gsumwrd2dccat  33152  isarchiofld  33273  elrgspnsubrunlem2  33322  nsgmgc  33485  nsgqusf1olem1  33486  nsgqusf1olem3  33488  nsgqusf1o  33489  elrspunidl  33501  elrspunsn  33502  deg1prod  33656  ply1gsumz  33672  ig1pmindeg  33675  mplvrpmga  33702  psrgsum  33705  psrmonprod  33709  esplylem  33723  esplyfv1  33726  esplyfval1  33730  esplyfvaln  33731  esplyind  33732  vieta  33737  exsslsb  33754  ply1degltdimlem  33780  fedgmullem2  33788  evls1fldgencl  33828  irngnzply1  33849  extdgfialglem2  33851  ply1annidllem  33859  algextdeglem6  33880  constrfin  33904  reff  33997  locfinreflem  33998  cmpcref  34008  zarclsiin  34029  zarcls  34032  zarcmplem  34039  ordtconnlem1  34082  qqhval2  34140  esumeq12dva  34190  esumeq2dv  34196  esumrnmpt  34210  esumpad  34213  esumpad2  34214  esumadd  34215  gsumesum  34217  esumlub  34218  esumsnf  34222  esumpr  34224  esumrnmpt2  34226  esumfzf  34227  esumfsup  34228  esumpcvgval  34236  esumpmono  34237  esumcocn  34238  hasheuni  34243  esumcvg  34244  esumgect  34248  esum2dlem  34250  esum2d  34251  esumiun  34252  ldsysgenld  34318  sigapildsyslem  34319  sigapildsys  34320  ldgenpisyslem1  34321  fiunelros  34332  measvunilem  34370  measvunilem0  34371  measvuni  34372  measiun  34376  measinblem  34378  voliune  34387  volfiniune  34388  volmeas  34389  ddemeas  34394  oms0  34455  omssubadd  34458  carsgclctunlem1  34475  carsggect  34476  omsmeas  34481  eulerpartlemgvv  34534  dstrvprob  34630  ballotlemodife  34656  reprsuc  34773  reprdifc  34785  breprexplema  34788  breprexplemc  34790  circlemethhgt  34801  hgt750lemd  34806  bnj919  34924  bnj1146  34947  bnj1379  34986  bnj1385  34988  bnj1400  34991  bnj1534  35009  bnj1542  35013  bnj110  35014  bnj121  35026  bnj124  35027  bnj130  35030  bnj207  35037  bnj571  35062  bnj605  35063  bnj580  35069  bnj607  35072  bnj611  35074  bnj873  35080  bnj849  35081  bnj900  35085  bnj916  35089  bnj1000  35097  bnj964  35099  bnj981  35106  bnj985v  35109  bnj985  35110  bnj1014  35117  bnj1123  35142  bnj1128  35146  bnj1228  35167  bnj1204  35168  bnj1279  35174  bnj1307  35179  bnj1321  35183  bnj1388  35189  bnj1398  35190  bnj1408  35192  bnj1417  35197  bnj1444  35199  bnj1445  35200  bnj1446  35201  bnj1449  35204  bnj1467  35210  bnj1489  35212  bnj1312  35214  bnj1497  35216  bnj1518  35220  bnj1525  35225  bnj1529  35226  dvelimalcased  35231  dvelimexcased  35233  axsepg2  35239  axsepg2ALT  35240  fineqvrep  35272  onvf1odlem2  35300  cvmcov  35459  untsucf  35906  dfon2lem1  35977  dfon2lem3  35979  finminlem  36514  weiunpo  36661  weiunso  36662  weiunfr  36663  weiunse  36664  axtcond  36674  regsfromregtco  36734  regsfromsetind  36735  bj-nexdvt  37001  bj-cbvaldv  37112  bj-cbval2vv  37114  bj-cbvex2vv  37115  bj-cbvaldvav  37116  bj-cbvexdvav  37117  ax11-pm2  37149  bj-dvelimdv  37164  bj-nfeel2  37167  bj-ceqsalv  37207  bj-vtocl  37229  bj-inrab2  37241  currysetlem  37258  currysetlem1  37260  bj-axseprep  37387  bj-axreprepsep  37388  bj-opabco  37508  mptsnunlem  37658  exlimim  37662  exellim  37664  topdifinfindis  37666  topdifinffinlem  37667  icorempo  37671  isbasisrelowllem1  37675  isbasisrelowllem2  37676  relowlssretop  37683  finxpreclem2  37710  finxpreclem6  37716  fvineqsneu  37731  fvineqsneq  37732  wl-euequf  37903  wl-sb8eut  37907  wl-issetft  37911  phpreu  37929  matunitlindflem2  37942  ptrest  37944  ptrecube  37945  poimirlem2  37947  poimirlem23  37968  poimirlem24  37969  poimirlem25  37970  poimirlem26  37971  poimirlem27  37972  poimirlem28  37973  heicant  37980  mbfposadd  37992  itgabsnc  38014  itggt0cn  38015  ftc1anclem5  38022  upixp  38054  indexa  38058  indexdom  38059  filbcmb  38065  sdclem2  38067  sdclem1  38068  fdc1  38071  totbndbnd  38114  sbcalf  38439  sbcexf  38440  scottexf  38493  scott0f  38494  eqrelf  38583  ralrmo3  38689  disjqmap2  39151  fsumshftd  39402  riotasv2d  39407  riotasv2s  39408  riotasv3d  39410  glbconxN  39828  pmapglbx  40219  pmapglb2xN  40222  cdleme26ee  40810  cdleme31sn  40830  cdleme31sn1  40831  cdlemefr29exN  40852  cdlemefs32sn1aw  40864  cdleme43fsv1snlem  40870  cdleme41sn3a  40883  cdleme32fva  40887  cdleme32d  40894  cdleme32f  40896  cdleme40m  40917  cdleme40n  40918  cdleme42b  40928  cdlemk36  41363  cdlemk38  41365  cdlemkid  41386  cdlemk19x  41393  cdlemk11t  41396  dihvalcqpre  41685  mapdheq  42178  hdmap1eq  42251  hdmapval2lem  42281  lcmineqlem9  42480  lcmineqlem12  42483  aks4d1p1p2  42513  mndmolinv  42538  primrootsunit1  42540  primrootsunit  42541  primrootspoweq0  42549  aks6d1c1p5  42555  aks6d1c3  42566  aks6d1c4  42567  aks6d1c1rh  42568  aks6d1c2lem4  42570  aks6d1c2  42573  deg1gprod  42583  sticksstones1  42589  sticksstones11  42599  sticksstones16  42605  sticksstones22  42611  aks6d1c6lem2  42614  aks6d1c6isolem1  42617  aks6d1c6isolem2  42618  bcled  42621  bcle2d  42622  aks6d1c7lem3  42625  aks6d1c7  42627  rhmqusspan  42628  grpods  42637  unitscyglem1  42638  unitscyglem2  42639  unitscyglem3  42640  unitscyglem4  42641  unitscyglem5  42642  nfa1w  43112  mzpexpmpt  43181  eq0rabdioph  43212  rexrabdioph  43230  rexfrabdioph  43231  elnn0rabdioph  43239  dvdsrabdioph  43246  fphpd  43252  monotuz  43377  monotoddzz  43379  oddcomabszz  43380  setindtr  43460  dford4  43465  wdom2d2  43471  aomclem6  43495  aomclem8  43497  flcidc  43606  areaquad  43652  unielss  43654  onsucf1lem  43705  oaun3lem1  43810  nadd1suc  43828  rababg  44009  ss2iundv  44095  cbviuneq12dv  44097  gneispace  44569  mnringvald  44648  mnringmulrcld  44663  nfscott  44674  scottabf  44675  scottab  44676  mnuprdlem4  44710  ismnushort  44736  binomcxplemdvsum  44790  binomcxplemnotnn0  44791  aaanv  44823  pm11.57  44824  pm11.58  44825  pm11.59  44826  pm11.71  44832  pm14.12  44856  ssralv2  44966  tratrb  44971  iunconnlem2  45369  modelaxreplem3  45415  modelaxrep  45416  permaxrep  45441  evth2f  45454  elunif  45455  fvelrnbf  45457  evthf  45466  fnchoice  45468  sumpair  45474  rfcnnnub  45475  refsum2cn  45477  uzwo4  45492  fiiuncl  45504  fiunicl  45506  elintdv  45518  ssd  45519  cbvmpo2  45535  cbvmpo1  45536  eliin2f  45542  eliuniin2  45558  cbvrabv2  45565  suprnmpt  45612  disjf1  45621  disjrnmpt2  45626  disjf1o  45629  disjinfi  45630  choicefi  45637  iunmapsn  45654  axccdom  45659  dmrelrnrel  45663  axccd  45666  fmptf  45676  rnmptlb  45680  rnmptbddlem  45681  rnmptbd2lem  45685  rnmptbdlem  45692  rnmptbd  45693  fmptff  45706  upbdrech  45746  ssfiunibd  45750  supxrgere  45771  iuneqfzuzlem  45772  supxrgelem  45775  supxrge  45776  suplesup  45777  infrpge  45789  xralrple2  45792  infxr  45804  infxrunb2  45805  infleinf  45809  xrralrecnnle  45820  xrralrecnnge  45827  supxrunb3  45836  supxrleubrnmpt  45842  infleinf2  45850  unb2ltle  45851  rexabslelem  45854  rexabsle  45855  allbutfiinf  45856  suprleubrnmpt  45858  infrnmptle  45859  infxrunb3rnmpt  45864  uzublem  45866  uzub  45867  supminfrnmpt  45881  infxrpnf  45882  supxrleubrnmptf  45887  infxrgelbrnmpt  45890  infrpgernmpt  45901  supminfxr2  45905  monoordxr  45918  monoord2xr  45920  caucvgbf  45925  cvgcaule  45927  rexanuz2nf  45928  iccshift  45956  iooshift  45960  iooiinicc  45980  iooiinioc  45994  fsummulc1f  46009  fsumnncl  46010  fsumf1of  46012  fsumiunss  46013  fsumreclf  46014  fsumlessf  46015  fsumsermpt  46017  fmul01  46018  fmuldfeqlem1  46020  fmuldfeq  46021  fmul01lt1lem1  46022  fmul01lt1lem2  46023  fmul01lt1  46024  fprodsplit1  46031  fprodexp  46032  fprodabs2  46033  mccllem  46035  mccl  46036  fprodcnlem  46037  fprodcn  46038  climexp  46043  climsuse  46046  climrecf  46047  climinff  46049  climaddf  46053  mullimc  46054  ellimcabssub0  46055  islptre  46057  climf  46060  mullimcf  46061  rexlim2d  46063  idlimc  46064  limcperiod  46066  limcrecl  46067  sumnnodd  46068  islpcn  46075  limsupre  46077  limcleqr  46080  neglimc  46083  addlimc  46084  0ellimcdiv  46085  limclner  46087  climsubmpt  46096  climreclf  46100  climf2  46102  fnlimcnv  46103  climeldmeqmpt  46104  clim2f2  46106  climfveqmpt  46107  fnlimfvre  46110  allbutfifvre  46111  climleltrp  46112  fnlimf  46114  fnlimabslt  46115  climfveqmpt3  46118  climeldmeqf  46119  limsupref  46121  limsupbnd1f  46122  climbddf  46123  climeqf  46124  climeldmeqmpt3  46125  limsuplesup  46135  limsuppnfd  46138  limsupub  46140  limsupres  46141  climinf2lem  46142  climinf2  46143  limsuppnf  46147  limsupubuzlem  46148  limsupubuz  46149  climinf2mpt  46150  climinfmpt  46151  climinf3  46152  limsupmnflem  46156  limsupmnf  46157  limsupequz  46159  limsupre2  46161  limsupmnfuzlem  46162  limsupmnfuz  46163  limsupequzmptf  46167  limsupre3lem  46168  limsupre3  46169  limsupre3uzlem  46171  limsupre3uz  46172  limsupreuz  46173  limsupvaluz2  46174  limsupreuzmpt  46175  supcnvlimsup  46176  climuzlem  46179  climuz  46180  climisp  46182  lmbr3  46183  climrescn  46184  climxrrelem  46185  climxrre  46186  liminfcl  46199  liminfval2  46204  limsup10exlem  46208  liminflelimsuplem  46211  limsupgtlem  46213  limsupgt  46214  climliminflimsupd  46237  liminfreuzlem  46238  liminfreuz  46239  liminfltlem  46240  liminflt  46241  limsupub2  46248  xlimpnfxnegmnf  46250  liminflbuz2  46251  liminfpnfuz  46252  liminflimsupxrre  46253  xlimmnfvlem1  46268  xlimmnfvlem2  46269  xlimmnfv  46270  xlimpnfvlem1  46272  xlimpnfvlem2  46273  xlimpnfv  46274  xlimmnf  46277  xlimpnf  46278  xlimmnfmpt  46279  xlimpnfmpt  46280  climxlim2lem  46281  dfxlim2  46284  cncfshift  46310  icccncfext  46323  cncficcgt0  46324  cncfiooicc  46330  cncfioobd  46333  fprodcncf  46336  fprodsubrecnncnvlem  46343  fprodaddrecnncnvlem  46345  dvmptmulf  46373  dvnmptdivc  46374  dvnmul  46379  dvmptfprodlem  46380  dvmptfprod  46381  dvnprodlem1  46382  dvnprodlem2  46383  iblsplitf  46406  iblspltprt  46409  itgioocnicc  46413  iblcncfioo  46414  itgspltprt  46415  itgperiod  46417  stoweidlem3  46439  stoweidlem14  46450  stoweidlem17  46453  stoweidlem19  46455  stoweidlem20  46456  stoweidlem26  46462  stoweidlem27  46463  stoweidlem28  46464  stoweidlem29  46465  stoweidlem31  46467  stoweidlem34  46470  stoweidlem35  46471  stoweidlem36  46472  stoweidlem39  46475  stoweidlem42  46478  stoweidlem43  46479  stoweidlem44  46480  stoweidlem46  46482  stoweidlem48  46484  stoweidlem49  46485  stoweidlem50  46486  stoweidlem51  46487  stoweidlem52  46488  stoweidlem53  46489  stoweidlem54  46490  stoweidlem56  46492  stoweidlem57  46493  stoweidlem59  46495  stoweidlem60  46496  stoweidlem61  46497  stoweidlem62  46498  stoweid  46499  wallispilem3  46503  stirlinglem13  46522  stirling  46525  fourierdlem16  46559  fourierdlem21  46564  fourierdlem22  46565  fourierdlem31  46574  fourierdlem39  46582  fourierdlem48  46590  fourierdlem51  46593  fourierdlem53  46595  fourierdlem68  46610  fourierdlem69  46611  fourierdlem71  46613  fourierdlem73  46615  fourierdlem77  46619  fourierdlem80  46622  fourierdlem81  46623  fourierdlem82  46624  fourierdlem83  46625  fourierdlem86  46628  fourierdlem87  46629  fourierdlem89  46631  fourierdlem91  46633  fourierdlem93  46635  fourierdlem94  46636  fourierdlem103  46645  fourierdlem104  46646  fourierdlem112  46654  fourierdlem113  46655  elaa2  46670  etransclem18  46688  etransclem22  46692  etransclem23  46693  etransclem32  46702  etransclem35  46705  etransclem44  46714  etransclem46  46716  etransclem48  46718  rrndistlt  46726  ioorrnopnlem  46740  saliuncl  46759  saliincl  46763  intsaluni  46765  salexct  46770  subsaliuncl  46794  sge00  46812  sge0revalmpt  46814  sge0sn  46815  sge0f1o  46818  sge0gerp  46831  sge0pnffigt  46832  sge0lefi  46834  sge0ltfirp  46836  sge0resrnlem  46839  sge0resplit  46842  sge0lempt  46846  sge0iunmptlemfi  46849  sge0p1  46850  sge0iunmptlemre  46851  sge0fodjrnlem  46852  sge0iunmpt  46854  sge0rpcpnf  46857  sge0ltfirpmpt2  46862  sge0isum  46863  sge0xp  46865  sge0ad2en  46867  sge0isummpt2  46868  sge0xaddlem1  46869  sge0xaddlem2  46870  sge0xadd  46871  sge0pnffsumgt  46878  sge0gtfsumgt  46879  sge0uzfsumgt  46880  sge0seq  46882  sge0reuz  46883  sge0reuzb  46884  iundjiun  46896  meadjiunlem  46901  meadjiun  46902  ismeannd  46903  voliunsge0lem  46908  meaiuninclem  46916  meaiunincf  46919  meaiuninc3v  46920  meaiuninc3  46921  meaiininclem  46922  meaiininc  46923  meaiininc2  46924  caragenfiiuncl  46951  omeiunltfirp  46955  carageniuncllem1  46957  carageniuncllem2  46958  caratheodorylem2  46963  0ome  46965  isomenndlem  46966  hoicvrrex  46992  ovnsupge0  46993  ovnlecvr  46994  ovnlerp  46998  ovncvrrp  47000  ovn0lem  47001  ovnsubaddlem1  47006  ovnsubaddlem2  47007  hoidmvcl  47018  hsphoidmvle2  47021  hsphoidmvle  47022  hoidmvval0  47023  sge0hsphoire  47025  hoidmvval0b  47026  hoidmv1lelem1  47027  hoidmv1lelem2  47028  hoidmv1lelem3  47029  hoidmvlelem1  47031  hoidmvlelem2  47032  hoidmvlelem3  47033  hoidmvlelem4  47034  hoidmvlelem5  47035  hoidmvle  47036  ovnhoilem1  47037  ovnhoilem2  47038  ovnhoi  47039  ovnlecvr2  47046  hspdifhsp  47052  hoidifhspdmvle  47056  hoiqssbllem3  47060  hspmbllem1  47062  hspmbllem2  47063  opnvonmbllem1  47068  opnvonmbllem2  47069  ovnsubadd2lem  47081  ovolval5lem1  47088  ovnovollem1  47092  ovnovollem2  47093  hoimbl2  47101  vonhoire  47108  iinhoiicclem  47109  iinhoiicc  47110  iunhoiioolem  47111  iunhoiioo  47112  vonioolem1  47116  vonioolem2  47117  vonioo  47118  vonicclem1  47119  vonicclem2  47120  vonicc  47121  vonn0ioo2  47126  vonn0icc2  47128  vonct  47129  pimltmnf2f  47133  pimgtpnf2f  47141  salpreimagelt  47143  salpreimalegt  47145  pimltpnf2f  47148  pimgtmnf2  47150  pimdecfgtioc  47151  pimincfltioc  47152  pimdecfgtioo  47153  pimincfltioo  47154  preimageiingt  47156  preimaleiinlt  47157  salpreimagtge  47161  salpreimaltle  47162  salpreimalelt  47165  salpreimagtlt  47166  issmff  47170  sssmf  47174  mbfresmf  47175  cnfsmf  47176  incsmflem  47177  incsmf  47178  smfsssmf  47179  issmflelem  47180  issmfle  47181  smfconst  47185  issmfgtlem  47191  issmfgt  47192  smfpimltxrmptf  47194  smfmbfcex  47196  smfaddlem1  47199  smfaddlem2  47200  smfadd  47201  decsmflem  47202  decsmf  47203  smfpreimagtf  47204  issmfgelem  47205  issmfge  47206  smflimlem2  47208  smflimlem4  47210  smflim  47213  smfpimgtxr  47216  smfpimgtxrmptf  47220  smfpimioo  47223  smfresal  47224  smfrec  47225  smfres  47226  smfmullem2  47228  smfmullem4  47230  smfmul  47231  smfpimbor1lem2  47235  smf2id  47237  smfco  47238  smflim2  47242  smfpimcc  47244  smflimmpt  47246  smfsuplem1  47247  smfsuplem3  47249  smfsup  47250  smfsupmpt  47251  smfsupxr  47252  smfinflem  47253  smfinf  47254  smfinfmpt  47255  smflimsuplem3  47258  smflimsuplem4  47259  smflimsuplem5  47260  smflimsuplem7  47262  smflimsuplem8  47263  smflimsup  47264  smflimsupmpt  47265  smfliminflem  47266  smfliminf  47267  smfliminfmpt  47268  smfpimne2  47276  fsupdm  47278  smfsupdmmbllem  47280  smfsupdmmbl  47281  finfdm  47282  smfinfdmmbllem  47284  smfinfdmmbl  47285  or2expropbilem1  47482  or2expropbilem2  47483  or2expropbi  47484  cfsetsnfsetf  47508  cfsetsnfsetfo  47510  rexsb  47549  reuf1odnf  47557  2reu8i  47563  ffnafv  47621  tz6.12c-afv2  47692  f1oresf1o2  47741  iccelpart  47895  iccpartdisj  47899  dfich2  47920  ichbi12i  47922  ichnfimlem  47925  ich2exprop  47933  ichnreuop  47934  ichreuopeq  47935  sprsymrelfo  47959  reupr  47984  reuopreuprim  47988  mogoldbb  48263  2zrngagrp  48727  2zrngmmgm  48730  cbvmpox2  48814  ovmpordx  48818  1arymaptfo  49121  2arymaptfo  49132  mo0sn  49293  iinfssclem3  49533  iinfssc  49534  iinfsubc  49535  infsubc2  49538  iinfconstbas  49543  isthincd2lem1  49902  nfintd  50150  nfiund  50151  nfiundg  50152  iunord  50153  spcdvw  50156  nfsetrecs  50163  setrec1lem2  50165  setrec1  50168  setrec2fun  50169  pgindnf  50193  pgind  50194  aacllem  50278