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 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 1912

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

This theorem is referenced by:  nfvd  1917  nfsbvOLD  2323  cbvaldw  2333  cbval2v  2338  dvelimhw  2340  pm11.53  2341  19.12vv  2342  eeanv  2344  eeeanv  2345  sbnf2  2353  exsb  2354  2exsb  2355  sbbibvv  2357  cbvsbvf  2359  cleljustALT2  2361  spimv  2388  spimev  2390  chvarv  2394  cbvalv  2398  cbvexv  2399  cbvald  2405  cbvaldva  2407  cbvexdva  2408  cbval2  2409  axc16i  2434  dvelimnf  2451  sbel2x  2472  sbiedv  2502  2sbiev  2503  sbid2v  2507  sbhb  2519  2sb8e  2528  nfmod2  2551  nfmodv  2552  mof  2556  mo4f  2560  euf  2569  sb8eulem  2591  cbvmow  2596  sbmo  2609  moexexvw  2623  moexexv  2634  2mo  2643  2mos  2644  2eu6  2651  axextmo  2706  nulmo  2707  abbib  2803  clelsb2OLD  2861  cleqh  2862  clelabOLD  2879  nfcv  2902  nfeqd  2912  nfeld  2913  nfabdw  2925  nfabdwOLD  2926  nfabd  2927  dvelimdc  2929  nfcvf  2931  cleqf  2933  sbabelOLD  2938  r19.29af  3264  rexbidvALT  3271  rexbidvaALT  3272  2ralbida  3279  r19.12  3310  r19.12OLD  3311  reean  3312  cbvralsvw  3313  cbvrexsvw  3314  cbvralsvwOLD  3315  cbvrexsvwOLD  3316  cbvralfwOLD  3319  cbvralf  3355  cbvralv  3359  cbvrexv  3360  cbvralsv  3361  cbvrexsv  3362  rmobidvaOLD  3403  cbvrmow  3404  cbvreuwOLD  3411  cbvreuvwOLD  3412  cbvreu  3423  cbvrmov  3425  cbvreuv  3426  cbvrabw  3466  cbvrab  3472  issetft  3487  ceqsalvOLD  3512  ceqsralvOLD  3514  ceqsexvOLDOLD  3527  ceqsex2  3529  vtocldOLD  3548  vtoclALT  3553  vtoclgOLDOLD  3560  vtocl2gaf  3568  vtocl3gaf  3569  vtocl3gaOLD  3571  spc2ed  3591  rspct  3598  rspc  3600  rspce  3601  eqvincf  3638  clel2gOLD  3648  elabgtOLD  3663  elabgOLD  3667  elabOLD  3669  elrab3t  3682  ralab2  3693  rexab2  3695  mob2  3711  mob  3713  reu2  3721  rmo4f  3731  reu2eqd  3732  cdeqab1  3768  nfcdeq  3773  sbcco  3803  cbvsbcv  3814  sbciegOLD  3818  sbciedOLD  3823  elrabsf  3825  sbcgOLD  3857  sbc2iegf  3859  sbc2ieOLD  3861  reu8nf  3871  rmo2  3881  rmo3  3883  rmoanimALT  3889  csbeq2dv  3900  nfcsb1d  3916  nfcsbd  3919  csbiebt  3923  csbiedOLD  3932  csbie2t  3934  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  cbvralv2  3942  cbvrexv2  3943  rspc2vd  3944  dfss2f  3972  rabss3d  4079  uniiunlem  4084  rspn0OLD  4353  ab0OLD  4375  ab0orv  4378  ab0orvALT  4379  sbcnestgw  4420  sbcnestg  4425  sbnfc2  4436  r19.3rzv  4498  r19.28zv  4500  r19.27zv  4505  2reu4lem  4525  nfifd  4557  reusngf  4676  reusng  4679  ralsngOLD  4681  rexsngOLD  4682  rexreusng  4683  ralprgOLD  4699  rexprgOLD  4701  reuprg0  4706  rabsnifsb  4726  euabsn  4730  nfunid  4914  eluniab  4923  nfint  4960  elintabOLD  4963  iuneqconst  5008  iineq2dv  5022  disjiun  5135  disjxun  5146  nfopabd  5216  cbvopab  5220  cbvopabvOLD  5222  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  cbvopab1vOLD  5228  mpteq12da  5233  mpteq12dfOLD  5235  mpteq12f  5236  mpteq2dvaOLD  5249  cbvmptf  5257  cbvmptfg  5258  axrep1  5286  axrep2  5288  axrep3  5289  axrep4  5290  axrep5  5291  zfrepclf  5294  reusv2lem3  5398  reusv2lem4  5399  reusv2  5401  reusv3  5403  alxfr  5405  ralxfrALT  5413  axprlem3  5423  axprlem4  5424  axprlem5  5425  copsex2t  5492  copsex2gOLD  5494  iunopeqop  5521  rexopabb  5528  opelopabaf  5544  nfso  5594  pofun  5606  isso2i  5623  nffr  5650  opeliunxp  5743  opeliunxp2  5838  ralxpf  5846  dfdmf  5896  dfrnf  5949  elrnmpt1  5957  dfrel4  6190  reuop  6292  frpoinsg  6344  frpoins2g  6346  wfisgOLD  6355  wfis2g  6360  nfiotadw  6498  nfiotad  6500  cbviotaw  6502  cbviotavwOLD  6504  cbviota  6505  cbviotav  6506  sb8iota  6507  iota2d  6531  iota2  6532  dffun6f  6561  imadif  6632  funimaexgOLD  6635  isarep1  6637  isarep1OLD  6638  isarep2  6639  fv3  6909  tz6.12f  6917  tz6.12cOLD  6918  funimassd  6958  fvelimad  6959  feqmptdf  6962  opabiotafun  6972  funfv2f  6980  fvmptd  7005  fvmptd2f  7014  fvmptdv  7015  fvmptt  7018  fvopab5  7030  eqfnfv2f  7036  ralrnmptw  7095  ralrnmpt  7097  dffo3f  7107  f1ompt  7112  fompt  7119  ffnfv  7120  ffnfvf  7121  f1ossf1o  7128  fmptco  7129  elabrex  7244  elabrexg  7245  dff13f  7258  fsnex  7284  fliftfun  7312  cbvriotaw  7377  cbvriotavwOLD  7379  cbvriota  7382  cbvriotav  7383  riota2  7394  riotaeqimp  7395  riota5f  7397  oprabv  7472  nfoprab  7476  mpoeq123  7484  cbvoprab1  7499  cbvoprab2  7500  cbvoprab12  7501  cbvoprab12v  7502  cbvoprab3  7503  cbvoprab3v  7504  cbvmpox  7505  ralrnmpo  7550  ovmpodx  7562  ovmpodf  7567  ovmpodv  7568  ov3  7574  ovmpt3rab1  7668  ofrfval2  7695  onminex  7794  tfis  7848  tfis2  7850  tfisi  7852  tfinds  7853  tfindes  7856  peano5OLD  7889  findes  7897  fiun  7933  f1iun  7934  abrexex2g  7955  opabex3d  7956  opabex3rd  7957  opabex3  7958  dfoprab4f  8046  fmpox  8057  offval22  8078  ovmptss  8083  ralxpes  8126  ralxp3  8128  ralxp3es  8129  frpoins3xpg  8130  frpoins3xp3g  8131  opeliunxp2f  8199  tposoprab  8251  fvmpocurryd  8260  nffrecs  8272  nfwrecsOLD  8306  tfr3  8403  nfrdg  8418  tz7.48-1  8447  tz7.49  8449  eqerlem  8741  erovlem  8811  mptelixpg  8933  boxcutc  8939  dom2lem  8992  xpf1o  9143  mapxpen  9147  findcard2  9168  pssnn  9172  nneneq  9213  nneneqOLD  9225  pssnnOLD  9269  findcard2OLD  9288  ac6sfi  9291  fiint  9328  indexfi  9364  wdom2d  9579  ixpiunwdom  9589  cantnflem1  9688  nfttrcld  9709  frinsg  9750  frins2  9753  r1val1  9785  rankuni2b  9852  scottexs  9886  scott0s  9887  dfac8clem  10031  acni2  10045  aceq1  10116  dfac5lem5  10126  kmlem15  10163  infpssrlem4  10305  fin23lem27  10327  hsmexlem2  10426  hsmexlem4  10428  axcc3  10437  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  ac6c4  10480  zorn2lem4  10498  zorn2lem5  10499  iunfo  10538  iundom2g  10539  uniimadomf  10544  konigthlem  10567  axrepndlem2  10592  axunnd  10595  axpowndlem2  10597  axpowndlem4  10599  axregndlem2  10602  axacndlem5  10610  zfcndrep  10613  zfcndinf  10617  pwfseqlem4a  10660  pwfseqlem4  10661  tskuni  10782  gruiin  10809  reclem2pr  11047  dedekind  11382  dedekindle  11383  fimaxre3  12165  nn0ind-raph  12667  uzind4s  12897  nnwof  12903  lbzbi  12925  fzrevral  13591  rabssnn0fi  13956  fsuppmapnn0fiublem  13960  fsuppmapnn0fiub  13961  fsuppmapnn0fiubex  13962  seqof2  14031  reuccatpfxs1  14702  cotr2g  14928  rlim2  15445  ello1mpt  15470  climeu  15504  o1compt  15536  summolem2a  15666  zsum  15669  sumss  15675  sumss2  15677  fsumcvg2  15678  fsumclf  15689  fsumsplitf  15693  fsumsplit1  15696  fsum2dlem  15721  fsum00  15749  o1fsum  15764  nfcprod1  15859  nfcprod  15860  prodmolem2a  15883  zprod  15886  fprod  15890  fprodntriv  15891  prodss  15896  fprodn0  15928  fprod2dlem  15929  fprodsplitf  15937  fprodsplit1f  15939  fprodle  15945  fprodmodd  15946  lcmfunsnlem1  16579  lcmfunsnlem2lem1  16580  lcmfunsnlem2  16582  coprmprod  16603  coprmproddvdslem  16604  prmind2  16627  iserodd  16773  pcmpt  16830  pcmptdvds  16832  prmolefac  16984  mreexexd  17597  catpropd  17658  invfuc  17932  natpropd  17934  fucpropd  17935  initoeu2  17971  acsmapd  18512  symgval  19278  gsumsnd  19862  gsumsnf  19863  gsumunsnfd  19867  gsummptf1o  19873  gsummpt1n0  19875  gsum2d2lem  19883  gsumcom2  19885  gsummptnn0fz  19896  dprd2d2  19956  rngqiprngimf1  21060  gsummoncoe1  22049  gsumply1eq  22050  mdetralt2  22332  mdetunilem2  22336  madugsum  22366  gsummatr01lem4  22381  cpmatmcllem  22441  cayleyhamilton1  22615  neiptopnei  22857  neiptopreu  22858  neitr  22905  fiuncmp  23129  iunconnlem  23152  iunconn  23153  2ndcdisj  23181  dissnlocfin  23254  elptr2  23299  ptbasfi  23306  ptcld  23338  ptcldmpt  23339  ptclsg  23340  ptcnplem  23346  ptcnp  23347  cnmpt11  23388  cnmpt21  23396  cnmptcom  23403  imasnopn  23415  imasncld  23416  imasncls  23417  xkocnv  23539  elmptrab  23552  isfildlem  23582  alexsubALTlem3  23774  cnextfvval  23790  utopsnneiplem  23973  isucn2  24005  cfilucfil  24289  blval2  24292  restmetu  24300  ovoliunlem3  25254  ovoliun  25255  ovoliun2  25256  ovoliunnul  25257  finiunmbl  25294  volfiniun  25297  iundisj  25298  iunmbl  25303  voliun  25304  iunmbl2  25307  mbfeqalem1  25391  mbfsup  25414  mbfinf  25415  mbflim  25418  itg2splitlem  25499  itg2split  25500  isibl2  25517  cbvitg  25526  itgeqa  25564  itgss3  25565  itgfsum  25577  itgabs  25585  itggt0  25594  itgcn  25595  limcmpt  25633  limciun  25644  dvmptfsum  25728  dvlipcn  25747  dvfsumlem2  25780  dvfsumlem4  25782  dvfsumrlim  25784  dvfsum2  25787  itgsubst  25802  coeeq2  25992  dgrle  25993  ulmss  26146  leibpi  26684  rlimcnp  26707  rlimcnp2  26708  o1cxp  26716  lgamgulmlem2  26771  lgamgulmlem6  26775  fsumdvdscom  26926  lgseisenlem2  27116  2sqmo  27177  2sqreulem4  27194  dchrisumlema  27228  dchrisumlem2  27230  dchrisumlem3  27231  nosupbnd1  27454  nosupbnd2  27456  noinfbnd1  27469  noinfbnd2  27471  istrkg2ld  27979  mptelee  28421  gropd  28559  grstructd  28560  clwwlknonclwlknonf1o  29883  dlwwlknondlwlknonf1o  29886  ex-natded9.26  29940  isch3  30762  atom1d  31874  chirred  31916  sbc2iedf  31975  rspc2daf  31976  19.9d2r  31980  opreu2reuALT  31985  mo5f  31997  reuxfrdf  31999  eqrrabd  32009  foresf1o  32010  elabreximdv  32016  iinabrex  32068  cbvdisjf  32070  disjorf  32078  disjabrex  32081  iundisjf  32088  disjunsn  32093  brabgaf  32105  ac6sf2  32117  dfimafnf  32128  fimarab  32136  2ndresdju  32142  fmptcof2  32150  acunirnmpt2  32153  acunirnmpt2f  32154  aciunf1lem  32155  aciunf1  32156  ofpreima  32158  funcnv5mpt  32161  funcnv4mpt  32162  fnpreimac  32164  padct  32212  cnvoprabOLD  32213  f1od2  32214  fpwrelmap  32226  xrofsup  32248  iundisjfi  32275  nnindf  32293  nn0min  32294  fprodex01  32299  fsumiunle  32303  gsummpt2d  32472  gsumhashmul  32479  isarchiofld  32706  nsgmgc  32798  nsgqusf1olem1  32799  nsgqusf1olem3  32801  nsgqusf1o  32802  elrspunidl  32821  elrspunsn  32822  ply1gsumz  32945  ig1pmindeg  32948  ply1degltdimlem  32996  fedgmullem2  33004  evls1fldgencl  33034  irngnzply1  33045  ply1annidllem  33052  algextdeglem6  33068  reff  33118  locfinreflem  33119  cmpcref  33129  zarclsiin  33150  zarcls  33153  zarcmplem  33160  ordtconnlem1  33203  qqhval2  33261  prodindf  33320  esumeq12dva  33329  esumeq2dv  33335  esumrnmpt  33349  esumpad  33352  esumpad2  33353  esumadd  33354  gsumesum  33356  esumlub  33357  esumsnf  33361  esumpr  33363  esumrnmpt2  33365  esumfzf  33366  esumfsup  33367  esumpcvgval  33375  esumpmono  33376  esumcocn  33377  hasheuni  33382  esumcvg  33383  esumgect  33387  esum2dlem  33389  esum2d  33390  esumiun  33391  ldsysgenld  33457  sigapildsyslem  33458  sigapildsys  33459  ldgenpisyslem1  33460  fiunelros  33471  measvunilem  33509  measvunilem0  33510  measvuni  33511  measiun  33515  measinblem  33517  voliune  33526  volfiniune  33527  volmeas  33528  ddemeas  33533  oms0  33595  omssubadd  33598  carsgclctunlem1  33615  carsggect  33616  omsmeas  33621  eulerpartlemgvv  33674  dstrvprob  33769  ballotlemodife  33795  reprsuc  33926  reprdifc  33938  breprexplema  33941  breprexplemc  33943  circlemethhgt  33954  hgt750lemd  33959  bnj919  34077  bnj1146  34101  bnj1379  34140  bnj1385  34142  bnj1400  34145  bnj1534  34163  bnj1542  34167  bnj110  34168  bnj121  34180  bnj124  34181  bnj130  34184  bnj207  34191  bnj571  34216  bnj605  34217  bnj580  34223  bnj607  34226  bnj611  34228  bnj873  34234  bnj849  34235  bnj900  34239  bnj916  34243  bnj1000  34251  bnj964  34253  bnj981  34260  bnj985v  34263  bnj985  34264  bnj1014  34271  bnj1123  34296  bnj1128  34300  bnj1228  34321  bnj1204  34322  bnj1279  34328  bnj1307  34333  bnj1321  34337  bnj1388  34343  bnj1398  34344  bnj1408  34346  bnj1417  34351  bnj1444  34353  bnj1445  34354  bnj1446  34355  bnj1449  34358  bnj1467  34364  bnj1489  34366  bnj1312  34368  bnj1497  34370  bnj1518  34374  bnj1525  34379  bnj1529  34380  fineqvrep  34394  cvmcov  34553  untsucf  34984  setinds2  35057  dfon2lem1  35060  dfon2lem3  35062  gg-dvfsumlem2  35470  finminlem  35507  bj-nexdvt  35880  bj-cbvaldv  35981  bj-cbval2vv  35983  bj-cbvex2vv  35984  bj-cbvaldvav  35985  bj-cbvexdvav  35986  ax11-pm2  36018  bj-dvelimdv  36034  bj-nfeel2  36037  bj-ceqsalv  36078  bj-vtocl  36100  bj-inrab2  36112  currysetlem  36130  currysetlem1  36132  bj-opabco  36373  mptsnunlem  36523  exlimim  36527  exellim  36529  topdifinfindis  36531  topdifinffinlem  36532  icorempo  36536  isbasisrelowllem1  36540  isbasisrelowllem2  36541  relowlssretop  36548  finxpreclem2  36575  finxpreclem6  36581  fvineqsneu  36596  fvineqsneq  36597  wl-euequf  36743  wl-sb8eut  36746  wl-issetft  36748  phpreu  36776  matunitlindflem2  36789  ptrest  36791  ptrecube  36792  poimirlem2  36794  poimirlem23  36815  poimirlem24  36816  poimirlem25  36817  poimirlem26  36818  poimirlem27  36819  poimirlem28  36820  heicant  36827  mbfposadd  36839  itgabsnc  36861  itggt0cn  36862  ftc1anclem5  36869  upixp  36901  indexa  36905  indexdom  36906  filbcmb  36912  sdclem2  36914  sdclem1  36915  fdc1  36918  totbndbnd  36961  sbcalf  37286  sbcexf  37287  scottexf  37340  scott0f  37341  eqrelf  37427  fsumshftd  38126  riotasv2d  38131  riotasv2s  38132  riotasv3d  38134  glbconxN  38553  pmapglbx  38944  pmapglb2xN  38947  cdleme26ee  39535  cdleme31sn  39555  cdleme31sn1  39556  cdlemefr29exN  39577  cdlemefs32sn1aw  39589  cdleme43fsv1snlem  39595  cdleme41sn3a  39608  cdleme32fva  39612  cdleme32d  39619  cdleme32f  39621  cdleme40m  39642  cdleme40n  39643  cdleme42b  39653  cdlemk36  40088  cdlemk38  40090  cdlemkid  40111  cdlemk19x  40118  cdlemk11t  40121  dihvalcqpre  40410  mapdheq  40903  hdmap1eq  40976  hdmapval2lem  41006  lcmineqlem9  41209  lcmineqlem12  41212  aks4d1p1p2  41242  sticksstones1  41269  sticksstones11  41279  sticksstones16  41285  sticksstones22  41291  metakunt33  41324  mzpexpmpt  41786  eq0rabdioph  41817  rexrabdioph  41835  rexfrabdioph  41836  elnn0rabdioph  41844  dvdsrabdioph  41851  fphpd  41857  monotuz  41983  monotoddzz  41985  oddcomabszz  41986  setindtr  42066  dford4  42071  wdom2d2  42077  aomclem6  42104  aomclem8  42106  flcidc  42219  areaquad  42268  unielss  42270  onsucf1lem  42322  oaun3lem1  42427  nadd1suc  42445  naddsuc2  42446  rababg  42628  ss2iundv  42714  cbviuneq12dv  42716  gneispace  43188  mnringvald  43270  mnringmulrcld  43290  nfscott  43301  scottabf  43302  scottab  43303  mnuprdlem4  43337  ismnushort  43363  binomcxplemdvsum  43417  binomcxplemnotnn0  43418  aaanv  43450  pm11.57  43451  pm11.58  43452  pm11.59  43453  pm11.71  43459  pm14.12  43483  ssralv2  43595  tratrb  43600  iunconnlem2  43999  evth2f  44002  elunif  44003  fvelrnbf  44005  evthf  44014  fnchoice  44016  sumpair  44022  rfcnnnub  44023  refsum2cn  44025  uzwo4  44042  fiiuncl  44054  fiunicl  44056  elintdv  44070  ssd  44071  cbvmpo2  44088  cbvmpo1  44089  eliin2f  44095  eliuniin2  44111  cbvrabv2  44118  cbvrabv2w  44119  suprnmpt  44172  disjf1  44181  disjrnmpt2  44186  disjf1o  44189  disjinfi  44190  choicefi  44198  iunmapsn  44215  axccdom  44220  dmrelrnrel  44224  axccd  44227  fmptf  44241  rnmptlb  44246  rnmptbddlem  44247  rnmptbd2lem  44251  rnmptbdlem  44258  rnmptbd  44259  fmptff  44273  upbdrech  44314  ssfiunibd  44318  supxrgere  44342  iuneqfzuzlem  44343  supxrgelem  44346  supxrge  44347  suplesup  44348  infrpge  44360  xralrple2  44363  infxr  44376  infxrunb2  44377  infleinf  44381  xrralrecnnle  44392  xrralrecnnge  44399  supxrunb3  44408  supxrleubrnmpt  44415  infleinf2  44423  unb2ltle  44424  rexabslelem  44427  rexabsle  44428  allbutfiinf  44429  suprleubrnmpt  44431  infrnmptle  44432  infxrunb3rnmpt  44437  uzublem  44439  uzub  44440  supminfrnmpt  44454  infxrpnf  44455  supxrleubrnmptf  44460  infxrgelbrnmpt  44463  infrpgernmpt  44474  supminfxr2  44478  monoordxr  44492  monoord2xr  44494  caucvgbf  44499  cvgcaule  44501  rexanuz2nf  44502  iccshift  44530  iooshift  44534  iooiinicc  44554  iooiinioc  44568  fsummulc1f  44586  fsumnncl  44587  fsumf1of  44589  fsumiunss  44590  fsumreclf  44591  fsumlessf  44592  fsumsermpt  44594  fmul01  44595  fmuldfeqlem1  44597  fmuldfeq  44598  fmul01lt1lem1  44599  fmul01lt1lem2  44600  fmul01lt1  44601  fprodsplit1  44608  fprodexp  44609  fprodabs2  44610  mccllem  44612  mccl  44613  fprodcnlem  44614  fprodcn  44615  climexp  44620  climsuse  44623  climrecf  44624  climinff  44626  climaddf  44630  mullimc  44631  ellimcabssub0  44632  islptre  44634  climf  44637  mullimcf  44638  rexlim2d  44640  idlimc  44641  limcperiod  44643  limcrecl  44644  sumnnodd  44645  islpcn  44654  limsupre  44656  limcleqr  44659  neglimc  44662  addlimc  44663  0ellimcdiv  44664  limclner  44666  climsubmpt  44675  climreclf  44679  climf2  44681  fnlimcnv  44682  climeldmeqmpt  44683  clim2f2  44685  climfveqmpt  44686  fnlimfvre  44689  allbutfifvre  44690  climleltrp  44691  fnlimf  44693  fnlimabslt  44694  climfveqmpt3  44697  climeldmeqf  44698  limsupref  44700  limsupbnd1f  44701  climbddf  44702  climeqf  44703  climeldmeqmpt3  44704  limsuplesup  44714  limsuppnfd  44717  limsupub  44719  limsupres  44720  climinf2lem  44721  climinf2  44722  limsuppnf  44726  limsupubuzlem  44727  limsupubuz  44728  climinf2mpt  44729  climinfmpt  44730  climinf3  44731  limsupmnflem  44735  limsupmnf  44736  limsupequz  44738  limsupre2  44740  limsupmnfuzlem  44741  limsupmnfuz  44742  limsupequzmptf  44746  limsupre3lem  44747  limsupre3  44748  limsupre3uzlem  44750  limsupre3uz  44751  limsupreuz  44752  limsupvaluz2  44753  limsupreuzmpt  44754  supcnvlimsup  44755  climuzlem  44758  climuz  44759  climisp  44761  lmbr3  44762  climrescn  44763  climxrrelem  44764  climxrre  44765  liminfcl  44778  liminfval2  44783  limsup10exlem  44787  liminflelimsuplem  44790  limsupgtlem  44792  limsupgt  44793  climliminflimsupd  44816  liminfreuzlem  44817  liminfreuz  44818  liminfltlem  44819  liminflt  44820  limsupub2  44827  xlimpnfxnegmnf  44829  liminflbuz2  44830  liminfpnfuz  44831  liminflimsupxrre  44832  xlimmnfvlem1  44847  xlimmnfvlem2  44848  xlimmnfv  44849  xlimpnfvlem1  44851  xlimpnfvlem2  44852  xlimpnfv  44853  xlimmnf  44856  xlimpnf  44857  xlimmnfmpt  44858  xlimpnfmpt  44859  climxlim2lem  44860  dfxlim2  44863  cncfshift  44889  icccncfext  44902  cncficcgt0  44903  cncfiooicc  44909  cncfioobd  44912  fprodcncf  44915  fprodsubrecnncnvlem  44922  fprodaddrecnncnvlem  44924  dvmptmulf  44952  dvnmptdivc  44953  dvnmul  44958  dvmptfprodlem  44959  dvmptfprod  44960  dvnprodlem1  44961  dvnprodlem2  44962  iblsplitf  44985  iblspltprt  44988  itgioocnicc  44992  iblcncfioo  44993  itgspltprt  44994  itgperiod  44996  stoweidlem3  45018  stoweidlem14  45029  stoweidlem17  45032  stoweidlem19  45034  stoweidlem20  45035  stoweidlem26  45041  stoweidlem27  45042  stoweidlem28  45043  stoweidlem29  45044  stoweidlem31  45046  stoweidlem34  45049  stoweidlem35  45050  stoweidlem36  45051  stoweidlem39  45054  stoweidlem42  45057  stoweidlem43  45058  stoweidlem44  45059  stoweidlem46  45061  stoweidlem48  45063  stoweidlem49  45064  stoweidlem50  45065  stoweidlem51  45066  stoweidlem52  45067  stoweidlem53  45068  stoweidlem54  45069  stoweidlem56  45071  stoweidlem57  45072  stoweidlem59  45074  stoweidlem60  45075  stoweidlem61  45076  stoweidlem62  45077  stoweid  45078  wallispilem3  45082  stirlinglem13  45101  stirling  45104  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem31  45153  fourierdlem39  45161  fourierdlem48  45169  fourierdlem51  45172  fourierdlem53  45174  fourierdlem68  45189  fourierdlem69  45190  fourierdlem71  45192  fourierdlem73  45194  fourierdlem77  45198  fourierdlem80  45201  fourierdlem81  45202  fourierdlem82  45203  fourierdlem83  45204  fourierdlem86  45207  fourierdlem87  45208  fourierdlem89  45210  fourierdlem91  45212  fourierdlem93  45214  fourierdlem94  45215  fourierdlem103  45224  fourierdlem104  45225  fourierdlem112  45233  fourierdlem113  45234  elaa2  45249  etransclem18  45267  etransclem22  45271  etransclem23  45272  etransclem32  45281  etransclem35  45284  etransclem44  45293  etransclem46  45295  etransclem48  45297  rrndistlt  45305  ioorrnopnlem  45319  saliuncl  45338  saliincl  45342  intsaluni  45344  salexct  45349  subsaliuncl  45373  sge00  45391  sge0revalmpt  45393  sge0sn  45394  sge0f1o  45397  sge0gerp  45410  sge0pnffigt  45411  sge0lefi  45413  sge0ltfirp  45415  sge0resrnlem  45418  sge0resplit  45421  sge0lempt  45425  sge0iunmptlemfi  45428  sge0p1  45429  sge0iunmptlemre  45430  sge0fodjrnlem  45431  sge0iunmpt  45433  sge0rpcpnf  45436  sge0ltfirpmpt2  45441  sge0isum  45442  sge0xp  45444  sge0ad2en  45446  sge0isummpt2  45447  sge0xaddlem1  45448  sge0xaddlem2  45449  sge0xadd  45450  sge0pnffsumgt  45457  sge0gtfsumgt  45458  sge0uzfsumgt  45459  sge0seq  45461  sge0reuz  45462  sge0reuzb  45463  iundjiun  45475  meadjiunlem  45480  meadjiun  45481  ismeannd  45482  voliunsge0lem  45487  meaiuninclem  45495  meaiunincf  45498  meaiuninc3v  45499  meaiuninc3  45500  meaiininclem  45501  meaiininc  45502  meaiininc2  45503  caragenfiiuncl  45530  omeiunltfirp  45534  carageniuncllem1  45536  carageniuncllem2  45537  caratheodorylem2  45542  0ome  45544  isomenndlem  45545  hoicvrrex  45571  ovnsupge0  45572  ovnlecvr  45573  ovnlerp  45577  ovncvrrp  45579  ovn0lem  45580  ovnsubaddlem1  45585  ovnsubaddlem2  45586  hoidmvcl  45597  hsphoidmvle2  45600  hsphoidmvle  45601  hoidmvval0  45602  sge0hsphoire  45604  hoidmvval0b  45605  hoidmv1lelem1  45606  hoidmv1lelem2  45607  hoidmv1lelem3  45608  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  hoidmvlelem5  45614  hoidmvle  45615  ovnhoilem1  45616  ovnhoilem2  45617  ovnhoi  45618  ovnlecvr2  45625  hspdifhsp  45631  hoidifhspdmvle  45635  hoiqssbllem3  45639  hspmbllem1  45641  hspmbllem2  45642  opnvonmbllem1  45647  opnvonmbllem2  45648  ovnsubadd2lem  45660  ovolval5lem1  45667  ovnovollem1  45671  ovnovollem2  45672  hoimbl2  45680  vonhoire  45687  iinhoiicclem  45688  iinhoiicc  45689  iunhoiioolem  45690  iunhoiioo  45691  vonioolem1  45695  vonioolem2  45696  vonioo  45697  vonicclem1  45698  vonicclem2  45699  vonicc  45700  vonn0ioo2  45705  vonn0icc2  45707  vonct  45708  pimltmnf2f  45712  pimgtpnf2f  45720  salpreimagelt  45722  salpreimalegt  45724  pimltpnf2f  45727  pimgtmnf2  45729  pimdecfgtioc  45730  pimincfltioc  45731  pimdecfgtioo  45732  pimincfltioo  45733  preimageiingt  45735  preimaleiinlt  45736  salpreimagtge  45740  salpreimaltle  45741  salpreimalelt  45744  salpreimagtlt  45745  issmff  45749  sssmf  45753  mbfresmf  45754  cnfsmf  45755  incsmflem  45756  incsmf  45757  smfsssmf  45758  issmflelem  45759  issmfle  45760  smfconst  45764  issmfgtlem  45770  issmfgt  45771  smfpimltxrmptf  45773  smfmbfcex  45775  smfaddlem1  45778  smfaddlem2  45779  smfadd  45780  decsmflem  45781  decsmf  45782  smfpreimagtf  45783  issmfgelem  45784  issmfge  45785  smflimlem2  45787  smflimlem4  45789  smflim  45792  smfpimgtxr  45795  smfpimgtxrmptf  45799  smfpimioo  45802  smfresal  45803  smfrec  45804  smfres  45805  smfmullem2  45807  smfmullem4  45809  smfmul  45810  smfpimbor1lem2  45814  smf2id  45816  smfco  45817  smflim2  45821  smfpimcc  45823  smflimmpt  45825  smfsuplem1  45826  smfsuplem3  45828  smfsup  45829  smfsupmpt  45830  smfsupxr  45831  smfinflem  45832  smfinf  45833  smfinfmpt  45834  smflimsuplem3  45837  smflimsuplem4  45838  smflimsuplem5  45839  smflimsuplem7  45841  smflimsuplem8  45842  smflimsup  45843  smflimsupmpt  45844  smfliminflem  45845  smfliminf  45846  smfliminfmpt  45847  smfpimne2  45855  fsupdm  45857  smfsupdmmbllem  45859  smfsupdmmbl  45860  finfdm  45861  smfinfdmmbllem  45863  smfinfdmmbl  45864  or2expropbilem1  46041  or2expropbilem2  46042  or2expropbi  46043  cfsetsnfsetf  46067  cfsetsnfsetfo  46069  rexsb  46106  reuf1odnf  46114  2reu8i  46120  ffnafv  46178  tz6.12c-afv2  46249  f1oresf1o2  46298  iccelpart  46400  iccpartdisj  46404  dfich2  46425  ichbi12i  46427  ichnfimlem  46430  ich2exprop  46438  ichnreuop  46439  ichreuopeq  46440  sprsymrelfo  46464  reupr  46489  reuopreuprim  46493  mogoldbb  46752  2zrngagrp  46930  2zrngmmgm  46933  opeliun2xp  47097  cbvmpox2  47100  ovmpordx  47104  1arymaptfo  47417  2arymaptfo  47428  mo0sn  47588  isthincd2lem1  47735  nfintd  47806  nfiund  47807  nfiundg  47808  iunord  47809  spcdvw  47812  nfsetrecs  47819  setrec1lem2  47821  setrec1  47824  setrec2fun  47825  pgindnf  47849  pgind  47850  aacllem  47936