Theorem nfv 1941

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

Syntax hints:  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfvd  1942  cbvaldw  2376  cbval2v  2381  dvelimhw  2383  pm11.53  2384  19.12vv  2385  eeanv  2387  eeeanv  2388  ee4anv  2389  sbnf2  2396  exsb  2397  2exsb  2398  sbbibvv  2400  cbvsbvf  2401  cleljustALT2  2403  spimv  2428  spimev  2430  chvarv  2434  cbvalv  2438  cbvexv  2439  cbvald  2445  cbvaldva  2447  cbvexdva  2448  cbval2  2449  axc16i  2474  dvelimnf  2491  sbel2x  2512  sbiedv  2542  2sbiev  2543  sbid2v  2547  sbhb  2559  2sb8e  2568  nfmod2  2592  nfmodv  2593  mof  2597  mo4f  2601  euf  2610  sb8eulem  2632  cbvmow  2637  sbmo  2648  moexexvw  2662  moexexv  2673  2mo  2682  2eu6  2690  axextmo  2745  nulmo  2746  abbib  2838  cleqh  2898  nfcv  2931  nfeqd  2941  nfeld  2942  nfabdw  2952  nfabd  2953  dvelimdc  2955  nfcvf  2957  cleqf  2959  r19.29af  3280  rexbidvALT  3286  rexbidvaALT  3287  2ralbida  3294  r19.12  3320  reean  3321  cbvrexsvw  3323  cbvralsvwOLD  3324  sbralieOLD  3351  cbvralf  3356  cbvralv  3360  cbvrexv  3361  cbvralsv  3362  cbvrexsv  3363  cbvrmow  3401  cbvreu  3415  cbvrmov  3417  cbvreuv  3418  cbvrabwOLD  3459  cbvrab  3462  cbvexeqsetf  3478  ceqsex2  3513  vtocl2gaf  3552  vtocl3gaf  3553  spc2ed  3569  rspct  3576  rspc  3578  rspce  3579  eqvincf  3618  elrab3t  3658  ralab2  3669  rexab2  3671  mob2  3687  mob  3689  reu2  3697  rmo4f  3707  reu2eqd  3708  cdeqab1  3744  nfcdeq  3749  sbcco  3779  cbvsbcv  3789  elrabsf  3798  sbc2iegf  3827  reu8nf  3839  rmo2  3849  rmo3  3851  rmoanimALT  3857  nfcsb1d  3883  nfcsbd  3886  csbiebt  3890  csbie2t  3899  cbvrabcsfw  3902  cbvralcsf  3903  cbvreucsf  3905  cbvrabcsf  3906  cbvralv2  3907  cbvrexv2  3908  rspc2vd  3909  dfssf  3936  rabss3d  4043  eqrrabd  4048  uniiunlem  4049  ab0orv  4346  ab0orvALT  4347  sbcnestgw  4394  sbcnestg  4399  sbnfc2  4410  r19.3rzvOLD  4470  r19.28zv  4472  r19.27zv  4477  2reu4lem  4489  nfifd  4522  reusngf  4645  reusng  4648  rexreusng  4650  reuprg0  4673  rabsnifsb  4693  euabsn  4697  nfunid  4882  eluniab  4890  nfint  4926  iuneqconst  4972  disjiun  5101  disjxun  5111  nfopabd  5183  cbvopab  5187  cbvopab1  5189  cbvopab1g  5190  cbvopab2  5191  cbvopab1s  5192  mpteq12da  5198  mpteq12f  5200  cbvmptf  5215  cbvmptfg  5216  axrep1  5243  axrep2  5245  axrep3  5246  axrep4OLD  5249  axrep5  5250  zfrepclf  5256  reusv2lem3  5374  reusv2lem4  5375  reusv2  5377  reusv3  5379  alxfr  5381  ralxfrALT  5389  axprlem3OLD  5403  axprlem4OLD  5404  axprlem5OLD  5405  copsex2t  5478  iunopeqop  5507  iunopeqopOLD  5508  rexopabb  5515  opelopabaf  5532  nfso  5579  pofun  5590  isso2i  5609  nffr  5637  opeliunxp  5731  opeliun2xp  5732  opeliunxp2  5827  ralxpf  5835  dfdmf  5889  dfrnf  5943  elrnmpt1  5953  dfrel4  6192  reuop  6297  frpoinsg  6347  frpoins2g  6349  wfis2g  6359  nfiotadw  6498  nfiotad  6500  cbviotaw  6502  cbviota  6504  cbviotav  6505  sb8iota  6506  iota2d  6527  iota2  6528  dffun6f  6554  imadif  6623  isarep1  6627  isarep2  6628  fv3  6902  tz6.12f  6909  funimassd  6950  fvelimad  6951  feqmptdf  6954  fimarab  6958  opabiotafun  6964  funfv2f  6973  fvmptd  7000  fvmptd2f  7009  fvmptdv  7010  fvmptt  7013  fvopab5  7026  eqfnfv2f  7032  ralrnmptw  7092  ralrnmpt  7094  dffo3f  7104  f1ompt  7109  fompt  7116  ffnfv  7117  ffnfvf  7118  f1ossf1o  7127  fmptco  7128  elabrex  7243  elabrexg  7244  dff13f  7256  fsnex  7284  fliftfun  7313  cbvriotaw  7379  cbvriota  7383  cbvriotav  7384  riota2  7395  riotaeqimp  7396  riota5f  7398  oprabv  7473  nfoprab  7477  mpoeq123  7485  cbvoprab1  7500  cbvoprab2  7501  cbvoprab12  7502  cbvoprab3  7504  cbvmpox  7506  ralrnmpo  7552  ovmpodx  7564  ovmpodf  7569  ovmpodv  7570  ov3  7576  ovmpt3rab1  7671  ofrfval2  7698  onminex  7803  tfis  7853  tfis2  7855  tfisi  7857  tfinds  7858  tfindes  7861  findes  7899  fiun  7942  f1iun  7943  abrexex2g  7963  opabex3d  7964  opabex3rd  7965  opabex3  7966  dfoprab4f  8055  fmpox  8066  offval22  8085  ovmptss  8090  ralxpes  8134  ralxp3  8136  ralxp3es  8137  frpoins3xpg  8138  frpoins3xp3g  8139  opeliunxp2f  8208  tposoprab  8260  fvmpocurryd  8269  nffrecs  8282  tfr3  8388  nfrdg  8403  tz7.48-1  8432  tz7.49  8434  naddsuc2  8690  eqerlem  8732  erovlem  8813  mptelixpg  8935  boxcutc  8941  dom2lem  8991  xpf1o  9129  mapxpen  9133  findcard2  9151  pssnn  9155  nneneq  9192  ac6sfi  9246  fiint  9288  indexfi  9319  wdom2d  9544  ixpiunwdom  9554  cantnflem1  9660  nfttrcld  9681  setinds2  9722  frinsg  9725  frins2  9728  r1val1  9760  rankuni2b  9827  scottexs  9863  scott0s  9864  nfscott  9867  scottabf  9868  scottab  9869  dfac8clem  10018  acni2  10032  aceq1  10103  dfac5lem5  10113  kmlem15  10150  infpssrlem4  10292  fin23lem27  10314  hsmexlem2  10413  hsmexlem4  10415  axcc3  10424  domtriomlem  10428  axdc3lem2  10437  axdc3lem4  10439  axdc4lem  10441  ac6c4  10467  zorn2lem4  10485  zorn2lem5  10486  iunfo  10525  iundom2g  10526  uniimadomf  10531  konigthlem  10555  axrepndlem2  10580  axunnd  10583  axpowndlem2  10585  axpowndlem4  10587  axregndlem2  10590  axacndlem5  10598  zfcndrep  10601  zfcndinf  10605  pwfseqlem4a  10648  pwfseqlem4  10649  tskuni  10770  gruiin  10797  reclem2pr  11035  dedekind  11375  dedekindle  11376  fimaxre3  12163  nn0ind-raph  12698  uzind4s  12934  nnwof  12940  lbzbi  12962  fzrevral  13642  rabssnn0fi  14024  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fsuppmapnn0fiubex  14030  seqof2  14098  reuccatpfxs1  14786  cotr2g  15015  rlim2  15549  ello1mpt  15574  climeu  15608  o1compt  15640  summolem2a  15768  zsum  15771  sumss  15777  sumss2  15779  fsumcvg2  15780  fsumclf  15791  fsumsplitf  15795  fsumsplit1  15798  fsum2dlem  15823  fsum00  15852  o1fsum  15867  nfcprod1  15964  nfcprod  15965  prodmolem2a  15990  zprod  15993  fprod  15997  fprodntriv  15998  prodss  16003  fprodn0  16035  fprod2dlem  16036  fprodsplitf  16044  fprodsplit1f  16046  fprodle  16052  fprodmodd  16053  lcmfunsnlem1  16697  lcmfunsnlem2lem1  16698  lcmfunsnlem2  16700  coprmprod  16721  coprmproddvdslem  16722  prmind2  16745  iserodd  16897  pcmpt  16954  pcmptdvds  16956  prmolefac  17108  mreexexd  17706  catpropd  17767  invfuc  18036  natpropd  18038  fucpropd  18039  initoeu2  18075  acsmapd  18612  nfchnd  18669  symgval  19443  gsumsnd  20024  gsumsnf  20025  gsumunsnfd  20029  gsummptf1o  20035  gsummpt1n0  20037  gsum2d2lem  20045  gsumcom2  20047  gsummptnn0fz  20058  dprd2d2  20118  rngqiprngimf1  21413  gsummoncoe1  22439  gsumply1eq  22440  mdetralt2  22737  mdetunilem2  22741  madugsum  22771  gsummatr01lem4  22786  cpmatmcllem  22846  cayleyhamilton1  23020  neiptopnei  23260  neiptopreu  23261  neitr  23308  fiuncmp  23532  iunconnlem  23555  iunconn  23556  2ndcdisj  23584  dissnlocfin  23657  elptr2  23702  ptbasfi  23709  ptcld  23741  ptcldmpt  23742  ptclsg  23743  ptcnplem  23749  ptcnp  23750  cnmpt11  23791  cnmpt21  23799  cnmptcom  23806  imasnopn  23818  imasncld  23819  imasncls  23820  xkocnv  23942  elmptrab  23955  isfildlem  23985  alexsubALTlem3  24177  cnextfvval  24193  utopsnneiplem  24375  isucn2  24406  cfilucfil  24687  blval2  24690  restmetu  24698  ovoliunlem3  25634  ovoliun  25635  ovoliun2  25636  ovoliunnul  25637  finiunmbl  25674  volfiniun  25677  iundisj  25678  iunmbl  25683  voliun  25684  iunmbl2  25687  mbfeqalem1  25771  mbfsup  25794  mbfinf  25795  mbflim  25798  itg2splitlem  25878  itg2split  25879  isibl2  25896  cbvitg  25906  itgeqa  25944  itgss3  25945  itgfsum  25957  itgabs  25965  itggt0  25974  itgcn  25975  limcmpt  26013  limciun  26024  dvmptfsum  26105  dvlipcn  26124  dvfsumlem2  26157  dvfsumlem4  26159  dvfsumrlim  26161  dvfsum2  26164  itgsubst  26179  coeeq2  26370  dgrle  26371  ulmss  26528  leibpi  27075  rlimcnp  27098  rlimcnp2  27099  o1cxp  27107  lgamgulmlem2  27162  lgamgulmlem6  27166  fsumdvdscom  27317  lgseisenlem2  27508  2sqmo  27569  2sqreulem4  27586  dchrisumlema  27620  dchrisumlem2  27622  dchrisumlem3  27623  nosupbnd1  27846  nosupbnd2  27848  noinfbnd1  27861  noinfbnd2  27863  bdayiun  28076  bdaypw2n0bndlem  28624  istrkg2ld  28697  mpteleeOLD  29188  gropd  29324  grstructd  29325  clwwlknonclwlknonf1o  30656  dlwwlknondlwlknonf1o  30659  ex-natded9.26  30713  isch3  31536  atom1d  32648  chirred  32690  sbc2iedf  32755  rspc2daf  32756  19.9d2r  32760  opreu2reuALT  32766  mo5f  32778  reuxfrdf  32780  foresf1o  32793  elabreximdv  32800  iinabrex  32857  cbvdisjf  32859  disjorf  32867  disjabrex  32870  iundisjf  32877  disjunsn  32882  brabgaf  32894  ac6sf2  32910  dfimafnf  32924  2ndresdju  32937  fmptcof2  32945  acunirnmpt2  32948  acunirnmpt2f  32949  aciunf1lem  32950  aciunf1  32951  ofpreima  32953  funcnv5mpt  32955  funcnv4mpt  32956  fnpreimac  32958  f1od2  33007  fpwrelmap  33021  xrofsup  33055  iundisjfi  33084  nnindf  33107  nn0min  33108  fprodex01  33112  fsumiunle  33116  prodindf  33125  gsummpt2d  33312  gsummptf1od  33318  gsummptfsf1o  33323  gsumhashmul  33330  suppgsumssiun  33335  gsumwrd2dccat  33341  isarchiofld  33462  elrgspnsubrunlem2  33511  nsgmgc  33667  nsgqusf1olem1  33668  nsgqusf1olem3  33670  nsgqusf1o  33671  elrspunidl  33682  elrspunsn  33683  deg1prod  33820  ply1gsumz  33836  ig1pmindeg  33839  mplvrpmga  33882  psrgsum  33885  psrmonprod  33889  esplylem  33903  esplyfv1  33906  esplyfval1  33910  esplyfvaln  33911  esplyind  33912  vieta  33917  exsslsb  33934  ply1degltdimlem  33959  fedgmullem2  33967  evls1fldgencl  34007  irngnzply1  34028  extdgfialglem2  34030  ply1annidllem  34038  algextdeglem6  34059  constrfin  34083  reff  34176  locfinreflem  34177  cmpcref  34187  zarclsiin  34208  zarcls  34211  zarcmplem  34218  ordtconnlem1  34261  qqhval2  34319  esumeq12dva  34369  esumeq2dv  34375  esumrnmpt  34389  esumpad  34392  esumpad2  34393  esumadd  34394  gsumesum  34396  esumlub  34397  esumsnf  34401  esumpr  34403  esumrnmpt2  34405  esumfzf  34406  esumfsup  34407  esumpcvgval  34415  esumpmono  34416  esumcocn  34417  hasheuni  34422  esumcvg  34423  esumgect  34427  esum2dlem  34429  esum2d  34430  esumiun  34431  ldsysgenld  34497  sigapildsyslem  34498  sigapildsys  34499  ldgenpisyslem1  34500  fiunelros  34511  measvunilem  34549  measvunilem0  34550  measvuni  34551  measiun  34555  measinblem  34557  voliune  34566  volfiniune  34567  volmeas  34568  ddemeas  34573  oms0  34634  omssubadd  34637  carsgclctunlem1  34654  carsggect  34655  omsmeas  34660  eulerpartlemgvv  34713  dstrvprob  34809  ballotlemodife  34835  reprsuc  34949  reprdifc  34961  breprexplema  34964  breprexplemc  34966  circlemethhgt  34977  hgt750lemd  34982  bnj919  35103  bnj1146  35126  bnj1379  35165  bnj1385  35167  bnj1400  35170  bnj1534  35188  bnj1542  35192  bnj110  35193  bnj121  35205  bnj124  35206  bnj130  35209  bnj207  35216  bnj571  35241  bnj605  35242  bnj580  35248  bnj607  35251  bnj611  35253  bnj873  35259  bnj849  35260  bnj900  35264  bnj916  35268  bnj1000  35276  bnj964  35278  bnj981  35285  bnj985v  35288  bnj985  35289  bnj1014  35296  bnj1123  35321  bnj1128  35325  bnj1228  35346  bnj1204  35347  bnj1279  35353  bnj1307  35358  bnj1321  35362  bnj1388  35368  bnj1398  35369  bnj1408  35371  bnj1417  35376  bnj1444  35378  bnj1445  35379  bnj1446  35380  bnj1449  35383  bnj1467  35389  bnj1489  35391  bnj1312  35393  bnj1497  35395  bnj1518  35399  bnj1525  35404  bnj1529  35405  dvelimalcased  35410  dvelimexcased  35412  fineqvrep  35462  axsepg2  35488  axsepg3  35489  axsepg3ALT  35490  axpowg2  35495  axpowg3  35496  onvf1odlem2  35523  cvmcov  35690  untsucf  36137  dfon2lem1  36208  dfon2lem3  36210  finminlem  36754  weiunpo  36901  weiunso  36902  weiunfr  36903  weiunse  36904  axtcond  36914  regsfromregtco  36974  regsfromsetind  36975  bj-nexdvt  37248  bj-cbvaldv  37359  bj-cbval2vv  37361  bj-cbvex2vv  37362  bj-cbvaldvav  37363  bj-cbvexdvav  37364  ax11-pm2  37396  bj-dvelimdv  37411  bj-nfeel2  37414  bj-ceqsalv  37454  bj-vtocl  37476  bj-inrab2  37489  currysetlem  37506  currysetlem1  37508  bj-axseprep  37636  bj-axreprepsep  37637  bj-opabco  37757  mptsnunlem  37909  exlimim  37913  exellim  37915  topdifinfindis  37917  topdifinffinlem  37918  icorempo  37922  isbasisrelowllem1  37926  isbasisrelowllem2  37927  relowlssretop  37934  finxpreclem2  37961  finxpreclem6  37967  fvineqsneu  37982  fvineqsneq  37983  wl-euequf  38154  wl-sb8eut  38158  wl-issetft  38162  phpreu  38180  matunitlindflem2  38193  ptrest  38195  ptrecube  38196  poimirlem2  38198  poimirlem23  38219  poimirlem24  38220  poimirlem25  38221  poimirlem26  38222  poimirlem27  38223  poimirlem28  38224  heicant  38231  mbfposadd  38243  itgabsnc  38265  itggt0cn  38266  ftc1anclem5  38273  upixp  38305  indexa  38309  indexdom  38310  filbcmb  38316  sdclem2  38318  sdclem1  38319  fdc1  38322  totbndbnd  38365  sbcalf  38690  sbcexf  38691  scottexf  38744  scott0f  38745  eqrelf  38834  ralrmo3  38940  disjqmap2  39402  fsumshftd  39653  riotasv2d  39658  riotasv2s  39659  riotasv3d  39661  glbconxN  40079  pmapglbx  40470  pmapglb2xN  40473  cdleme26ee  41061  cdleme31sn  41081  cdleme31sn1  41082  cdlemefr29exN  41103  cdlemefs32sn1aw  41115  cdleme43fsv1snlem  41121  cdleme41sn3a  41134  cdleme32fva  41138  cdleme32d  41145  cdleme32f  41147  cdleme40m  41168  cdleme40n  41169  cdleme42b  41179  cdlemk36  41614  cdlemk38  41616  cdlemkid  41637  cdlemk19x  41644  cdlemk11t  41647  dihvalcqpre  41936  mapdheq  42429  hdmap1eq  42502  hdmapval2lem  42532  lcmineqlem9  42731  lcmineqlem12  42734  aks4d1p1p2  42764  mndmolinv  42789  primrootsunit1  42791  primrootsunit  42792  primrootspoweq0  42800  aks6d1c1p5  42806  aks6d1c3  42817  aks6d1c4  42818  aks6d1c1rh  42819  aks6d1c2lem4  42821  aks6d1c2  42824  deg1gprod  42834  sticksstones1  42840  sticksstones11  42850  sticksstones16  42856  sticksstones22  42862  aks6d1c6lem2  42865  aks6d1c6isolem1  42868  aks6d1c6isolem2  42869  bcled  42872  bcle2d  42873  aks6d1c7lem3  42876  aks6d1c7  42878  rhmqusspan  42879  grpods  42888  unitscyglem1  42889  unitscyglem2  42890  unitscyglem3  42891  unitscyglem4  42892  unitscyglem5  42893  nfa1w  43336  mzpexpmpt  43405  eq0rabdioph  43436  rexrabdioph  43450  rexfrabdioph  43451  elnn0rabdioph  43459  dvdsrabdioph  43466  fphpd  43472  monotuz  43597  monotoddzz  43599  oddcomabszz  43600  setindtr  43680  dford4  43685  wdom2d2  43691  aomclem6  43715  aomclem8  43717  flcidc  43826  areaquad  43872  unielss  43874  onsucf1lem  43925  oaun3lem1  44030  nadd1suc  44048  rababg  44229  ss2iundv  44315  cbviuneq12dv  44317  gneispace  44789  mnringvald  44866  mnringmulrcld  44881  mnuprdlem4  44914  ismnushort  44940  binomcxplemdvsum  44994  binomcxplemnotnn0  44995  aaanv  45027  pm11.57  45028  pm11.58  45029  pm11.59  45030  pm11.71  45036  pm14.12  45060  ssralv2  45169  tratrb  45174  iunconnlem2  45572  modelaxreplem3  45618  modelaxrep  45619  permaxrep  45644  evth2f  45664  elunif  45665  fvelrnbf  45667  evthf  45676  fnchoice  45678  sumpair  45684  rfcnnnub  45685  refsum2cn  45687  uzwo4  45702  fiiuncl  45714  fiunicl  45716  elintdv  45728  ssd  45729  cbvmpo2  45744  cbvmpo1  45745  eliin2f  45751  eliuniin2  45767  cbvrabv2  45774  suprnmpt  45821  disjf1  45830  disjrnmpt2  45835  disjf1o  45838  disjinfi  45839  choicefi  45846  iunmapsn  45862  axccdom  45867  dmrelrnrel  45871  axccd  45873  fmptf  45883  rnmptlb  45887  rnmptbddlem  45888  rnmptbd2lem  45892  rnmptbdlem  45899  rnmptbd  45900  fmptff  45913  upbdrech  45953  ssfiunibd  45957  supxrgere  45978  iuneqfzuzlem  45979  supxrgelem  45982  supxrge  45983  suplesup  45984  infrpge  45996  xralrple2  45999  infxr  46011  infxrunb2  46012  infleinf  46016  xrralrecnnle  46027  xrralrecnnge  46034  supxrunb3  46043  supxrleubrnmpt  46049  infleinf2  46057  unb2ltle  46058  rexabslelem  46061  rexabsle  46062  allbutfiinf  46063  suprleubrnmpt  46065  infrnmptle  46066  infxrunb3rnmpt  46071  uzublem  46073  uzub  46074  supminfrnmpt  46088  infxrpnf  46089  supxrleubrnmptf  46094  infxrgelbrnmpt  46097  infrpgernmpt  46108  supminfxr2  46112  monoordxr  46125  monoord2xr  46127  caucvgbf  46132  cvgcaule  46134  rexanuz2nf  46135  iccshift  46163  iooshift  46167  iooiinicc  46187  iooiinioc  46201  fsummulc1f  46216  fsumnncl  46217  fsumf1of  46219  fsumiunss  46220  fsumreclf  46221  fsumlessf  46222  fsumsermpt  46224  fmul01  46225  fmuldfeqlem1  46227  fmuldfeq  46228  fmul01lt1lem1  46229  fmul01lt1lem2  46230  fmul01lt1  46231  fprodsplit1  46238  fprodexp  46239  fprodabs2  46240  mccllem  46242  mccl  46243  fprodcnlem  46244  fprodcn  46245  climexp  46250  climsuse  46253  climrecf  46254  climinff  46256  climaddf  46260  mullimc  46261  ellimcabssub0  46262  islptre  46264  climf  46267  mullimcf  46268  rexlim2d  46270  idlimc  46271  limcperiod  46273  limcrecl  46274  sumnnodd  46275  islpcn  46282  limsupre  46284  limcleqr  46287  neglimc  46290  addlimc  46291  0ellimcdiv  46292  limclner  46294  climsubmpt  46303  climreclf  46307  climf2  46309  fnlimcnv  46310  climeldmeqmpt  46311  clim2f2  46313  climfveqmpt  46314  fnlimfvre  46317  allbutfifvre  46318  climleltrp  46319  fnlimf  46321  fnlimabslt  46322  climfveqmpt3  46325  climeldmeqf  46326  limsupref  46328  limsupbnd1f  46329  climbddf  46330  climeqf  46331  climeldmeqmpt3  46332  limsuplesup  46342  limsuppnfd  46345  limsupub  46347  limsupres  46348  climinf2lem  46349  climinf2  46350  limsuppnf  46354  limsupubuzlem  46355  limsupubuz  46356  climinf2mpt  46357  climinfmpt  46358  climinf3  46359  limsupmnflem  46363  limsupmnf  46364  limsupequz  46366  limsupre2  46368  limsupmnfuzlem  46369  limsupmnfuz  46370  limsupequzmptf  46374  limsupre3lem  46375  limsupre3  46376  limsupre3uzlem  46378  limsupre3uz  46379  limsupreuz  46380  limsupvaluz2  46381  limsupreuzmpt  46382  supcnvlimsup  46383  climuzlem  46386  climuz  46387  climisp  46389  lmbr3  46390  climrescn  46391  climxrrelem  46392  climxrre  46393  liminfcl  46406  liminfval2  46411  limsup10exlem  46415  liminflelimsuplem  46418  limsupgtlem  46420  limsupgt  46421  climliminflimsupd  46444  liminfreuzlem  46445  liminfreuz  46446  liminfltlem  46447  liminflt  46448  limsupub2  46455  xlimpnfxnegmnf  46457  liminflbuz2  46458  liminfpnfuz  46459  liminflimsupxrre  46460  xlimmnfvlem1  46475  xlimmnfvlem2  46476  xlimmnfv  46477  xlimpnfvlem1  46479  xlimpnfvlem2  46480  xlimpnfv  46481  xlimmnf  46484  xlimpnf  46485  xlimmnfmpt  46486  xlimpnfmpt  46487  climxlim2lem  46488  dfxlim2  46491  cncfshift  46517  icccncfext  46530  cncficcgt0  46531  cncfiooicc  46537  cncfioobd  46540  fprodcncf  46543  fprodsubrecnncnvlem  46550  fprodaddrecnncnvlem  46552  dvmptmulf  46580  dvnmptdivc  46581  dvnmul  46586  dvmptfprodlem  46587  dvmptfprod  46588  dvnprodlem1  46589  dvnprodlem2  46590  iblsplitf  46613  iblspltprt  46616  itgioocnicc  46620  iblcncfioo  46621  itgspltprt  46622  itgperiod  46624  stoweidlem3  46646  stoweidlem14  46657  stoweidlem17  46660  stoweidlem19  46662  stoweidlem20  46663  stoweidlem26  46669  stoweidlem27  46670  stoweidlem28  46671  stoweidlem29  46672  stoweidlem31  46674  stoweidlem34  46677  stoweidlem35  46678  stoweidlem36  46679  stoweidlem39  46682  stoweidlem42  46685  stoweidlem43  46686  stoweidlem44  46687  stoweidlem46  46689  stoweidlem48  46691  stoweidlem49  46692  stoweidlem50  46693  stoweidlem51  46694  stoweidlem52  46695  stoweidlem53  46696  stoweidlem54  46697  stoweidlem56  46699  stoweidlem57  46700  stoweidlem59  46702  stoweidlem60  46703  stoweidlem61  46704  stoweidlem62  46705  stoweid  46706  wallispilem3  46710  stirlinglem13  46729  stirling  46732  fourierdlem16  46766  fourierdlem21  46771  fourierdlem22  46772  fourierdlem31  46781  fourierdlem39  46789  fourierdlem48  46797  fourierdlem51  46800  fourierdlem53  46802  fourierdlem68  46817  fourierdlem69  46818  fourierdlem71  46820  fourierdlem73  46822  fourierdlem77  46826  fourierdlem80  46829  fourierdlem81  46830  fourierdlem82  46831  fourierdlem83  46832  fourierdlem86  46835  fourierdlem87  46836  fourierdlem89  46838  fourierdlem91  46840  fourierdlem93  46842  fourierdlem94  46843  fourierdlem103  46852  fourierdlem104  46853  fourierdlem112  46861  fourierdlem113  46862  elaa2  46877  etransclem18  46895  etransclem22  46899  etransclem23  46900  etransclem32  46909  etransclem35  46912  etransclem44  46921  etransclem46  46923  etransclem48  46925  rrndistlt  46933  ioorrnopnlem  46947  saliuncl  46966  saliincl  46970  intsaluni  46972  salexct  46977  subsaliuncl  47001  sge00  47019  sge0revalmpt  47021  sge0sn  47022  sge0f1o  47025  sge0gerp  47038  sge0pnffigt  47039  sge0lefi  47041  sge0ltfirp  47043  sge0resrnlem  47046  sge0resplit  47049  sge0lempt  47053  sge0iunmptlemfi  47056  sge0p1  47057  sge0iunmptlemre  47058  sge0fodjrnlem  47059  sge0iunmpt  47061  sge0rpcpnf  47064  sge0ltfirpmpt2  47069  sge0isum  47070  sge0xp  47072  sge0ad2en  47074  sge0isummpt2  47075  sge0xaddlem1  47076  sge0xaddlem2  47077  sge0xadd  47078  sge0pnffsumgt  47085  sge0gtfsumgt  47086  sge0uzfsumgt  47087  sge0seq  47089  sge0reuz  47090  sge0reuzb  47091  iundjiun  47103  meadjiunlem  47108  meadjiun  47109  ismeannd  47110  voliunsge0lem  47115  meaiuninclem  47123  meaiunincf  47126  meaiuninc3v  47127  meaiuninc3  47128  meaiininclem  47129  meaiininc  47130  meaiininc2  47131  caragenfiiuncl  47158  omeiunltfirp  47162  carageniuncllem1  47164  carageniuncllem2  47165  caratheodorylem2  47170  0ome  47172  isomenndlem  47173  hoicvrrex  47199  ovnsupge0  47200  ovnlecvr  47201  ovnlerp  47205  ovncvrrp  47207  ovn0lem  47208  ovnsubaddlem1  47213  ovnsubaddlem2  47214  hoidmvcl  47225  hsphoidmvle2  47228  hsphoidmvle  47229  hoidmvval0  47230  sge0hsphoire  47232  hoidmvval0b  47233  hoidmv1lelem1  47234  hoidmv1lelem2  47235  hoidmv1lelem3  47236  hoidmvlelem1  47238  hoidmvlelem2  47239  hoidmvlelem3  47240  hoidmvlelem4  47241  hoidmvlelem5  47242  hoidmvle  47243  ovnhoilem1  47244  ovnhoilem2  47245  ovnhoi  47246  ovnlecvr2  47253  hspdifhsp  47259  hoidifhspdmvle  47263  hoiqssbllem3  47267  hspmbllem1  47269  hspmbllem2  47270  opnvonmbllem1  47275  opnvonmbllem2  47276  ovnsubadd2lem  47288  ovolval5lem1  47295  ovnovollem1  47299  ovnovollem2  47300  hoimbl2  47308  vonhoire  47315  iinhoiicclem  47316  iinhoiicc  47317  iunhoiioolem  47318  iunhoiioo  47319  vonioolem1  47323  vonioolem2  47324  vonioo  47325  vonicclem1  47326  vonicclem2  47327  vonicc  47328  vonn0ioo2  47333  vonn0icc2  47335  vonct  47336  pimltmnf2f  47340  pimgtpnf2f  47348  salpreimagelt  47350  salpreimalegt  47352  pimltpnf2f  47355  pimgtmnf2  47357  pimdecfgtioc  47358  pimincfltioc  47359  pimdecfgtioo  47360  pimincfltioo  47361  preimageiingt  47363  preimaleiinlt  47364  salpreimagtge  47368  salpreimaltle  47369  salpreimalelt  47372  salpreimagtlt  47373  issmff  47377  sssmf  47381  mbfresmf  47382  cnfsmf  47383  incsmflem  47384  incsmf  47385  smfsssmf  47386  issmflelem  47387  issmfle  47388  smfconst  47392  issmfgtlem  47398  issmfgt  47399  smfpimltxrmptf  47401  smfmbfcex  47403  smfaddlem1  47406  smfaddlem2  47407  smfadd  47408  decsmflem  47409  decsmf  47410  smfpreimagtf  47411  issmfgelem  47412  issmfge  47413  smflimlem2  47415  smflimlem4  47417  smflim  47420  smfpimgtxr  47423  smfpimgtxrmptf  47427  smfpimioo  47430  smfresal  47431  smfrec  47432  smfres  47433  smfmullem2  47435  smfmullem4  47437  smfmul  47438  smfpimbor1lem2  47442  smf2id  47444  smfco  47445  smflim2  47449  smfpimcc  47451  smflimmpt  47453  smfsuplem1  47454  smfsuplem3  47456  smfsup  47457  smfsupmpt  47458  smfsupxr  47459  smfinflem  47460  smfinf  47461  smfinfmpt  47462  smflimsuplem3  47465  smflimsuplem4  47466  smflimsuplem5  47467  smflimsuplem7  47469  smflimsuplem8  47470  smflimsup  47471  smflimsupmpt  47472  smfliminflem  47473  smfliminf  47474  smfliminfmpt  47475  smfpimne2  47483  fsupdm  47485  smfsupdmmbllem  47487  smfsupdmmbl  47488  finfdm  47489  smfinfdmmbllem  47491  smfinfdmmbl  47492  or2expropbilem1  47695  or2expropbilem2  47696  or2expropbi  47697  cfsetsnfsetf  47721  cfsetsnfsetfo  47723  rexsb  47762  reuf1odnf  47770  2reu8i  47776  ffnafv  47834  tz6.12c-afv2  47905  f1oresf1o2  47954  iccelpart  48108  iccpartdisj  48112  dfich2  48133  ichbi12i  48135  ichnfimlem  48138  ich2exprop  48146  ichnreuop  48147  ichreuopeq  48148  sprsymrelfo  48172  reupr  48197  reuopreuprim  48201  mogoldbb  48476  2zrngagrp  48940  2zrngmmgm  48943  cbvmpox2  49038  ovmpordx  49042  1arymaptfo  49345  2arymaptfo  49356  mo0sn  49516  iinfssclem3  49756  iinfssc  49757  iinfsubc  49758  infsubc2  49761  iinfconstbas  49766  isthincd2lem1  50125  nfintd  50373  nfiund  50374  nfiundg  50375  iunord  50376  spcdvw  50379  nfsetrecs  50386  setrec1lem2  50388  setrec1  50391  setrec2fun  50392  pgindnf  50416  pgind  50417  aacllem  50512