Theorem nfv 1918

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

Syntax hints:  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfvd  1919  nfsbvOLD  2326  cbvaldw  2336  cbval2v  2341  cbval2vOLD  2342  dvelimhw  2344  pm11.53  2345  19.12vv  2346  eeanv  2348  eeeanv  2349  sbnf2  2357  exsb  2358  2exsb  2359  sbbibvv  2361  sbievg  2362  cleljustALT2  2364  spimv  2391  spimev  2393  chvarv  2397  cbvalv  2401  cbvexv  2402  cbvald  2408  cbvaldva  2410  cbvexdva  2411  cbval2  2412  axc16i  2437  dvelimnf  2454  sbel2x  2475  sbiedv  2509  2sbiev  2510  sbid2v  2514  sbhb  2526  2sb8e  2536  nfmod2  2559  nfmodv  2560  mof  2564  mo4f  2568  euf  2577  sb8eulem  2599  cbvmow  2604  sbmo  2617  moexexvw  2631  moexexv  2642  2mo  2651  2mos  2652  2eu6  2659  axextmo  2714  nulmo  2715  abbi  2811  cleqh  2863  clelsb2OLD  2869  clelabOLD  2885  nfcv  2908  nfeqd  2918  nfeld  2919  nfabdw  2931  nfabdwOLD  2932  nfabd  2933  dvelimdc  2935  nfcvf  2937  cleqf  2939  sbabelOLD  2943  2ralbida  3163  rexbidvaALT  3253  rexbidvALT  3255  r19.12  3258  r19.12OLD  3259  r19.29af  3263  reean  3294  rmobidvaOLD  3329  cbvralfwOLD  3370  cbvralf  3372  cbvrmow  3376  cbvreuwOLD  3378  cbvreu  3382  cbvreuvwOLD  3388  cbvralv  3389  cbvrexv  3390  cbvreuv  3391  cbvrmov  3392  cbvralsvw  3403  cbvrexsvw  3404  cbvralsv  3405  cbvrexsv  3406  cbvrabw  3425  cbvrab  3426  issetf  3447  ceqsalvOLD  3469  ceqsralvOLD  3471  ceqsexvOLD  3481  ceqsex2  3483  vtoclgft  3493  vtocldOLD  3496  vtoclALT  3500  vtoclgOLD  3507  vtocl2gaf  3516  vtocl3gaf  3517  vtocl3gaOLD  3519  spc2ed  3541  rspct  3548  rspc  3550  rspce  3551  eqvincf  3581  clel2gOLD  3590  elabgtOLD  3605  elabgOLD  3609  elabOLD  3611  elrab3t  3624  ralab2  3635  rexab2  3637  mob2  3651  mob  3653  reu2  3661  rmo4f  3671  reu2eqd  3672  cdeqab1  3708  nfcdeq  3713  sbcco  3743  cbvsbcv  3754  sbciegOLD  3758  sbciedOLD  3763  elrabsf  3765  sbcgOLD  3797  sbc2iegf  3799  sbc2ieOLD  3801  reu8nf  3811  rmo2  3821  rmo3  3823  rmoanimALT  3829  csbeq2dv  3840  nfcsb1d  3856  nfcsbd  3859  csbiebt  3863  csbiedOLD  3872  csbie2t  3874  cbvrabcsfw  3877  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  cbvralv2  3882  cbvrexv2  3883  rspc2vd  3884  dfss2f  3912  uniiunlem  4020  rspn0OLD  4288  ab0OLD  4310  ab0orv  4313  ab0orvALT  4314  sbcnestgw  4355  sbcnestg  4360  sbnfc2  4371  r19.3rzv  4430  r19.28zv  4432  r19.27zv  4437  2reu4lem  4457  nfifd  4489  reusngf  4609  reusng  4612  ralsngOLD  4614  rexsngOLD  4615  rexreusng  4616  ralprgOLD  4632  rexprgOLD  4634  reuprg0  4639  rabsnifsb  4659  euabsn  4663  nfunid  4846  eluniab  4855  nfint  4890  elintab  4891  iuneqconst  4936  iineq2dv  4950  disjiun  5062  disjxun  5073  nfopabd  5143  cbvopab  5147  cbvopabvOLD  5149  cbvopab1  5150  cbvopab1g  5151  cbvopab2  5152  cbvopab1s  5153  cbvopab1vOLD  5155  mpteq12da  5160  mpteq12dfOLD  5162  mpteq12f  5163  mpteq2dvaOLD  5176  cbvmptf  5184  cbvmptfg  5185  axrep1  5211  axrep2  5213  axrep3  5214  axrep4  5215  axrep5  5216  zfrepclf  5219  reusv2lem3  5324  reusv2lem4  5325  reusv2  5327  reusv3  5329  alxfr  5331  ralxfrALT  5339  axprlem3  5349  axprlem4  5350  axprlem5  5351  copsex2t  5407  copsex2gOLD  5409  iunopeqop  5436  rexopabb  5442  opelopabaf  5458  nfso  5510  pofun  5522  isso2i  5539  nffr  5564  opeliunxp  5655  opeliunxp2  5750  ralxpf  5758  dfdmf  5808  dfrnf  5862  elrnmpt1  5870  dfrel4  6099  reuop  6200  frpoinsg  6250  frpoins2g  6252  wfisgOLD  6261  wfis2g  6266  nfiotadw  6398  nfiotad  6400  cbviotaw  6402  cbviotavwOLD  6404  cbviota  6405  cbviotav  6406  sb8iota  6407  iota2d  6425  iota2  6426  dffun6f  6454  imadif  6525  funimaexgOLD  6528  isarep1  6530  isarep1OLD  6531  isarep2  6532  fv3  6801  tz6.12f  6807  tz6.12c  6808  fvelimad  6845  feqmptdf  6848  opabiotafun  6858  funfv2f  6866  fvmptd  6891  fvmptd2f  6900  fvmptdv  6901  fvmptt  6904  fvopab5  6916  eqfnfv2f  6922  ralrnmptw  6979  ralrnmpt  6981  f1ompt  6994  ffnfv  7001  ffnfvf  7002  f1ossf1o  7009  fmptco  7010  elabrex  7125  dff13f  7138  fsnex  7164  fliftfun  7192  cbvriotaw  7250  cbvriotavwOLD  7252  cbvriota  7255  cbvriotav  7256  riota2  7267  riotaeqimp  7268  riota5f  7270  oprabv  7344  nfoprab  7348  mpoeq123  7356  cbvoprab1  7371  cbvoprab2  7372  cbvoprab12  7373  cbvoprab12v  7374  cbvoprab3  7375  cbvoprab3v  7376  cbvmpox  7377  ralrnmpo  7421  ovmpodx  7433  ovmpodf  7438  ovmpodv  7439  ov3  7444  ovmpt3rab1  7536  ofrfval2  7563  onminex  7661  tfis  7710  tfis2  7712  tfisi  7714  tfinds  7715  tfindes  7718  peano5OLD  7750  findes  7758  fiun  7794  f1iun  7795  abrexex2g  7816  opabex3d  7817  opabex3rd  7818  opabex3  7819  dfoprab4f  7905  fmpox  7916  offval22  7937  ovmptss  7942  opeliunxp2f  8035  tposoprab  8087  fvmpocurryd  8096  nffrecs  8108  nfwrecsOLD  8142  tfr3  8239  nfrdg  8254  tz7.48-1  8283  tz7.49  8285  eqerlem  8541  erovlem  8611  mptelixpg  8732  boxcutc  8738  dom2lem  8789  xpf1o  8935  mapxpen  8939  findcard2  8956  pssnn  8960  nneneq  9001  nneneqOLD  9013  pssnnOLD  9049  findcard2OLD  9065  ac6sfi  9067  fiint  9100  indexfi  9136  wdom2d  9348  ixpiunwdom  9358  cantnflem1  9456  nfttrcld  9477  frinsg  9518  frins2  9521  r1val1  9553  rankuni2b  9620  scottexs  9654  scott0s  9655  dfac8clem  9797  acni2  9811  aceq1  9882  dfac5lem5  9892  kmlem15  9929  infpssrlem4  10071  fin23lem27  10093  hsmexlem2  10192  hsmexlem4  10194  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  ac6c4  10246  zorn2lem4  10264  zorn2lem5  10265  iunfo  10304  iundom2g  10305  uniimadomf  10310  konigthlem  10333  axrepndlem2  10358  axunnd  10361  axpowndlem2  10363  axpowndlem4  10365  axregndlem2  10368  axacndlem5  10376  zfcndrep  10379  zfcndinf  10383  pwfseqlem4a  10426  pwfseqlem4  10427  tskuni  10548  gruiin  10575  reclem2pr  10813  dedekind  11147  dedekindle  11148  fimaxre3  11930  nn0ind-raph  12429  uzind4s  12657  nnwof  12663  lbzbi  12685  fzrevral  13350  rabssnn0fi  13715  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  fsuppmapnn0fiubex  13721  seqof2  13790  reuccatpfxs1  14469  cotr2g  14696  rlim2  15214  ello1mpt  15239  climeu  15273  o1compt  15305  summolem2a  15436  zsum  15439  sumss  15445  sumss2  15447  fsumcvg2  15448  fsumclf  15459  fsumsplitf  15463  fsumsplit1  15466  fsum2dlem  15491  fsum00  15519  o1fsum  15534  nfcprod1  15629  nfcprod  15630  prodmolem2a  15653  zprod  15656  fprod  15660  fprodntriv  15661  prodss  15666  fprodn0  15698  fprod2dlem  15699  fprodsplitf  15707  fprodsplit1f  15709  fprodle  15715  fprodmodd  15716  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  coprmprod  16375  coprmproddvdslem  16376  prmind2  16399  iserodd  16545  pcmpt  16602  pcmptdvds  16604  prmolefac  16756  mreexexd  17366  catpropd  17427  invfuc  17701  natpropd  17703  fucpropd  17704  initoeu2  17740  acsmapd  18281  symgval  18985  gsumsnd  19562  gsumsnf  19563  gsumunsnfd  19567  gsummptf1o  19573  gsummpt1n0  19575  gsum2d2lem  19583  gsumcom2  19585  gsummptnn0fz  19596  dprd2d2  19656  gsummoncoe1  21484  gsumply1eq  21485  mdetralt2  21767  mdetunilem2  21771  madugsum  21801  gsummatr01lem4  21816  cpmatmcllem  21876  cayleyhamilton1  22050  neiptopnei  22292  neiptopreu  22293  neitr  22340  fiuncmp  22564  iunconnlem  22587  iunconn  22588  2ndcdisj  22616  dissnlocfin  22689  elptr2  22734  ptbasfi  22741  ptcld  22773  ptcldmpt  22774  ptclsg  22775  ptcnplem  22781  ptcnp  22782  cnmpt11  22823  cnmpt21  22831  cnmptcom  22838  imasnopn  22850  imasncld  22851  imasncls  22852  xkocnv  22974  elmptrab  22987  isfildlem  23017  alexsubALTlem3  23209  cnextfvval  23225  utopsnneiplem  23408  isucn2  23440  cfilucfil  23724  blval2  23727  restmetu  23735  ovoliunlem3  24677  ovoliun  24678  ovoliun2  24679  ovoliunnul  24680  finiunmbl  24717  volfiniun  24720  iundisj  24721  iunmbl  24726  voliun  24727  iunmbl2  24730  mbfeqalem1  24814  mbfsup  24837  mbfinf  24838  mbflim  24841  itg2splitlem  24922  itg2split  24923  isibl2  24940  cbvitg  24949  itgeqa  24987  itgss3  24988  itgfsum  25000  itgabs  25008  itggt0  25017  itgcn  25018  limcmpt  25056  limciun  25067  dvmptfsum  25148  dvlipcn  25167  dvfsumlem2  25200  dvfsumlem4  25202  dvfsumrlim  25204  dvfsum2  25207  itgsubst  25222  coeeq2  25412  dgrle  25413  ulmss  25565  leibpi  26101  rlimcnp  26124  rlimcnp2  26125  o1cxp  26133  lgamgulmlem2  26188  lgamgulmlem6  26192  fsumdvdscom  26343  lgseisenlem2  26533  2sqmo  26594  2sqreulem4  26611  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  istrkg2ld  26830  mptelee  27272  gropd  27410  grstructd  27411  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1o  28738  ex-natded9.26  28792  isch3  29612  atom1d  30724  chirred  30766  sbc2iedf  30824  rspc2daf  30825  19.9d2r  30830  opreu2reuALT  30834  mo5f  30846  reuxfrdf  30848  eqrrabd  30858  foresf1o  30859  elabreximdv  30865  rabss3d  30870  iinabrex  30917  cbvdisjf  30919  disjorf  30927  disjabrex  30930  iundisjf  30937  disjunsn  30942  brabgaf  30957  ac6sf2  30969  dfimafnf  30980  fimarab  30989  2ndresdju  30995  fmptcof2  31003  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  aciunf1  31009  ofpreima  31011  funcnv5mpt  31014  funcnv4mpt  31015  fnpreimac  31017  padct  31063  cnvoprabOLD  31064  f1od2  31065  fpwrelmap  31077  xrofsup  31099  iundisjfi  31126  nnindf  31142  nn0min  31143  fprodex01  31148  fsumiunle  31152  gsummpt2d  31318  gsumhashmul  31325  isarchiofld  31525  nsgmgc  31606  nsgqusf1olem1  31607  nsgqusf1olem3  31609  nsgqusf1o  31610  elrspunidl  31615  fedgmullem2  31720  reff  31798  locfinreflem  31799  cmpcref  31809  zarclsiin  31830  zarcls  31833  zarcmplem  31840  ordtconnlem1  31883  qqhval2  31941  prodindf  32000  esumeq12dva  32009  esumeq2dv  32015  esumrnmpt  32029  esumpad  32032  esumpad2  32033  esumadd  32034  gsumesum  32036  esumlub  32037  esumsnf  32041  esumpr  32043  esumrnmpt2  32045  esumfzf  32046  esumfsup  32047  esumpcvgval  32055  esumpmono  32056  esumcocn  32057  hasheuni  32062  esumcvg  32063  esumgect  32067  esum2dlem  32069  esum2d  32070  esumiun  32071  ldsysgenld  32137  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  fiunelros  32151  measvunilem  32189  measvunilem0  32190  measvuni  32191  measiun  32195  measinblem  32197  voliune  32206  volfiniune  32207  volmeas  32208  ddemeas  32213  oms0  32273  omssubadd  32276  carsgclctunlem1  32293  carsggect  32294  omsmeas  32299  eulerpartlemgvv  32352  dstrvprob  32447  ballotlemodife  32473  reprsuc  32604  reprdifc  32616  breprexplema  32619  breprexplemc  32621  circlemethhgt  32632  hgt750lemd  32637  bnj919  32756  bnj1146  32780  bnj1379  32819  bnj1385  32821  bnj1400  32824  bnj1534  32842  bnj1542  32846  bnj110  32847  bnj121  32859  bnj124  32860  bnj130  32863  bnj207  32870  bnj571  32895  bnj605  32896  bnj580  32902  bnj607  32905  bnj611  32907  bnj873  32913  bnj849  32914  bnj900  32918  bnj916  32922  bnj1000  32930  bnj964  32932  bnj981  32939  bnj985v  32942  bnj985  32943  bnj1014  32950  bnj1123  32975  bnj1128  32979  bnj1228  33000  bnj1204  33001  bnj1279  33007  bnj1307  33012  bnj1321  33016  bnj1388  33022  bnj1398  33023  bnj1408  33025  bnj1417  33030  bnj1444  33032  bnj1445  33033  bnj1446  33034  bnj1449  33037  bnj1467  33043  bnj1489  33045  bnj1312  33047  bnj1497  33049  bnj1518  33053  bnj1525  33058  bnj1529  33059  fineqvrep  33073  cvmcov  33234  untsucf  33660  ralxpes  33687  ralxp3  33695  ralxp3es  33697  setinds2  33765  dfon2lem1  33768  dfon2lem3  33770  frpoins3xpg  33796  frpoins3xp3g  33797  nosupbnd1  33926  nosupbnd2  33928  noinfbnd1  33941  noinfbnd2  33943  finminlem  34516  bj-nexdvt  34889  bj-cbvaldv  34990  bj-cbval2vv  34992  bj-cbvex2vv  34993  bj-cbvaldvav  34994  bj-cbvexdvav  34995  ax11-pm2  35028  bj-dvelimdv  35044  bj-nfeel2  35047  bj-ceqsalv  35088  bj-vtocl  35110  bj-inrab2  35125  currysetlem  35143  currysetlem1  35145  bj-opabco  35368  mptsnunlem  35518  exlimim  35522  exellim  35524  topdifinfindis  35526  topdifinffinlem  35527  icorempo  35531  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlssretop  35543  finxpreclem2  35570  finxpreclem6  35576  fvineqsneu  35591  fvineqsneq  35592  wl-euequf  35738  wl-sb8eut  35741  phpreu  35770  matunitlindflem2  35783  ptrest  35785  ptrecube  35786  poimirlem2  35788  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  heicant  35821  mbfposadd  35833  itgabsnc  35855  itggt0cn  35856  ftc1anclem5  35863  upixp  35896  indexa  35900  indexdom  35901  filbcmb  35907  sdclem2  35909  sdclem1  35910  fdc1  35913  totbndbnd  35956  sbcalf  36281  sbcexf  36282  scottexf  36335  scott0f  36336  eqrelf  36403  fsumshftd  36973  riotasv2d  36978  riotasv2s  36979  riotasv3d  36981  glbconxN  37399  pmapglbx  37790  pmapglb2xN  37793  cdleme26ee  38381  cdleme31sn  38401  cdleme31sn1  38402  cdlemefr29exN  38423  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32fva  38458  cdleme32d  38465  cdleme32f  38467  cdleme40m  38488  cdleme40n  38489  cdleme42b  38499  cdlemk36  38934  cdlemk38  38936  cdlemkid  38957  cdlemk19x  38964  cdlemk11t  38967  dihvalcqpre  39256  mapdheq  39749  hdmap1eq  39822  hdmapval2lem  39852  lcmineqlem9  40052  lcmineqlem12  40055  aks4d1p1p2  40085  sticksstones1  40109  sticksstones11  40119  sticksstones16  40125  sticksstones22  40131  metakunt33  40164  mzpexpmpt  40574  eq0rabdioph  40605  rexrabdioph  40623  rexfrabdioph  40624  elnn0rabdioph  40632  dvdsrabdioph  40639  fphpd  40645  monotuz  40770  monotoddzz  40772  oddcomabszz  40773  setindtr  40853  dford4  40858  wdom2d2  40864  aomclem6  40891  aomclem8  40893  flcidc  41006  areaquad  41054  rababg  41188  ss2iundv  41275  cbviuneq12dv  41277  gneispace  41751  mnringvald  41833  mnringmulrcld  41853  nfscott  41864  scottabf  41865  scottab  41866  mnuprdlem4  41900  ismnushort  41926  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  aaanv  42013  pm11.57  42014  pm11.58  42015  pm11.59  42016  pm11.71  42022  pm14.12  42046  ssralv2  42158  tratrb  42163  iunconnlem2  42562  evth2f  42565  elunif  42566  fvelrnbf  42568  evthf  42577  fnchoice  42579  sumpair  42585  rfcnnnub  42586  refsum2cn  42588  elabrexg  42596  uzwo4  42608  fiiuncl  42620  fiunicl  42622  elintdv  42636  ssd  42637  cbvmpo2  42654  cbvmpo1  42655  eliin2f  42661  eliuniin2  42676  cbvrabv2  42683  cbvrabv2w  42684  suprnmpt  42717  dffo3f  42724  disjf1  42727  disjrnmpt2  42733  disjf1o  42736  fompt  42737  disjinfi  42738  choicefi  42747  iunmapsn  42764  axccdom  42769  dmrelrnrel  42772  axccd  42775  funimassd  42777  fmptf  42790  rnmptlb  42795  rnmptbddlem  42796  rnmptbd2lem  42801  rnmptbdlem  42808  rnmptbd  42809  upbdrech  42851  ssfiunibd  42855  supxrgere  42879  iuneqfzuzlem  42880  supxrgelem  42883  supxrge  42884  suplesup  42885  infrpge  42897  xralrple2  42900  infxr  42913  infxrunb2  42914  infleinf  42918  xrralrecnnle  42929  xrralrecnnge  42937  supxrunb3  42946  supxrleubrnmpt  42953  infleinf2  42961  unb2ltle  42962  rexabslelem  42965  rexabsle  42966  allbutfiinf  42967  suprleubrnmpt  42969  infrnmptle  42970  infxrunb3rnmpt  42975  uzublem  42977  uzub  42978  supminfrnmpt  42992  infxrpnf  42993  supxrleubrnmptf  42998  infxrgelbrnmpt  43001  infrpgernmpt  43012  supminfxr2  43016  monoordxr  43030  monoord2xr  43032  iccshift  43063  iooshift  43067  iooiinicc  43087  iooiinioc  43101  fsummulc1f  43119  fsumnncl  43120  fsumf1of  43122  fsumiunss  43123  fsumreclf  43124  fsumlessf  43125  fsumsermpt  43127  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  fmul01lt1  43134  fprodsplit1  43141  fprodexp  43142  fprodabs2  43143  mccllem  43145  mccl  43146  fprodcnlem  43147  fprodcn  43148  climexp  43153  climsuse  43156  climrecf  43157  climinff  43159  climaddf  43163  mullimc  43164  ellimcabssub0  43165  islptre  43167  climf  43170  mullimcf  43171  rexlim2d  43173  idlimc  43174  limcperiod  43176  limcrecl  43177  sumnnodd  43178  islpcn  43187  limsupre  43189  limcleqr  43192  neglimc  43195  addlimc  43196  0ellimcdiv  43197  limclner  43199  climsubmpt  43208  climreclf  43212  climf2  43214  fnlimcnv  43215  climeldmeqmpt  43216  clim2f2  43218  climfveqmpt  43219  fnlimfvre  43222  allbutfifvre  43223  climleltrp  43224  fnlimf  43226  fnlimabslt  43227  climfveqmpt3  43230  climeldmeqf  43231  limsupref  43233  limsupbnd1f  43234  climbddf  43235  climeqf  43236  climeldmeqmpt3  43237  limsuplesup  43247  limsuppnfd  43250  limsupub  43252  limsupres  43253  climinf2lem  43254  climinf2  43255  limsuppnf  43259  limsupubuzlem  43260  limsupubuz  43261  climinf2mpt  43262  climinfmpt  43263  climinf3  43264  limsupmnflem  43268  limsupmnf  43269  limsupequz  43271  limsupre2  43273  limsupmnfuzlem  43274  limsupmnfuz  43275  limsupequzmptf  43279  limsupre3lem  43280  limsupre3  43281  limsupre3uzlem  43283  limsupre3uz  43284  limsupreuz  43285  limsupvaluz2  43286  limsupreuzmpt  43287  supcnvlimsup  43288  climuzlem  43291  climuz  43292  climisp  43294  lmbr3  43295  climrescn  43296  climxrrelem  43297  climxrre  43298  liminfcl  43311  liminfval2  43316  limsup10exlem  43320  liminflelimsuplem  43323  limsupgtlem  43325  limsupgt  43326  climliminflimsupd  43349  liminfreuzlem  43350  liminfreuz  43351  liminfltlem  43352  liminflt  43353  limsupub2  43360  xlimpnfxnegmnf  43362  liminflbuz2  43363  liminfpnfuz  43364  liminflimsupxrre  43365  xlimmnfvlem1  43380  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem1  43384  xlimpnfvlem2  43385  xlimpnfv  43386  xlimmnf  43389  xlimpnf  43390  xlimmnfmpt  43391  xlimpnfmpt  43392  climxlim2lem  43393  dfxlim2  43396  cncfshift  43422  icccncfext  43435  cncficcgt0  43436  cncfiooicc  43442  cncfioobd  43445  fprodcncf  43448  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  dvmptmulf  43485  dvnmptdivc  43486  dvnmul  43491  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  iblsplitf  43518  iblspltprt  43521  itgioocnicc  43525  iblcncfioo  43526  itgspltprt  43527  itgperiod  43529  stoweidlem3  43551  stoweidlem14  43562  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem26  43574  stoweidlem27  43575  stoweidlem28  43576  stoweidlem29  43577  stoweidlem31  43579  stoweidlem34  43582  stoweidlem35  43583  stoweidlem36  43584  stoweidlem39  43587  stoweidlem42  43590  stoweidlem43  43591  stoweidlem44  43592  stoweidlem46  43594  stoweidlem48  43596  stoweidlem49  43597  stoweidlem50  43598  stoweidlem51  43599  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  stoweidlem56  43604  stoweidlem57  43605  stoweidlem59  43607  stoweidlem60  43608  stoweidlem61  43609  stoweidlem62  43610  stoweid  43611  wallispilem3  43615  stirlinglem13  43634  stirling  43637  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem31  43686  fourierdlem39  43694  fourierdlem48  43702  fourierdlem51  43705  fourierdlem53  43707  fourierdlem68  43722  fourierdlem69  43723  fourierdlem71  43725  fourierdlem73  43727  fourierdlem77  43731  fourierdlem80  43734  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem86  43740  fourierdlem87  43741  fourierdlem89  43743  fourierdlem91  43745  fourierdlem93  43747  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem113  43767  elaa2  43782  etransclem18  43800  etransclem22  43804  etransclem23  43805  etransclem32  43814  etransclem35  43817  etransclem44  43826  etransclem46  43828  etransclem48  43830  rrndistlt  43838  ioorrnopnlem  43852  intsaluni  43875  salexct  43880  subsaliuncl  43904  sge00  43921  sge0revalmpt  43923  sge0sn  43924  sge0f1o  43927  sge0gerp  43940  sge0pnffigt  43941  sge0lefi  43943  sge0ltfirp  43945  sge0resrnlem  43948  sge0resplit  43951  sge0lempt  43955  sge0iunmptlemfi  43958  sge0p1  43959  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0iunmpt  43963  sge0rpcpnf  43966  sge0ltfirpmpt2  43971  sge0isum  43972  sge0xp  43974  sge0ad2en  43976  sge0isummpt2  43977  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0xadd  43980  sge0pnffsumgt  43987  sge0gtfsumgt  43988  sge0uzfsumgt  43989  sge0seq  43991  sge0reuz  43992  sge0reuzb  43993  iundjiun  44005  meadjiunlem  44010  meadjiun  44011  ismeannd  44012  voliunsge0lem  44017  meaiuninclem  44025  meaiunincf  44028  meaiuninc3v  44029  meaiuninc3  44030  meaiininclem  44031  meaiininc  44032  meaiininc2  44033  caragenfiiuncl  44060  omeiunltfirp  44064  carageniuncllem1  44066  carageniuncllem2  44067  caratheodorylem2  44072  0ome  44074  isomenndlem  44075  hoicvrrex  44101  ovnsupge0  44102  ovnlecvr  44103  ovnlerp  44107  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  ovnsubaddlem2  44116  hoidmvcl  44127  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmvval0  44132  sge0hsphoire  44134  hoidmvval0b  44135  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem1  44146  ovnhoilem2  44147  ovnhoi  44148  ovnlecvr2  44155  hspdifhsp  44161  hoidifhspdmvle  44165  hoiqssbllem3  44169  hspmbllem1  44171  hspmbllem2  44172  opnvonmbllem1  44177  opnvonmbllem2  44178  ovnsubadd2lem  44190  ovolval5lem1  44197  ovnovollem1  44201  ovnovollem2  44202  hoimbl2  44210  vonhoire  44217  iinhoiicclem  44218  iinhoiicc  44219  iunhoiioolem  44220  iunhoiioo  44221  vonioolem1  44225  vonioolem2  44226  vonioo  44227  vonicclem1  44228  vonicclem2  44229  vonicc  44230  vonn0ioo2  44235  vonn0icc2  44237  vonct  44238  pimltmnf2f  44242  pimgtpnf2f  44250  salpreimagelt  44252  salpreimalegt  44254  pimltpnf2f  44257  pimgtmnf2  44259  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  salpreimagtge  44270  salpreimaltle  44271  salpreimalelt  44274  salpreimagtlt  44275  issmff  44279  sssmf  44283  mbfresmf  44284  cnfsmf  44285  incsmflem  44286  incsmf  44287  smfsssmf  44288  issmflelem  44289  issmfle  44290  smfconst  44294  issmfgtlem  44300  issmfgt  44301  smfpimltxrmptf  44303  smfmbfcex  44305  smfaddlem1  44308  smfaddlem2  44309  smfadd  44310  decsmflem  44311  decsmf  44312  smfpreimagtf  44313  issmfgelem  44314  issmfge  44315  smflimlem2  44317  smflimlem4  44319  smflim  44322  smfpimgtxr  44325  smfpimgtxrmptf  44329  smfpimioo  44332  smfresal  44333  smfrec  44334  smfres  44335  smfmullem2  44337  smfmullem4  44339  smfmul  44340  smfpimbor1lem2  44344  smf2id  44346  smfco  44347  smflim2  44350  smfpimcc  44352  smflimmpt  44354  smfsuplem1  44355  smfsuplem3  44357  smfsup  44358  smfsupmpt  44359  smfsupxr  44360  smfinflem  44361  smfinf  44362  smfinfmpt  44363  smflimsuplem3  44366  smflimsuplem4  44367  smflimsuplem5  44368  smflimsuplem7  44370  smflimsuplem8  44371  smflimsup  44372  smflimsupmpt  44373  smfliminflem  44374  smfliminf  44375  smfliminfmpt  44376  or2expropbilem1  44537  or2expropbilem2  44538  or2expropbi  44539  cfsetsnfsetf  44563  cfsetsnfsetfo  44565  rexsb  44602  reuf1odnf  44610  2reu8i  44616  ffnafv  44674  tz6.12c-afv2  44745  f1oresf1o2  44794  iccelpart  44896  iccpartdisj  44900  dfich2  44921  ichbi12i  44923  ichnfimlem  44926  ich2exprop  44934  ichnreuop  44935  ichreuopeq  44936  sprsymrelfo  44960  reupr  44985  reuopreuprim  44989  mogoldbb  45248  2zrngagrp  45512  2zrngmmgm  45515  opeliun2xp  45679  cbvmpox2  45682  ovmpordx  45686  1arymaptfo  46000  2arymaptfo  46011  mo0sn  46172  isthincd2lem1  46319  nfintd  46390  nfiund  46391  nfiundg  46392  iunord  46393  spcdvw  46396  nfsetrecs  46403  setrec1lem2  46405  setrec1  46408  setrec2fun  46409  aacllem  46516