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  2342  cbval2v  2347  dvelimhw  2349  pm11.53  2350  19.12vv  2351  eeanv  2353  eeeanv  2354  ee4anv  2355  sbnf2  2362  exsb  2363  2exsb  2364  sbbibvv  2366  cbvsbvf  2367  cleljustALT2  2369  spimv  2394  spimev  2396  chvarv  2400  cbvalv  2404  cbvexv  2405  cbvald  2411  cbvaldva  2413  cbvexdva  2414  cbval2  2415  axc16i  2440  dvelimnf  2457  sbel2x  2478  sbiedv  2508  2sbiev  2509  sbid2v  2513  sbhb  2525  2sb8e  2534  nfmod2  2558  nfmodv  2559  mof  2563  mo4f  2567  euf  2576  sb8eulem  2598  cbvmow  2603  sbmo  2614  moexexvw  2628  moexexv  2639  2mo  2648  2mosOLD  2650  2eu6  2657  axextmo  2712  nulmo  2713  abbib  2805  cleqh  2865  nfcv  2898  nfeqd  2909  nfeld  2910  nfabdw  2920  nfabd  2921  dvelimdc  2923  nfcvf  2925  cleqf  2927  r19.29af  3246  rexbidvALT  3252  rexbidvaALT  3253  2ralbida  3260  r19.12  3286  reean  3287  cbvrexsvw  3289  cbvralsvwOLD  3290  sbralieOLD  3317  cbvralf  3322  cbvralv  3326  cbvrexv  3327  cbvralsv  3328  cbvrexsv  3329  cbvrmow  3367  cbvreu  3381  cbvrmov  3383  cbvreuv  3384  cbvrabwOLD  3425  cbvrab  3428  cbvexeqsetf  3444  ceqsex2  3481  vtocl2gaf  3522  vtocl2gafOLD  3523  vtocl3gaf  3524  vtocl3gafOLD  3525  spc2ed  3543  rspct  3550  rspc  3552  rspce  3553  eqvincf  3592  elrab3t  3633  ralab2  3643  rexab2  3645  mob2  3661  mob  3663  reu2  3671  rmo4f  3681  reu2eqd  3682  cdeqab1  3718  nfcdeq  3723  sbcco  3754  cbvsbcv  3764  elrabsf  3774  sbc2iegf  3803  reu8nf  3815  rmo2  3825  rmo3  3827  rmoanimALT  3833  nfcsb1d  3859  nfcsbd  3862  csbiebt  3866  csbie2t  3875  cbvrabcsfw  3878  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  cbvralv2  3883  cbvrexv2  3884  rspc2vd  3885  dfssf  3912  rabss3d  4021  eqrrabd  4026  uniiunlem  4027  ab0orv  4323  ab0orvALT  4324  sbcnestgw  4363  sbcnestg  4368  sbnfc2  4379  r19.3rzvOLD  4444  r19.28zv  4446  r19.27zv  4451  2reu4lem  4463  nfifd  4496  reusngf  4618  reusng  4621  rexreusng  4623  reuprg0  4646  rabsnifsb  4666  euabsn  4670  nfunid  4856  eluniab  4864  nfint  4899  iuneqconst  4945  disjiun  5073  disjxun  5083  nfopabd  5153  cbvopab  5157  cbvopab1  5159  cbvopab1g  5160  cbvopab2  5161  cbvopab1s  5162  mpteq12da  5168  mpteq12f  5170  cbvmptf  5185  cbvmptfg  5186  axrep1  5213  axrep2  5215  axrep3  5216  axrep4OLD  5219  axrep5  5220  zfrepclf  5226  reusv2lem3  5342  reusv2lem4  5343  reusv2  5345  reusv3  5347  alxfr  5349  ralxfrALT  5357  axprlem3OLD  5371  axprlem4OLD  5372  axprlem5OLD  5373  copsex2t  5446  iunopeqop  5475  iunopeqopOLD  5476  rexopabb  5483  opelopabaf  5499  nfso  5546  pofun  5557  isso2i  5576  nffr  5604  opeliunxp  5698  opeliun2xp  5699  opeliunxp2  5793  ralxpf  5801  dfdmf  5851  dfrnf  5905  elrnmpt1  5915  dfrel4  6155  reuop  6257  frpoinsg  6307  frpoins2g  6309  wfis2g  6319  nfiotadw  6457  nfiotad  6459  cbviotaw  6461  cbviota  6463  cbviotav  6464  sb8iota  6465  iota2d  6486  iota2  6487  dffun6f  6513  imadif  6582  isarep1  6587  isarep2  6588  fv3  6858  tz6.12f  6865  funimassd  6906  fvelimad  6907  feqmptdf  6910  fimarab  6914  opabiotafun  6920  funfv2f  6929  fvmptd  6955  fvmptd2f  6964  fvmptdv  6965  fvmptt  6968  fvopab5  6981  eqfnfv2f  6987  ralrnmptw  7046  ralrnmpt  7048  dffo3f  7058  f1ompt  7063  fompt  7070  ffnfv  7071  ffnfvf  7072  f1ossf1o  7081  fmptco  7082  elabrex  7197  elabrexg  7198  dff13f  7210  fsnex  7238  fliftfun  7267  cbvriotaw  7333  cbvriota  7337  cbvriotav  7338  riota2  7349  riotaeqimp  7350  riota5f  7352  oprabv  7427  nfoprab  7431  mpoeq123  7439  cbvoprab1  7454  cbvoprab2  7455  cbvoprab12  7456  cbvoprab3  7458  cbvmpox  7460  ralrnmpo  7506  ovmpodx  7518  ovmpodf  7523  ovmpodv  7524  ov3  7530  ovmpt3rab1  7625  ofrfval2  7652  onminex  7756  tfis  7806  tfis2  7808  tfisi  7810  tfinds  7811  tfindes  7814  findes  7851  fiun  7896  f1iun  7897  abrexex2g  7917  opabex3d  7918  opabex3rd  7919  opabex3  7920  dfoprab4f  8009  fmpox  8020  offval22  8038  ovmptss  8043  ralxpes  8086  ralxp3  8088  ralxp3es  8089  frpoins3xpg  8090  frpoins3xp3g  8091  opeliunxp2f  8160  tposoprab  8212  fvmpocurryd  8221  nffrecs  8233  tfr3  8338  nfrdg  8353  tz7.48-1  8382  tz7.49  8384  naddsuc2  8637  eqerlem  8679  erovlem  8760  mptelixpg  8883  boxcutc  8889  dom2lem  8939  xpf1o  9077  mapxpen  9081  findcard2  9099  pssnn  9103  nneneq  9140  ac6sfi  9194  fiint  9237  indexfi  9270  wdom2d  9495  ixpiunwdom  9505  cantnflem1  9610  nfttrcld  9631  setinds2  9672  frinsg  9675  frins2  9678  r1val1  9710  rankuni2b  9777  scottexs  9811  scott0s  9812  dfac8clem  9954  acni2  9968  aceq1  10039  dfac5lem5  10049  kmlem15  10087  infpssrlem4  10228  fin23lem27  10250  hsmexlem2  10349  hsmexlem4  10351  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6c4  10403  zorn2lem4  10421  zorn2lem5  10422  iunfo  10461  iundom2g  10462  uniimadomf  10467  konigthlem  10491  axrepndlem2  10516  axunnd  10519  axpowndlem2  10521  axpowndlem4  10523  axregndlem2  10526  axacndlem5  10534  zfcndrep  10537  zfcndinf  10541  pwfseqlem4a  10584  pwfseqlem4  10585  tskuni  10706  gruiin  10733  reclem2pr  10971  dedekind  11309  dedekindle  11310  fimaxre3  12102  nn0ind-raph  12629  uzind4s  12858  nnwof  12864  lbzbi  12886  fzrevral  13566  rabssnn0fi  13948  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiubex  13954  seqof2  14022  reuccatpfxs1  14709  cotr2g  14938  rlim2  15458  ello1mpt  15483  climeu  15517  o1compt  15549  summolem2a  15677  zsum  15680  sumss  15686  sumss2  15688  fsumcvg2  15689  fsumclf  15700  fsumsplitf  15704  fsumsplit1  15707  fsum2dlem  15732  fsum00  15761  o1fsum  15776  nfcprod1  15873  nfcprod  15874  prodmolem2a  15899  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  fprodn0  15944  fprod2dlem  15945  fprodsplitf  15953  fprodsplit1f  15955  fprodle  15961  fprodmodd  15962  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  coprmprod  16630  coprmproddvdslem  16631  prmind2  16654  iserodd  16806  pcmpt  16863  pcmptdvds  16865  prmolefac  17017  mreexexd  17614  catpropd  17675  invfuc  17944  natpropd  17946  fucpropd  17947  initoeu2  17983  acsmapd  18520  nfchnd  18577  symgval  19346  gsumsnd  19927  gsumsnf  19928  gsumunsnfd  19932  gsummptf1o  19938  gsummpt1n0  19940  gsum2d2lem  19948  gsumcom2  19950  gsummptnn0fz  19961  dprd2d2  20021  rngqiprngimf1  21298  gsummoncoe1  22273  gsumply1eq  22274  mdetralt2  22574  mdetunilem2  22578  madugsum  22608  gsummatr01lem4  22623  cpmatmcllem  22683  cayleyhamilton1  22857  neiptopnei  23097  neiptopreu  23098  neitr  23145  fiuncmp  23369  iunconnlem  23392  iunconn  23393  2ndcdisj  23421  dissnlocfin  23494  elptr2  23539  ptbasfi  23546  ptcld  23578  ptcldmpt  23579  ptclsg  23580  ptcnplem  23586  ptcnp  23587  cnmpt11  23628  cnmpt21  23636  cnmptcom  23643  imasnopn  23655  imasncld  23656  imasncls  23657  xkocnv  23779  elmptrab  23792  isfildlem  23822  alexsubALTlem3  24014  cnextfvval  24030  utopsnneiplem  24212  isucn2  24243  cfilucfil  24524  blval2  24527  restmetu  24535  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  finiunmbl  25511  volfiniun  25514  iundisj  25515  iunmbl  25520  voliun  25521  iunmbl2  25524  mbfeqalem1  25608  mbfsup  25631  mbfinf  25632  mbflim  25635  itg2splitlem  25715  itg2split  25716  isibl2  25733  cbvitg  25743  itgeqa  25781  itgss3  25782  itgfsum  25794  itgabs  25802  itggt0  25811  itgcn  25812  limcmpt  25850  limciun  25861  dvmptfsum  25942  dvlipcn  25961  dvfsumlem2  25994  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  itgsubst  26016  coeeq2  26207  dgrle  26208  ulmss  26362  leibpi  26906  rlimcnp  26929  rlimcnp2  26930  o1cxp  26938  lgamgulmlem2  26993  lgamgulmlem6  26997  fsumdvdscom  27148  lgseisenlem2  27339  2sqmo  27400  2sqreulem4  27417  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  bdayiun  27907  bdaypw2n0bndlem  28455  istrkg2ld  28528  mpteleeOLD  28964  gropd  29100  grstructd  29101  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  ex-natded9.26  30489  isch3  31312  atom1d  32424  chirred  32466  sbc2iedf  32534  rspc2daf  32535  19.9d2r  32539  opreu2reuALT  32546  mo5f  32558  reuxfrdf  32560  foresf1o  32574  elabreximdv  32581  iinabrex  32639  cbvdisjf  32641  disjorf  32649  disjabrex  32652  iundisjf  32659  disjunsn  32664  brabgaf  32679  ac6sf2  32695  dfimafnf  32709  2ndresdju  32722  fmptcof2  32730  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  aciunf1  32736  ofpreima  32738  funcnv5mpt  32740  funcnv4mpt  32741  fnpreimac  32743  f1od2  32792  fpwrelmap  32806  xrofsup  32840  iundisjfi  32869  nnindf  32893  nn0min  32894  fprodex01  32898  fsumiunle  32902  prodindf  32922  gsummpt2d  33110  gsummptf1od  33116  gsummptfsf1o  33121  gsumhashmul  33128  suppgsumssiun  33133  gsumwrd2dccat  33139  isarchiofld  33260  elrgspnsubrunlem2  33309  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem3  33475  nsgqusf1o  33476  elrspunidl  33488  elrspunsn  33489  deg1prod  33643  ply1gsumz  33659  ig1pmindeg  33662  mplvrpmga  33689  psrgsum  33692  psrmonprod  33696  esplylem  33710  esplyfv1  33713  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  vieta  33724  exsslsb  33741  ply1degltdimlem  33766  fedgmullem2  33774  evls1fldgencl  33814  irngnzply1  33835  extdgfialglem2  33837  ply1annidllem  33845  algextdeglem6  33866  constrfin  33890  reff  33983  locfinreflem  33984  cmpcref  33994  zarclsiin  34015  zarcls  34018  zarcmplem  34025  ordtconnlem1  34068  qqhval2  34126  esumeq12dva  34176  esumeq2dv  34182  esumrnmpt  34196  esumpad  34199  esumpad2  34200  esumadd  34201  gsumesum  34203  esumlub  34204  esumsnf  34208  esumpr  34210  esumrnmpt2  34212  esumfzf  34213  esumfsup  34214  esumpcvgval  34222  esumpmono  34223  esumcocn  34224  hasheuni  34229  esumcvg  34230  esumgect  34234  esum2dlem  34236  esum2d  34237  esumiun  34238  ldsysgenld  34304  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  fiunelros  34318  measvunilem  34356  measvunilem0  34357  measvuni  34358  measiun  34362  measinblem  34364  voliune  34373  volfiniune  34374  volmeas  34375  ddemeas  34380  oms0  34441  omssubadd  34444  carsgclctunlem1  34461  carsggect  34462  omsmeas  34467  eulerpartlemgvv  34520  dstrvprob  34616  ballotlemodife  34642  reprsuc  34759  reprdifc  34771  breprexplema  34774  breprexplemc  34776  circlemethhgt  34787  hgt750lemd  34792  bnj919  34910  bnj1146  34933  bnj1379  34972  bnj1385  34974  bnj1400  34977  bnj1534  34995  bnj1542  34999  bnj110  35000  bnj121  35012  bnj124  35013  bnj130  35016  bnj207  35023  bnj571  35048  bnj605  35049  bnj580  35055  bnj607  35058  bnj611  35060  bnj873  35066  bnj849  35067  bnj900  35071  bnj916  35075  bnj1000  35083  bnj964  35085  bnj981  35092  bnj985v  35095  bnj985  35096  bnj1014  35103  bnj1123  35128  bnj1128  35132  bnj1228  35153  bnj1204  35154  bnj1279  35160  bnj1307  35165  bnj1321  35169  bnj1388  35175  bnj1398  35176  bnj1408  35178  bnj1417  35183  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1449  35190  bnj1467  35196  bnj1489  35198  bnj1312  35200  bnj1497  35202  bnj1518  35206  bnj1525  35211  bnj1529  35212  dvelimalcased  35217  dvelimexcased  35219  axsepg2  35225  axsepg2ALT  35226  fineqvrep  35258  onvf1odlem2  35286  cvmcov  35445  untsucf  35892  dfon2lem1  35963  dfon2lem3  35965  finminlem  36500  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  axtcond  36660  regsfromregtco  36720  regsfromsetind  36721  bj-nexdvt  36995  bj-cbvaldv  37106  bj-cbval2vv  37108  bj-cbvex2vv  37109  bj-cbvaldvav  37110  bj-cbvexdvav  37111  ax11-pm2  37143  bj-dvelimdv  37158  bj-nfeel2  37161  bj-ceqsalv  37201  bj-vtocl  37223  bj-inrab2  37235  currysetlem  37252  currysetlem1  37254  bj-axseprep  37381  bj-axreprepsep  37382  bj-opabco  37502  mptsnunlem  37654  exlimim  37658  exellim  37660  topdifinfindis  37662  topdifinffinlem  37663  icorempo  37667  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  finxpreclem2  37706  finxpreclem6  37712  fvineqsneu  37727  fvineqsneq  37728  wl-euequf  37899  wl-sb8eut  37903  wl-issetft  37907  phpreu  37925  matunitlindflem2  37938  ptrest  37940  ptrecube  37941  poimirlem2  37943  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  heicant  37976  mbfposadd  37988  itgabsnc  38010  itggt0cn  38011  ftc1anclem5  38018  upixp  38050  indexa  38054  indexdom  38055  filbcmb  38061  sdclem2  38063  sdclem1  38064  fdc1  38067  totbndbnd  38110  sbcalf  38435  sbcexf  38436  scottexf  38489  scott0f  38490  eqrelf  38579  ralrmo3  38685  disjqmap2  39147  fsumshftd  39398  riotasv2d  39403  riotasv2s  39404  riotasv3d  39406  glbconxN  39824  pmapglbx  40215  pmapglb2xN  40218  cdleme26ee  40806  cdleme31sn  40826  cdleme31sn1  40827  cdlemefr29exN  40848  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32fva  40883  cdleme32d  40890  cdleme32f  40892  cdleme40m  40913  cdleme40n  40914  cdleme42b  40924  cdlemk36  41359  cdlemk38  41361  cdlemkid  41382  cdlemk19x  41389  cdlemk11t  41392  dihvalcqpre  41681  mapdheq  42174  hdmap1eq  42247  hdmapval2lem  42277  lcmineqlem9  42476  lcmineqlem12  42479  aks4d1p1p2  42509  mndmolinv  42534  primrootsunit1  42536  primrootsunit  42537  primrootspoweq0  42545  aks6d1c1p5  42551  aks6d1c3  42562  aks6d1c4  42563  aks6d1c1rh  42564  aks6d1c2lem4  42566  aks6d1c2  42569  deg1gprod  42579  sticksstones1  42585  sticksstones11  42595  sticksstones16  42601  sticksstones22  42607  aks6d1c6lem2  42610  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  bcled  42617  bcle2d  42618  aks6d1c7lem3  42621  aks6d1c7  42623  rhmqusspan  42624  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  unitscyglem5  42638  nfa1w  43108  mzpexpmpt  43177  eq0rabdioph  43208  rexrabdioph  43222  rexfrabdioph  43223  elnn0rabdioph  43231  dvdsrabdioph  43238  fphpd  43244  monotuz  43369  monotoddzz  43371  oddcomabszz  43372  setindtr  43452  dford4  43457  wdom2d2  43463  aomclem6  43487  aomclem8  43489  flcidc  43598  areaquad  43644  unielss  43646  onsucf1lem  43697  oaun3lem1  43802  nadd1suc  43820  rababg  44001  ss2iundv  44087  cbviuneq12dv  44089  gneispace  44561  mnringvald  44640  mnringmulrcld  44655  nfscott  44666  scottabf  44667  scottab  44668  mnuprdlem4  44702  ismnushort  44728  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  aaanv  44815  pm11.57  44816  pm11.58  44817  pm11.59  44818  pm11.71  44824  pm14.12  44848  ssralv2  44958  tratrb  44963  iunconnlem2  45361  modelaxreplem3  45407  modelaxrep  45408  permaxrep  45433  evth2f  45446  elunif  45447  fvelrnbf  45449  evthf  45458  fnchoice  45460  sumpair  45466  rfcnnnub  45467  refsum2cn  45469  uzwo4  45484  fiiuncl  45496  fiunicl  45498  elintdv  45510  ssd  45511  cbvmpo2  45527  cbvmpo1  45528  eliin2f  45534  eliuniin2  45550  cbvrabv2  45557  suprnmpt  45604  disjf1  45613  disjrnmpt2  45618  disjf1o  45621  disjinfi  45622  choicefi  45629  iunmapsn  45646  axccdom  45651  dmrelrnrel  45655  axccd  45658  fmptf  45668  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  rnmptbdlem  45684  rnmptbd  45685  fmptff  45698  upbdrech  45738  ssfiunibd  45742  supxrgere  45763  iuneqfzuzlem  45764  supxrgelem  45767  supxrge  45768  suplesup  45769  infrpge  45781  xralrple2  45784  infxr  45796  infxrunb2  45797  infleinf  45801  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  supxrleubrnmpt  45834  infleinf2  45842  unb2ltle  45843  rexabslelem  45846  rexabsle  45847  allbutfiinf  45848  suprleubrnmpt  45850  infrnmptle  45851  infxrunb3rnmpt  45856  uzublem  45858  uzub  45859  supminfrnmpt  45873  infxrpnf  45874  supxrleubrnmptf  45879  infxrgelbrnmpt  45882  infrpgernmpt  45893  supminfxr2  45897  monoordxr  45910  monoord2xr  45912  caucvgbf  45917  cvgcaule  45919  rexanuz2nf  45920  iccshift  45948  iooshift  45952  iooiinicc  45972  iooiinioc  45986  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fmul01lt1  46016  fprodsplit1  46023  fprodexp  46024  fprodabs2  46025  mccllem  46027  mccl  46028  fprodcnlem  46029  fprodcn  46030  climexp  46035  climsuse  46038  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  ellimcabssub0  46047  islptre  46049  climf  46052  mullimcf  46053  rexlim2d  46055  idlimc  46056  limcperiod  46058  limcrecl  46059  sumnnodd  46060  islpcn  46067  limsupre  46069  limcleqr  46072  neglimc  46075  addlimc  46076  0ellimcdiv  46077  limclner  46079  climsubmpt  46088  climreclf  46092  climf2  46094  fnlimcnv  46095  climeldmeqmpt  46096  clim2f2  46098  climfveqmpt  46099  fnlimfvre  46102  allbutfifvre  46103  climleltrp  46104  fnlimf  46106  fnlimabslt  46107  climfveqmpt3  46110  climeldmeqf  46111  limsupref  46113  limsupbnd1f  46114  climbddf  46115  climeqf  46116  climeldmeqmpt3  46117  limsuplesup  46127  limsuppnfd  46130  limsupub  46132  limsupres  46133  climinf2lem  46134  climinf2  46135  limsuppnf  46139  limsupubuzlem  46140  limsupubuz  46141  climinf2mpt  46142  climinfmpt  46143  climinf3  46144  limsupmnflem  46148  limsupmnf  46149  limsupequz  46151  limsupre2  46153  limsupmnfuzlem  46154  limsupmnfuz  46155  limsupequzmptf  46159  limsupre3lem  46160  limsupre3  46161  limsupre3uzlem  46163  limsupre3uz  46164  limsupreuz  46165  limsupvaluz2  46166  limsupreuzmpt  46167  supcnvlimsup  46168  climuzlem  46171  climuz  46172  climisp  46174  lmbr3  46175  climrescn  46176  climxrrelem  46177  climxrre  46178  liminfcl  46191  liminfval2  46196  limsup10exlem  46200  liminflelimsuplem  46203  limsupgtlem  46205  limsupgt  46206  climliminflimsupd  46229  liminfreuzlem  46230  liminfreuz  46231  liminfltlem  46232  liminflt  46233  limsupub2  46240  xlimpnfxnegmnf  46242  liminflbuz2  46243  liminfpnfuz  46244  liminflimsupxrre  46245  xlimmnfvlem1  46260  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem1  46264  xlimpnfvlem2  46265  xlimpnfv  46266  xlimmnf  46269  xlimpnf  46270  xlimmnfmpt  46271  xlimpnfmpt  46272  climxlim2lem  46273  dfxlim2  46276  cncfshift  46302  icccncfext  46315  cncficcgt0  46316  cncfiooicc  46322  cncfioobd  46325  fprodcncf  46328  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvmptmulf  46365  dvnmptdivc  46366  dvnmul  46371  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  iblsplitf  46398  iblspltprt  46401  itgioocnicc  46405  iblcncfioo  46406  itgspltprt  46407  itgperiod  46409  stoweidlem3  46431  stoweidlem14  46442  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem26  46454  stoweidlem27  46455  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem36  46464  stoweidlem39  46467  stoweidlem42  46470  stoweidlem43  46471  stoweidlem44  46472  stoweidlem46  46474  stoweidlem48  46476  stoweidlem49  46477  stoweidlem50  46478  stoweidlem51  46479  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem56  46484  stoweidlem57  46485  stoweidlem59  46487  stoweidlem60  46488  stoweidlem61  46489  stoweidlem62  46490  stoweid  46491  wallispilem3  46495  stirlinglem13  46514  stirling  46517  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem31  46566  fourierdlem39  46574  fourierdlem48  46582  fourierdlem51  46585  fourierdlem53  46587  fourierdlem68  46602  fourierdlem69  46603  fourierdlem71  46605  fourierdlem73  46607  fourierdlem77  46611  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem86  46620  fourierdlem87  46621  fourierdlem89  46623  fourierdlem91  46625  fourierdlem93  46627  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  elaa2  46662  etransclem18  46680  etransclem22  46684  etransclem23  46685  etransclem32  46694  etransclem35  46697  etransclem44  46706  etransclem46  46708  etransclem48  46710  rrndistlt  46718  ioorrnopnlem  46732  saliuncl  46751  saliincl  46755  intsaluni  46757  salexct  46762  subsaliuncl  46786  sge00  46804  sge0revalmpt  46806  sge0sn  46807  sge0f1o  46810  sge0gerp  46823  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resrnlem  46831  sge0resplit  46834  sge0lempt  46838  sge0iunmptlemfi  46841  sge0p1  46842  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0rpcpnf  46849  sge0ltfirpmpt2  46854  sge0isum  46855  sge0xp  46857  sge0ad2en  46859  sge0isummpt2  46860  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0xadd  46863  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  sge0reuzb  46876  iundjiun  46888  meadjiunlem  46893  meadjiun  46894  ismeannd  46895  voliunsge0lem  46900  meaiuninclem  46908  meaiunincf  46911  meaiuninc3v  46912  meaiuninc3  46913  meaiininclem  46914  meaiininc  46915  meaiininc2  46916  caragenfiiuncl  46943  omeiunltfirp  46947  carageniuncllem1  46949  carageniuncllem2  46950  caratheodorylem2  46955  0ome  46957  isomenndlem  46958  hoicvrrex  46984  ovnsupge0  46985  ovnlecvr  46986  ovnlerp  46990  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubaddlem2  46999  hoidmvcl  47010  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmvval0  47015  sge0hsphoire  47017  hoidmvval0b  47018  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem1  47029  ovnhoilem2  47030  ovnhoi  47031  ovnlecvr2  47038  hspdifhsp  47044  hoidifhspdmvle  47048  hoiqssbllem3  47052  hspmbllem1  47054  hspmbllem2  47055  opnvonmbllem1  47060  opnvonmbllem2  47061  ovnsubadd2lem  47073  ovolval5lem1  47080  ovnovollem1  47084  ovnovollem2  47085  hoimbl2  47093  vonhoire  47100  iinhoiicclem  47101  iinhoiicc  47102  iunhoiioolem  47103  iunhoiioo  47104  vonioolem1  47108  vonioolem2  47109  vonioo  47110  vonicclem1  47111  vonicclem2  47112  vonicc  47113  vonn0ioo2  47118  vonn0icc2  47120  vonct  47121  pimltmnf2f  47125  pimgtpnf2f  47133  salpreimagelt  47135  salpreimalegt  47137  pimltpnf2f  47140  pimgtmnf2  47142  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  salpreimagtge  47153  salpreimaltle  47154  salpreimalelt  47157  salpreimagtlt  47158  issmff  47162  sssmf  47166  mbfresmf  47167  cnfsmf  47168  incsmflem  47169  incsmf  47170  smfsssmf  47171  issmflelem  47172  issmfle  47173  smfconst  47177  issmfgtlem  47183  issmfgt  47184  smfpimltxrmptf  47186  smfmbfcex  47188  smfaddlem1  47191  smfaddlem2  47192  smfadd  47193  decsmflem  47194  decsmf  47195  smfpreimagtf  47196  issmfgelem  47197  issmfge  47198  smflimlem2  47200  smflimlem4  47202  smflim  47205  smfpimgtxr  47208  smfpimgtxrmptf  47212  smfpimioo  47215  smfresal  47216  smfrec  47217  smfres  47218  smfmullem2  47220  smfmullem4  47222  smfmul  47223  smfpimbor1lem2  47227  smf2id  47229  smfco  47230  smflim2  47234  smfpimcc  47236  smflimmpt  47238  smfsuplem1  47239  smfsuplem3  47241  smfsup  47242  smfsupmpt  47243  smfsupxr  47244  smfinflem  47245  smfinf  47246  smfinfmpt  47247  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  smflimsuplem8  47255  smflimsup  47256  smflimsupmpt  47257  smfliminflem  47258  smfliminf  47259  smfliminfmpt  47260  smfpimne2  47268  fsupdm  47270  smfsupdmmbllem  47272  smfsupdmmbl  47273  finfdm  47274  smfinfdmmbllem  47276  smfinfdmmbl  47277  or2expropbilem1  47480  or2expropbilem2  47481  or2expropbi  47482  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  rexsb  47547  reuf1odnf  47555  2reu8i  47561  ffnafv  47619  tz6.12c-afv2  47690  f1oresf1o2  47739  iccelpart  47893  iccpartdisj  47897  dfich2  47918  ichbi12i  47920  ichnfimlem  47923  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  sprsymrelfo  47957  reupr  47982  reuopreuprim  47986  mogoldbb  48261  2zrngagrp  48725  2zrngmmgm  48728  cbvmpox2  48812  ovmpordx  48816  1arymaptfo  49119  2arymaptfo  49130  mo0sn  49291  iinfssclem3  49531  iinfssc  49532  iinfsubc  49533  infsubc2  49536  iinfconstbas  49541  isthincd2lem1  49900  nfintd  50148  nfiund  50149  nfiundg  50150  iunord  50151  spcdvw  50154  nfsetrecs  50161  setrec1lem2  50163  setrec1  50166  setrec2fun  50167  pgindnf  50191  pgind  50192  aacllem  50276