Theorem nfv 1947

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

This proof depends on syntax axioms:  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfvd  1948  cbvaldw  2369  cbval2v  2374  dvelimhw  2376  pm11.53  2377  19.12vv  2378  eeanv  2380  eeeanv  2381  ee4anv  2382  sbnf2  2389  exsb  2390  2exsb  2391  sbbibvv  2393  cbvsbvf  2394  cleljustALT2  2396  spimv  2421  spimev  2423  chvarv  2427  cbvalv  2431  cbvexv  2432  cbvald  2438  cbvaldva  2440  cbvexdva  2441  cbval2  2442  axc16i  2467  dvelimnf  2484  sbel2x  2505  sbiedv  2535  2sbiev  2536  sbid2v  2540  sbhb  2552  2sb8e  2561  nfmod2  2585  nfmodv  2586  mof  2590  mo4f  2594  euf  2603  sb8eulem  2625  cbvmow  2630  sbmo  2641  moexexvw  2655  moexexv  2666  2mo  2675  2eu6  2683  axextmo  2738  nulmo  2739  abbib  2831  cleqh  2891  nfcv  2924  nfeqd  2934  nfeld  2935  nfabdw  2945  nfabd  2946  dvelimdc  2948  nfcvf  2950  cleqf  2952  r19.29af  3273  rexbidvALT  3279  rexbidvaALT  3280  2ralbida  3287  r19.12  3313  reean  3314  cbvrexsvw  3316  sbralieOLD  3342  cbvralf  3347  cbvralv  3351  cbvrexv  3352  cbvralsv  3353  cbvrexsv  3354  cbvrmow  3392  cbvreu  3406  cbvrmov  3408  cbvreuv  3409  cbvrab  3452  cbvexeqsetf  3468  ceqsex2  3503  vtocl2gaf  3541  vtocl3gaf  3542  spc2ed  3558  rspct  3565  rspc  3567  rspce  3568  eqvincf  3607  elrab3t  3647  ralab2  3658  rexab2  3660  mob2  3676  mob  3678  reu2  3686  rmo4f  3696  reu2eqd  3697  cdeqab1  3733  nfcdeq  3738  sbcco  3768  cbvsbcv  3778  elrabsf  3787  sbc2iegf  3816  reu8nf  3827  rmo2  3837  rmo3  3839  rmoanimALT  3846  nfcsb1d  3872  nfcsbd  3875  csbiebt  3879  csbie2t  3888  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  cbvralv2  3896  cbvrexv2  3897  rspc2vd  3898  dfssf  3925  rabss3d  4032  eqrrabd  4037  uniiunlem  4038  ab0orv  4335  ab0orvALT  4336  sbcnestgw  4384  sbcnestg  4389  sbnfc2  4400  r19.3rzvOLD  4463  r19.28zv  4465  r19.27zv  4470  2reu4lem  4482  nfifd  4515  reusngf  4638  reusng  4641  rexreusng  4643  reuprg0  4666  rabsnifsb  4686  euabsn  4690  nfunid  4876  eluniab  4884  nfint  4920  iuneqconst  4966  disjiun  5095  disjxun  5105  nfopabd  5177  cbvopab  5181  cbvopab1  5183  cbvopab1g  5184  cbvopab2  5185  cbvopab1s  5186  mpteq12da  5192  mpteq12f  5194  cbvmptf  5209  cbvmptfg  5210  axrep1  5237  axrep2  5239  axrep3  5240  axrep4OLD  5243  axrep5  5244  zfrepclf  5250  reusv2lem3  5369  reusv2lem4  5370  reusv2  5372  reusv3  5374  alxfr  5376  ralxfrALT  5384  axprlem3OLD  5398  axprlem4OLD  5399  axprlem5OLD  5400  copsex2t  5473  iunopeqop  5502  iunopeqopOLD  5503  rexopabb  5510  opelopabaf  5527  nfso  5574  pofun  5585  isso2i  5604  nffr  5632  opeliunxp  5726  opeliun2xp  5727  opeliunxp2  5822  ralxpf  5830  dfdmf  5884  dfrnf  5938  elrnmpt1  5948  dfrel4  6188  reuop  6295  frpoinsg  6345  frpoins2g  6347  wfis2g  6357  nfiotadw  6496  nfiotad  6498  cbviotaw  6500  cbviota  6502  cbviotav  6503  sb8iota  6504  iota2d  6525  iota2  6526  dffun6f  6552  imadif  6621  isarep1  6625  isarep2  6626  fv3  6900  tz6.12f  6907  funimassd  6948  fvelimad  6949  feqmptdf  6952  fimarab  6956  opabiotafun  6962  funfv2f  6971  fvmptd  6998  fvmptd2f  7007  fvmptdv  7008  fvmptt  7011  fvopab5  7024  eqfnfv2f  7030  ralrnmptw  7090  ralrnmpt  7092  dffo3f  7102  f1ompt  7107  fompt  7114  ffnfv  7115  ffnfvf  7116  f1ossf1o  7125  fmptco  7126  elabrex  7242  elabrexg  7243  dff13f  7255  fsnex  7287  fliftfun  7316  cbvriotaw  7382  cbvriota  7386  cbvriotav  7387  riota2  7398  riotaeqimp  7399  riota5f  7401  oprabv  7476  nfoprab  7480  mpoeq123  7488  cbvoprab1  7503  cbvoprab2  7504  cbvoprab12  7505  cbvoprab3  7507  cbvmpox  7509  ralrnmpo  7555  ovmpodx  7567  ovmpodf  7572  ovmpodv  7573  ov3  7579  ovmpt3rab1  7675  ofrfval2  7702  onminex  7804  tfis  7854  tfis2  7856  tfisi  7858  tfinds  7859  tfindes  7862  findes  7900  fiun  7943  f1iun  7944  abrexex2g  7964  opabex3d  7965  opabex3rd  7966  opabex3  7967  dfoprab4f  8056  fmpox  8067  offval22  8088  ovmptss  8093  ralxpes  8137  ralxp3  8139  ralxp3es  8140  frpoins3xpg  8141  frpoins3xp3g  8142  opeliunxp2f  8211  tposoprab  8263  fvmpocurryd  8272  nffrecs  8285  tfr3  8391  nfrdg  8406  tz7.48-1  8435  tz7.49  8437  naddsuc2  8693  eqerlem  8735  erovlem  8816  mptelixpg  8945  boxcutc  8951  dom2lem  9001  xpf1o  9140  mapxpen  9144  findcard2  9162  pssnn  9166  nneneq  9203  ac6sfi  9257  fiint  9299  indexfi  9330  wdom2d  9555  ixpiunwdom  9565  cantnflem1  9671  nfttrcld  9692  setinds2  9733  frinsg  9736  frins2  9739  r1val1  9771  rankuni2b  9838  nfscott  9874  scottabf  9881  scottab  9882  scottexsOLD  9885  scott0bsOLD  9887  dfac8clem  10038  acni2  10052  aceq1  10123  dfac5lem5  10133  kmlem15  10170  infpssrlem4  10311  fin23lem27  10333  hsmexlem2  10432  hsmexlem4  10434  axcc3  10443  domtriomlem  10447  axdc3lem2  10456  axdc3lem4  10458  axdc4lem  10460  ac6c4  10486  zorn2lem4  10504  zorn2lem5  10505  iunfo  10548  iundom2g  10549  uniimadomf  10554  konigthlem  10578  axrepndlem2  10603  axunnd  10606  axpowndlem2  10608  axpowndlem4  10610  axregndlem2  10613  axacndlem5  10621  zfcndrep  10624  zfcndinf  10628  pwfseqlem4a  10671  pwfseqlem4  10672  tskuni  10793  gruiin  10820  reclem2pr  11058  dedekind  11398  dedekindle  11399  fimaxre3  12186  nn0ind-raph  12722  uzind4s  12958  nnwof  12964  lbzbi  12986  fzrevral  13667  rabssnn0fi  14050  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  fsuppmapnn0fiubex  14056  seqof2  14124  reuccatpfxs1  14816  cotr2g  15049  rlim2  15583  ello1mpt  15608  climeu  15642  o1compt  15674  summolem2a  15801  zsum  15804  sumss  15810  sumss2  15812  fsumcvg2  15813  fsumclf  15824  fsumsplitf  15828  fsumsplit1  15831  fsum2dlem  15856  fsum00  15885  o1fsum  15900  nfcprod1  15997  nfcprod  15998  prodmolem2a  16023  zprod  16026  fprod  16030  fprodntriv  16031  prodss  16036  fprodn0  16068  fprod2dlem  16069  fprodsplitf  16077  fprodsplit1f  16079  fprodle  16085  fprodmodd  16086  lcmfunsnlem1  16729  lcmfunsnlem2lem1  16730  lcmfunsnlem2  16732  coprmprod  16753  coprmproddvdslem  16754  prmind2  16777  iserodd  16929  pcmpt  16986  pcmptdvds  16988  prmolefac  17140  mreexexd  17738  catpropd  17799  invfuc  18068  natpropd  18070  fucpropd  18071  initoeu2  18107  acsmapd  18644  nfchnd  18701  symgval  19497  gsumsnd  20078  gsumsnf  20079  gsumunsnfd  20083  gsummptf1o  20089  gsummpt1n0  20091  gsum2d2lem  20099  gsumcom2  20101  gsummptnn0fz  20112  dprd2d2  20172  rngqiprngimf1  21502  gsummoncoe1  22532  gsumply1eq  22533  mdetralt2  22830  mdetunilem2  22834  madugsum  22864  gsummatr01lem4  22879  matunitlindflem2  22901  cpmatmcllem  22942  cayleyhamilton1  23116  neiptopnei  23356  neiptopreu  23357  neitr  23404  fiuncmp  23628  iunconnlem  23651  iunconn  23652  2ndcdisj  23681  dissnlocfin  23754  elptr2  23799  ptbasfi  23806  ptcld  23838  ptcldmpt  23839  ptclsg  23840  ptcnplem  23846  ptcnp  23847  cnmpt11  23888  cnmpt21  23896  cnmptcom  23903  imasnopn  23915  imasncld  23916  imasncls  23917  xkocnv  24039  elmptrab  24052  isfildlem  24082  alexsubALTlem3  24274  cnextfvval  24290  utopsnneiplem  24472  isucn2  24503  cfilucfil  24784  blval2  24787  restmetu  24795  ovoliunlem3  25731  ovoliun  25732  ovoliun2  25733  ovoliunnul  25734  finiunmbl  25771  volfiniun  25774  iundisj  25775  iunmbl  25780  voliun  25781  iunmbl2  25784  mbfeqalem1  25868  mbfsup  25891  mbfinf  25892  mbflim  25895  itg2splitlem  25975  itg2split  25976  isibl2  25993  cbvitg  26003  itgeqa  26041  itgss3  26042  itgfsum  26054  itgabs  26062  itggt0  26071  itgcn  26072  limcmpt  26110  limciun  26121  dvmptfsum  26202  dvlipcn  26221  dvfsumlem2  26254  dvfsumlem4  26256  dvfsumrlim  26258  dvfsum2  26261  itgsubst  26276  coeeq2  26467  dgrle  26468  ulmss  26628  leibpi  27175  rlimcnp  27198  rlimcnp2  27199  o1cxp  27207  lgamgulmlem2  27262  lgamgulmlem6  27266  fsumdvdscom  27417  lgseisenlem2  27608  2sqmo  27669  2sqreulem4  27686  dchrisumlema  27720  dchrisumlem2  27722  dchrisumlem3  27723  nosupbnd1  27946  nosupbnd2  27948  noinfbnd1  27961  noinfbnd2  27963  bdayiun  28176  bdaypw2n0bndlem  28724  istrkg2ld  28797  prlngmo2  29297  mpteleeOLD  29336  gropd  29472  grstructd  29473  clwwlknonclwlknonf1o  30826  dlwwlknondlwlknonf1o  30829  ex-natded9.26  30883  isch3  31706  atom1d  32818  chirred  32860  sbc2iedf  32925  rspc2daf  32926  19.9d2r  32930  opreu2reuALT  32936  mo5f  32948  reuxfrdf  32950  foresf1o  32963  elabreximdv  32970  iinabrex  33027  cbvdisjf  33029  disjorf  33037  disjabrex  33040  iundisjf  33047  disjunsn  33052  brabgaf  33064  ac6sf2  33080  dfimafnf  33094  2ndresdju  33107  fmptcof2  33115  acunirnmpt2  33118  acunirnmpt2f  33119  aciunf1lem  33120  aciunf1  33121  ofpreima  33123  funcnv5mpt  33125  funcnv4mpt  33126  fnpreimac  33128  f1od2  33175  fpwrelmap  33189  xrofsup  33223  iundisjfi  33252  nnindf  33275  nn0min  33276  fprodex01  33280  fsumiunle  33284  prodindf  33293  gsummpt2d  33474  gsummptf1od  33480  gsummptfsf1o  33485  gsumhashmul  33492  suppgsumssiun  33497  gsumwrd2dccat  33503  isarchiofld  33624  elrgspnsubrunlem2  33673  nsgmgc  33826  nsgqusf1olem1  33827  nsgqusf1olem3  33829  nsgqusf1o  33830  elrspunidl  33841  elrspunsn  33842  deg1prod  33978  ply1gsumz  33994  ig1pmindeg  33997  mplvrpmga  34040  psrgsum  34043  psrmonprod  34047  esplylem  34061  esplyfv1  34064  esplyfval1  34068  esplyfvaln  34069  esplyind  34070  vieta  34075  exsslsb  34092  ply1degltdimlem  34117  fedgmullem2  34125  evls1fldgencl  34165  irngnzply1  34186  extdgfialglem2  34188  ply1annidllem  34196  algextdeglem6  34217  constrfin  34241  reff  34334  locfinreflem  34335  cmpcref  34345  zarclsiin  34366  zarcls  34369  zarcmplem  34376  ordtconnlem1  34419  qqhval2  34477  esumeq12dva  34527  esumeq2dv  34533  esumrnmpt  34547  esumpad  34550  esumpad2  34551  esumadd  34552  gsumesum  34554  esumlub  34555  esumsnf  34559  esumpr  34561  esumrnmpt2  34563  esumfzf  34564  esumfsup  34565  esumpcvgval  34573  esumpmono  34574  esumcocn  34575  hasheuni  34580  esumcvg  34581  esumgect  34585  esum2dlem  34587  esum2d  34588  esumiun  34589  ldsysgenld  34656  sigapildsyslem  34657  sigapildsys  34658  ldgenpisyslem1  34659  fiunelros  34670  measvunilem  34708  measvunilem0  34709  measvuni  34710  measiun  34714  measinblem  34716  voliune  34725  volfiniune  34726  volmeas  34727  ddemeas  34732  oms0  34793  omssubadd  34796  carsgclctunlem1  34813  carsggect  34814  omsmeas  34819  eulerpartlemgvv  34872  dstrvprob  34968  ballotlemodife  34994  reprsuc  35108  reprdifc  35120  breprexplema  35123  breprexplemc  35125  circlemethhgt  35136  hgt750lemd  35141  bnj919  35262  bnj1146  35285  bnj1379  35324  bnj1385  35326  bnj1400  35329  bnj1534  35347  bnj1542  35351  bnj110  35352  bnj121  35364  bnj124  35365  bnj130  35368  bnj207  35375  bnj571  35400  bnj605  35401  bnj580  35407  bnj607  35410  bnj611  35412  bnj873  35418  bnj849  35419  bnj900  35423  bnj916  35427  bnj1000  35435  bnj964  35437  bnj981  35444  bnj985v  35447  bnj985  35448  bnj1014  35455  bnj1123  35480  bnj1128  35484  bnj1228  35505  bnj1204  35506  bnj1279  35512  bnj1307  35517  bnj1321  35521  bnj1388  35527  bnj1398  35528  bnj1408  35530  bnj1417  35535  bnj1444  35537  bnj1445  35538  bnj1446  35539  bnj1449  35542  bnj1467  35548  bnj1489  35550  bnj1312  35552  bnj1497  35554  bnj1518  35558  bnj1525  35563  bnj1529  35564  dvelimalcased  35569  dvelimexcased  35571  fineqvrep  35625  axsepg2  35651  axsepg3  35652  axsepg3ALT  35653  axpowg2  35658  axpowg3  35659  onvf1odlem2  35686  cvmcov  35827  untsucf  36274  dfon2lem1  36345  dfon2lem3  36347  finminlem  36922  weiunpo  37069  weiunso  37070  weiunfr  37071  weiunse  37072  axtcond  37082  regsfromregtco  37142  regsfromsetind  37143  bj-nexdvt  37416  bj-cbvaldv  37527  bj-cbval2vv  37529  bj-cbvex2vv  37530  bj-cbvaldvav  37531  bj-cbvexdvav  37532  ax11-pm2  37564  bj-dvelimdv  37579  bj-nfeel2  37582  bj-ceqsalv  37622  bj-vtocl  37644  bj-inrab2  37657  currysetlem  37674  currysetlem1  37676  bj-axseprep  37804  bj-axreprepsep  37805  bj-opabco  37925  mptsnunlem  38077  exlimim  38081  exellim  38083  topdifinfindis  38085  topdifinffinlem  38086  icorempo  38090  isbasisrelowllem1  38094  isbasisrelowllem2  38095  relowlssretop  38102  finxpreclem2  38129  finxpreclem6  38135  fvineqsneu  38150  fvineqsneq  38151  wl-euequf  38322  wl-sb8eut  38326  wl-issetft  38330  phpreu  38343  ptrest  38353  ptrecube  38354  poimirlem2  38356  poimirlem23  38377  poimirlem24  38378  poimirlem25  38379  poimirlem26  38380  poimirlem27  38381  poimirlem28  38382  heicant  38389  mbfposadd  38401  itgabsnc  38423  itggt0cn  38424  ftc1anclem5  38431  upixp  38464  indexa  38468  indexdom  38469  filbcmb  38475  sdclem2  38477  sdclem1  38478  fdc1  38481  totbndbnd  38524  sbcalf  38847  sbcexf  38848  scottexf  38901  scott0f  38902  eqrelf  38991  ralrmo3  39097  disjqmap2  39559  fsumshftd  39810  riotasv2d  39815  riotasv2s  39816  riotasv3d  39818  glbconxN  40236  pmapglbx  40627  pmapglb2xN  40630  cdleme26ee  41218  cdleme31sn  41238  cdleme31sn1  41239  cdlemefr29exN  41260  cdlemefs32sn1aw  41272  cdleme43fsv1snlem  41278  cdleme41sn3a  41291  cdleme32fva  41295  cdleme32d  41302  cdleme32f  41304  cdleme40m  41325  cdleme40n  41326  cdleme42b  41336  cdlemk36  41771  cdlemk38  41773  cdlemkid  41794  cdlemk19x  41801  cdlemk11t  41804  dihvalcqpre  42093  mapdheq  42586  hdmap1eq  42659  hdmapval2lem  42689  lcmineqlem9  42888  lcmineqlem12  42891  aks4d1p1p2  42921  mndmolinv  42946  primrootsunit1  42948  primrootsunit  42949  primrootspoweq0  42957  aks6d1c1p5  42963  aks6d1c3  42974  aks6d1c4  42975  aks6d1c1rh  42976  aks6d1c2lem4  42978  aks6d1c2  42981  deg1gprod  42991  sticksstones1  42997  sticksstones11  43007  sticksstones16  43013  sticksstones22  43019  aks6d1c6lem2  43022  aks6d1c6isolem1  43025  aks6d1c6isolem2  43026  bcled  43029  bcle2d  43030  aks6d1c7lem3  43033  aks6d1c7  43035  rhmqusspan  43036  grpods  43045  unitscyglem1  43046  unitscyglem2  43047  unitscyglem3  43048  unitscyglem4  43049  unitscyglem5  43050  nfa1w  43506  mzpexpmpt  43575  eq0rabdioph  43606  rexrabdioph  43620  rexfrabdioph  43621  elnn0rabdioph  43629  dvdsrabdioph  43636  fphpd  43642  monotuz  43767  monotoddzz  43769  oddcomabszz  43770  setindtr  43850  dford4  43855  wdom2d2  43861  aomclem6  43885  aomclem8  43887  flcidc  43996  areaquad  44042  unielss  44044  onsucf1lem  44095  oaun3lem1  44200  nadd1suc  44218  rababg  44399  ss2iundv  44485  cbviuneq12dv  44487  gneispace  44959  mnringvald  45036  mnringmulrcld  45051  mnuprdlem4  45084  ismnushort  45110  binomcxplemdvsum  45164  binomcxplemnotnn0  45165  aaanv  45197  pm11.57  45198  pm11.58  45199  pm11.59  45200  pm11.71  45206  pm14.12  45230  ssralv2  45339  tratrb  45344  iunconnlem2  45742  modelaxreplem3  45788  modelaxrep  45789  permaxrep  45814  evth2f  45834  elunif  45835  fvelrnbf  45837  evthf  45846  fnchoice  45848  sumpair  45854  rfcnnnub  45855  refsum2cn  45857  uzwo4  45872  fiiuncl  45884  fiunicl  45886  elintdv  45898  ssd  45899  cbvmpo2  45914  cbvmpo1  45915  eliin2f  45921  eliuniin2  45937  cbvrabv2  45944  suprnmpt  45991  disjf1  46000  disjrnmpt2  46005  disjf1o  46008  disjinfi  46009  choicefi  46016  iunmapsn  46032  axccdom  46037  dmrelrnrel  46041  axccd  46043  fmptf  46053  rnmptlb  46057  rnmptbddlem  46058  rnmptbd2lem  46062  rnmptbdlem  46069  rnmptbd  46070  fmptff  46083  upbdrech  46123  ssfiunibd  46127  supxrgere  46148  iuneqfzuzlem  46149  supxrgelem  46152  supxrge  46153  suplesup  46154  infrpge  46166  xralrple2  46169  infxr  46181  infxrunb2  46182  infleinf  46186  xrralrecnnle  46197  xrralrecnnge  46204  supxrunb3  46213  supxrleubrnmpt  46219  infleinf2  46227  unb2ltle  46228  rexabslelem  46231  rexabsle  46232  allbutfiinf  46233  suprleubrnmpt  46235  infrnmptle  46236  infxrunb3rnmpt  46241  uzublem  46243  uzub  46244  supminfrnmpt  46258  infxrpnf  46259  supxrleubrnmptf  46264  infxrgelbrnmpt  46267  infrpgernmpt  46278  supminfxr2  46282  monoordxr  46295  monoord2xr  46297  caucvgbf  46302  cvgcaule  46304  rexanuz2nf  46305  iccshift  46333  iooshift  46337  iooiinicc  46357  iooiinioc  46371  fsummulc1f  46386  fsumnncl  46387  fsumf1of  46389  fsumiunss  46390  fsumreclf  46391  fsumlessf  46392  fsumsermpt  46394  fmul01  46395  fmuldfeqlem1  46397  fmuldfeq  46398  fmul01lt1lem1  46399  fmul01lt1lem2  46400  fmul01lt1  46401  fprodsplit1  46408  fprodexp  46409  fprodabs2  46410  mccllem  46412  mccl  46413  fprodcnlem  46414  fprodcn  46415  climexp  46420  climsuse  46423  climrecf  46424  climinff  46426  climaddf  46430  mullimc  46431  ellimcabssub0  46432  islptre  46434  climf  46437  mullimcf  46438  rexlim2d  46440  idlimc  46441  limcperiod  46443  limcrecl  46444  sumnnodd  46445  islpcn  46452  limsupre  46454  limcleqr  46457  neglimc  46460  addlimc  46461  0ellimcdiv  46462  limclner  46464  climsubmpt  46473  climreclf  46477  climf2  46479  fnlimcnv  46480  climeldmeqmpt  46481  clim2f2  46483  climfveqmpt  46484  fnlimfvre  46487  allbutfifvre  46488  climleltrp  46489  fnlimf  46491  fnlimabslt  46492  climfveqmpt3  46495  climeldmeqf  46496  limsupref  46498  limsupbnd1f  46499  climbddf  46500  climeqf  46501  climeldmeqmpt3  46502  limsuplesup  46512  limsuppnfd  46515  limsupub  46517  limsupres  46518  climinf2lem  46519  climinf2  46520  limsuppnf  46524  limsupubuzlem  46525  limsupubuz  46526  climinf2mpt  46527  climinfmpt  46528  climinf3  46529  limsupmnflem  46533  limsupmnf  46534  limsupequz  46536  limsupre2  46538  limsupmnfuzlem  46539  limsupmnfuz  46540  limsupequzmptf  46544  limsupre3lem  46545  limsupre3  46546  limsupre3uzlem  46548  limsupre3uz  46549  limsupreuz  46550  limsupvaluz2  46551  limsupreuzmpt  46552  supcnvlimsup  46553  climuzlem  46556  climuz  46557  climisp  46559  lmbr3  46560  climrescn  46561  climxrrelem  46562  climxrre  46563  liminfcl  46576  liminfval2  46581  limsup10exlem  46585  liminflelimsuplem  46588  limsupgtlem  46590  limsupgt  46591  climliminflimsupd  46614  liminfreuzlem  46615  liminfreuz  46616  liminfltlem  46617  liminflt  46618  limsupub2  46625  xlimpnfxnegmnf  46627  liminflbuz2  46628  liminfpnfuz  46629  liminflimsupxrre  46630  xlimmnfvlem1  46645  xlimmnfvlem2  46646  xlimmnfv  46647  xlimpnfvlem1  46649  xlimpnfvlem2  46650  xlimpnfv  46651  xlimmnf  46654  xlimpnf  46655  xlimmnfmpt  46656  xlimpnfmpt  46657  climxlim2lem  46658  dfxlim2  46661  cncfshift  46687  icccncfext  46700  cncficcgt0  46701  cncfiooicc  46707  cncfioobd  46710  fprodcncf  46713  fprodsubrecnncnvlem  46720  fprodaddrecnncnvlem  46722  dvmptmulf  46750  dvnmptdivc  46751  dvnmul  46756  dvmptfprodlem  46757  dvmptfprod  46758  dvnprodlem1  46759  dvnprodlem2  46760  iblsplitf  46783  iblspltprt  46786  itgioocnicc  46790  iblcncfioo  46791  itgspltprt  46792  itgperiod  46794  stoweidlem3  46816  stoweidlem14  46827  stoweidlem17  46830  stoweidlem19  46832  stoweidlem20  46833  stoweidlem26  46839  stoweidlem27  46840  stoweidlem28  46841  stoweidlem29  46842  stoweidlem31  46844  stoweidlem34  46847  stoweidlem35  46848  stoweidlem36  46849  stoweidlem39  46852  stoweidlem42  46855  stoweidlem43  46856  stoweidlem44  46857  stoweidlem46  46859  stoweidlem48  46861  stoweidlem49  46862  stoweidlem50  46863  stoweidlem51  46864  stoweidlem52  46865  stoweidlem53  46866  stoweidlem54  46867  stoweidlem56  46869  stoweidlem57  46870  stoweidlem59  46872  stoweidlem60  46873  stoweidlem61  46874  stoweidlem62  46875  stoweid  46876  wallispilem3  46880  stirlinglem13  46899  stirling  46902  fourierdlem16  46936  fourierdlem21  46941  fourierdlem22  46942  fourierdlem31  46951  fourierdlem39  46959  fourierdlem48  46967  fourierdlem51  46970  fourierdlem53  46972  fourierdlem68  46987  fourierdlem69  46988  fourierdlem71  46990  fourierdlem73  46992  fourierdlem77  46996  fourierdlem80  46999  fourierdlem81  47000  fourierdlem82  47001  fourierdlem83  47002  fourierdlem86  47005  fourierdlem87  47006  fourierdlem89  47008  fourierdlem91  47010  fourierdlem93  47012  fourierdlem94  47013  fourierdlem103  47022  fourierdlem104  47023  fourierdlem112  47031  fourierdlem113  47032  elaa2  47047  etransclem18  47065  etransclem22  47069  etransclem23  47070  etransclem32  47079  etransclem35  47082  etransclem44  47091  etransclem46  47093  etransclem48  47095  rrndistlt  47103  ioorrnopnlem  47117  saliuncl  47136  saliincl  47140  intsaluni  47142  salexct  47147  subsaliuncl  47171  sge00  47189  sge0revalmpt  47191  sge0sn  47192  sge0f1o  47195  sge0gerp  47208  sge0pnffigt  47209  sge0lefi  47211  sge0ltfirp  47213  sge0resrnlem  47216  sge0resplit  47219  sge0lempt  47223  sge0iunmptlemfi  47226  sge0p1  47227  sge0iunmptlemre  47228  sge0fodjrnlem  47229  sge0iunmpt  47231  sge0rpcpnf  47234  sge0ltfirpmpt2  47239  sge0isum  47240  sge0xp  47242  sge0ad2en  47244  sge0isummpt2  47245  sge0xaddlem1  47246  sge0xaddlem2  47247  sge0xadd  47248  sge0pnffsumgt  47255  sge0gtfsumgt  47256  sge0uzfsumgt  47257  sge0seq  47259  sge0reuz  47260  sge0reuzb  47261  iundjiun  47273  meadjiunlem  47278  meadjiun  47279  ismeannd  47280  voliunsge0lem  47285  meaiuninclem  47293  meaiunincf  47296  meaiuninc3v  47297  meaiuninc3  47298  meaiininclem  47299  meaiininc  47300  meaiininc2  47301  caragenfiiuncl  47328  omeiunltfirp  47332  carageniuncllem1  47334  carageniuncllem2  47335  caratheodorylem2  47340  0ome  47342  isomenndlem  47343  hoicvrrex  47369  ovnsupge0  47370  ovnlecvr  47371  ovnlerp  47375  ovncvrrp  47377  ovn0lem  47378  ovnsubaddlem1  47383  ovnsubaddlem2  47384  hoidmvcl  47395  hsphoidmvle2  47398  hsphoidmvle  47399  hoidmvval0  47400  sge0hsphoire  47402  hoidmvval0b  47403  hoidmv1lelem1  47404  hoidmv1lelem2  47405  hoidmv1lelem3  47406  hoidmvlelem1  47408  hoidmvlelem2  47409  hoidmvlelem3  47410  hoidmvlelem4  47411  hoidmvlelem5  47412  hoidmvle  47413  ovnhoilem1  47414  ovnhoilem2  47415  ovnhoi  47416  ovnlecvr2  47423  hspdifhsp  47429  hoidifhspdmvle  47433  hoiqssbllem3  47437  hspmbllem1  47439  hspmbllem2  47440  opnvonmbllem1  47445  opnvonmbllem2  47446  ovnsubadd2lem  47458  ovolval5lem1  47465  ovnovollem1  47469  ovnovollem2  47470  hoimbl2  47478  vonhoire  47485  iinhoiicclem  47486  iinhoiicc  47487  iunhoiioolem  47488  iunhoiioo  47489  vonioolem1  47493  vonioolem2  47494  vonioo  47495  vonicclem1  47496  vonicclem2  47497  vonicc  47498  vonn0ioo2  47503  vonn0icc2  47505  vonct  47506  pimltmnf2f  47510  pimgtpnf2f  47518  salpreimagelt  47520  salpreimalegt  47522  pimltpnf2f  47525  pimgtmnf2  47527  pimdecfgtioc  47528  pimincfltioc  47529  pimdecfgtioo  47530  pimincfltioo  47531  preimageiingt  47533  preimaleiinlt  47534  salpreimagtge  47538  salpreimaltle  47539  salpreimalelt  47542  salpreimagtlt  47543  issmff  47547  sssmf  47551  mbfresmf  47552  cnfsmf  47553  incsmflem  47554  incsmf  47555  smfsssmf  47556  issmflelem  47557  issmfle  47558  smfconst  47562  issmfgtlem  47568  issmfgt  47569  smfpimltxrmptf  47571  smfmbfcex  47573  smfaddlem1  47576  smfaddlem2  47577  smfadd  47578  decsmflem  47579  decsmf  47580  smfpreimagtf  47581  issmfgelem  47582  issmfge  47583  smflimlem2  47585  smflimlem4  47587  smflim  47590  smfpimgtxr  47593  smfpimgtxrmptf  47597  smfpimioo  47600  smfresal  47601  smfrec  47602  smfres  47603  smfmullem2  47605  smfmullem4  47607  smfmul  47608  smfpimbor1lem2  47612  smf2id  47614  smfco  47615  smflim2  47619  smfpimcc  47621  smflimmpt  47623  smfsuplem1  47624  smfsuplem3  47626  smfsup  47627  smfsupmpt  47628  smfsupxr  47629  smfinflem  47630  smfinf  47631  smfinfmpt  47632  smflimsuplem3  47635  smflimsuplem4  47636  smflimsuplem5  47637  smflimsuplem7  47639  smflimsuplem8  47640  smflimsup  47641  smflimsupmpt  47642  smfliminflem  47643  smfliminf  47644  smfliminfmpt  47645  smfpimne2  47653  fsupdm  47655  smfsupdmmbllem  47657  smfsupdmmbl  47658  finfdm  47659  smfinfdmmbllem  47661  smfinfdmmbl  47662  tmachlem-agreesn  47760  or2expropbilem1  47905  or2expropbilem2  47906  or2expropbi  47907  cfsetsnfsetf  47931  cfsetsnfsetfo  47933  rexsb  47972  reuf1odnf  47980  2reu8i  47986  ffnafv  48044  tz6.12c-afv2  48115  f1oresf1o2  48164  iccelpart  48318  iccpartdisj  48322  dfich2  48343  ichbi12i  48345  ichnfimlem  48348  ich2exprop  48356  ichnreuop  48357  ichreuopeq  48358  sprsymrelfo  48382  reupr  48407  reuopreuprim  48411  mogoldbb  48686  2zrngagrp  49149  2zrngmmgm  49152  cbvmpox2  49251  ovmpordx  49255  1arymaptfo  49558  2arymaptfo  49569  mo0sn  49729  iinfssclem3  49967  iinfssc  49968  iinfsubc  49969  infsubc2  49972  iinfconstbas  49977  isthincd2lem1  50336  nfintd  50584  nfiund  50585  nfiundg  50586  iunord  50587  spcdvw  50590  nfsetrecs  50597  setrec1lem2  50599  setrec1  50602  setrec2fun  50603  pgindnf  50627  pgind  50628  aacllem  50754