Theorem nfv 1949

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 1948	. 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 1945

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

This theorem is used by:  nfvd  1950  cbvaldw  2371  cbval2v  2376  dvelimhw  2378  pm11.53  2379  19.12vv  2380  eeanv  2382  eeeanv  2383  ee4anv  2384  sbnf2  2390  exsb  2391  2exsb  2392  sbbibvv  2394  cbvsbvf  2395  cleljustALT2  2397  spimv  2422  spimev  2424  chvarv  2428  cbvalv  2432  cbvexv  2433  cbvald  2439  cbvaldva  2441  cbvexdva  2442  cbval2  2443  axc16i  2468  dvelimnf  2485  sbel2x  2506  sbiedv  2536  2sbiev  2537  sbid2v  2541  sbhb  2553  2sb8e  2562  nfmod2  2586  nfmodv  2587  mof  2591  mo4f  2595  euf  2604  sb8eulem  2626  cbvmow  2631  sbmo  2642  moexexvw  2656  moexexv  2667  2mo  2676  2eu6  2684  axextmo  2739  nulmo  2740  abbibOLD  2833  cleqh  2893  nfcv  2926  nfeqd  2936  nfeld  2937  nfabdw  2947  nfabd  2948  dvelimdc  2950  nfcvf  2952  cleqf  2954  r19.29af  3275  rexbidvALT  3281  rexbidvaALT  3282  2ralbida  3289  r19.12  3315  reean  3316  cbvrexsvw  3318  sbralieOLD  3344  cbvralf  3349  cbvralv  3353  cbvrexv  3354  cbvralsv  3355  cbvrexsv  3356  cbvrmow  3394  cbvreu  3408  cbvrmov  3410  cbvreuv  3411  cbvrab  3453  cbvexeqsetf  3469  ceqsex2  3504  vtocl2gaf  3542  vtocl3gaf  3543  spc2ed  3559  rspct  3566  rspc  3568  rspce  3569  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  3817  reu8nf  3828  rmo2  3838  rmo3  3840  rmoanimALT  3847  nfcsb1d  3873  nfcsbd  3876  csbiebt  3880  csbie2t  3889  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  cbvralv2  3897  cbvrexv2  3898  rspc2vd  3899  dfssf  3904  rabss3d  4009  eqrrabd  4014  uniiunlem  4015  ab0orv  4335  ab0orvALT  4336  sbcnestgw  4384  sbcnestg  4389  sbnfc2  4400  r19.3rzvOLD  4463  r19.28zv  4465  r19.27zv  4470  2reu4lem  4482  nfifd  4515  reusngf  4635  reusng  4638  rexreusng  4640  reuprg0  4663  rabsnifsb  4683  euabsn  4687  nfunid  4876  eluniab  4884  nfint  4920  iuneqconst  4966  disjiun  5094  disjxun  5104  nfopabd  5176  cbvopab  5180  cbvopab1  5182  cbvopab1g  5183  cbvopab2  5184  cbvopab1s  5185  mpteq12da  5191  mpteq12f  5193  cbvmptf  5208  cbvmptfg  5209  axrep1  5236  axrep2  5238  axrep3  5239  axrep5  5242  zfrepclf  5247  reusv2lem3  5366  reusv2lem4  5367  reusv2  5369  reusv3  5371  alxfr  5373  ralxfrALT  5381  copsex2t  5468  iunopeqop  5498  iunopeqopOLD  5499  rexopabb  5506  opelopabaf  5523  nfso  5570  pofun  5581  isso2i  5600  nffr  5628  opeliunxp  5722  opeliun2xp  5723  opeliunxp2  5820  ralxpf  5829  dfdmf  5884  dfrnf  5938  elrnmpt1  5948  dfrel4  6194  reuop  6311  frpoinsg  6361  frpoins2g  6363  wfis2g  6373  nfiotadw  6512  nfiotad  6514  cbviotaw  6516  cbviota  6518  cbviotav  6519  sb8iota  6520  iota2d  6542  iota2  6543  dffun6f  6570  imadif  6643  isarep1  6647  isarep2  6648  fv3  6923  tz6.12f  6930  funimassd  6971  fvelimad  6972  feqmptdf  6975  fimarab  6979  opabiotafun  6985  funfv2f  6994  fvmptd  7021  fvmptd2f  7030  fvmptdv  7031  fvmptt  7034  fvopab5  7047  eqfnfv2f  7053  ralrnmptw  7115  ralrnmpt  7117  dffo3f  7127  f1ompt  7132  fompt  7139  ffnfv  7140  ffnfvf  7141  f1ossf1o  7150  fmptco  7151  elabrex  7266  elabrexg  7267  dff13f  7279  fsnex  7311  fliftfun  7340  cbvriotaw  7406  cbvriota  7410  cbvriotav  7411  riota2  7422  riotaeqimp  7423  riota5f  7425  oprabv  7500  nfoprab  7504  mpoeq123  7512  cbvoprab1  7527  cbvoprab2  7528  cbvoprab12  7529  cbvoprab3  7531  cbvmpox  7533  ralrnmpo  7580  ovmpodx  7592  ovmpodf  7597  ovmpodv  7598  ov3  7604  ovmpt3rab1  7700  ofrfval2  7735  onminex  7837  tfis  7887  tfis2  7889  tfisi  7891  tfinds  7892  tfindes  7895  findes  7933  fiun  7976  f1iun  7977  abrexex2g  7997  opabex3d  7998  opabex3rd  7999  opabex3  8000  dfoprab4f  8089  fmpox  8100  offval22  8121  ovmptssOLD  8127  f1od2  8132  ralxpes  8177  ralxp3  8179  ralxp3es  8180  frpoins3xpg  8181  frpoins3xp3g  8182  opeliunxp2f  8252  tposoprab  8304  fvmpocurryd  8313  nffrecs  8326  tfr3  8432  nfrdg  8447  tz7.48-1  8478  tz7.49  8480  naddsuc2  8736  eqerlem  8778  erovlem  8859  mptelixpg  8988  boxcutc  8994  dom2lem  9044  xpf1o  9183  mapxpen  9187  findcard2  9205  pssnn  9209  nneneq  9246  ac6sfi  9300  fiint  9343  indexfi  9374  wdom2d  9598  ixpiunwdom  9608  cantnflem1  9714  nfttrcld  9735  setinds2  9776  frinsg  9779  frins2  9782  r1val1  9817  rankuni2b  9891  nfscott  9956  scottabf  9963  scottab  9964  scottexsOLD  9967  scott0bsOLD  9969  setrec1lem2  9991  spcdvw  9994  setrec1  9996  setrec2fun  9997  dfac8clem  10135  acni2  10149  aceq1  10220  dfac5lem5  10230  kmlem15  10267  infpssrlem4  10408  fin23lem27  10430  hsmexlem2  10529  hsmexlem4  10531  axcc3  10540  domtriomlem  10544  axdc3lem2  10553  axdc3lem4  10555  axdc4lem  10557  ac6c4  10583  zorn2lem4  10601  zorn2lem5  10602  iunfo  10647  iundom2g  10648  uniimadomf  10653  konigthlem  10677  axrepndlem2  10702  axunnd  10705  axpowndlem2  10707  axpowndlem4  10709  axregndlem2  10712  axacndlem5  10720  zfcndrep  10723  zfcndinf  10727  pwfseqlem4a  10770  pwfseqlem4  10771  tskuni  10892  gruiin  10919  reclem2pr  11157  dedekind  11497  dedekindle  11498  fimaxre3  12287  nn0ind-raph  12823  uzind4s  13059  nnwof  13065  lbzbi  13087  fzrevral  13770  rabssnn0fi  14153  fsuppmapnn0fiublem  14157  fsuppmapnn0fiub  14158  fsuppmapnn0fiubex  14159  seqof2  14227  reuccatpfxs1  14921  cotr2g  15155  rlim2  15689  ello1mpt  15714  climeu  15748  o1compt  15780  summolem2a  15907  zsum  15910  sumss  15916  sumss2  15918  fsumcvg2  15919  fsumclf  15930  fsumsplitf  15934  fsumsplit1  15937  fsum2dlem  15962  fsum00  15991  o1fsum  16006  nfcprod1  16103  nfcprod  16104  prodmolem2a  16127  zprod  16130  fprod  16134  fprodntriv  16135  prodss  16140  fprodn0  16172  fprod2dlem  16173  fprodsplitf  16181  fprodsplit1f  16183  fprodle  16189  fprodmodd  16190  lcmfunsnlem1  16838  lcmfunsnlem2lem1  16839  lcmfunsnlem2  16841  coprmprod  16862  coprmproddvdslem  16863  prmind2  16886  iserodd  17039  pcmpt  17096  pcmptdvds  17098  prmolefac  17250  mreexexd  17848  catpropd  17909  invfuc  18178  natpropd  18180  fucpropd  18181  initoeu2  18217  acsmapd  18754  nfchnd  18811  symgval  19612  gsumsnd  20193  gsumsnf  20194  gsumunsnfd  20198  gsummptf1o  20204  gsummpt1n0  20206  gsum2d2lem  20214  gsumcom2  20216  gsummptnn0fz  20227  dprd2d2  20287  rngqiprngimf1  21623  gsummoncoe1  22653  gsumply1eq  22654  mdetralt2  22951  mdetunilem2  22955  madugsum  22985  gsummatr01lem4  23000  matunitlindflem2  23022  cpmatmcllem  23063  cayleyhamilton1  23237  neiptopnei  23477  neiptopreu  23478  neitr  23525  fiuncmp  23749  iunconnlem  23772  iunconn  23773  2ndcdisj  23802  dissnlocfin  23875  elptr2  23920  ptbasfi  23927  ptcld  23959  ptcldmpt  23960  ptclsg  23961  ptcnplem  23967  ptcnp  23968  cnmpt11  24009  cnmpt21  24017  cnmptcom  24024  imasnopn  24036  imasncld  24037  imasncls  24038  xkocnv  24160  elmptrab  24173  isfildlem  24203  alexsubALTlem3  24395  cnextfvval  24411  utopsnneiplem  24593  isucn2  24624  cfilucfil  24905  blval2  24908  restmetu  24916  ovoliunlem3  25852  ovoliun  25853  ovoliun2  25854  ovoliunnul  25855  finiunmbl  25892  volfiniun  25895  iundisj  25896  iunmbl  25901  voliun  25902  iunmbl2  25905  mbfeqalem1  25989  mbfsup  26012  mbfinf  26013  mbflim  26016  itg2splitlem  26096  itg2split  26097  isibl2  26114  cbvitg  26123  itgeqa  26161  itgss3  26162  itgfsum  26174  itgabs  26182  itggt0  26191  itgcn  26192  limcmpt  26230  limciun  26241  dvmptfsum  26322  dvlipcn  26341  dvfsumlem2  26374  dvfsumlem4  26376  dvfsumrlim  26378  dvfsum2  26381  itgsubst  26396  coeeq2  26588  dgrle  26589  ulmss  26751  leibpi  27297  rlimcnp  27320  rlimcnp2  27321  o1cxp  27329  lgamgulmlem2  27384  lgamgulmlem6  27388  fsumdvdscom  27539  lgseisenlem2  27730  2sqmo  27791  2sqreulem4  27808  dchrisumlema  27842  dchrisumlem2  27844  dchrisumlem3  27845  nosupbnd1  28098  nosupbnd2  28100  noinfbnd1  28113  noinfbnd2  28115  bdayiun  28328  bdaypw2n0bndlem  28876  istrkg2ld  28949  prlngmo2  29461  mpteleeOLD  29500  gropd  29636  grstructd  29637  clwwlknonclwlknonf1o  30990  dlwwlknondlwlknonf1o  30993  ex-natded9.26  31047  isch3  31870  atom1d  32982  chirred  33024  sbc2iedf  33131  rspc2daf  33132  19.9d2r  33136  opreu2reuALT  33142  mo5f  33154  reuxfrdf  33156  foresf1o  33169  elabreximdv  33176  iinabrex  33232  cbvdisjf  33234  disjorf  33242  disjabrex  33245  iundisjf  33252  disjunsn  33257  brabgaf  33269  ac6sf2  33285  dfimafnf  33299  2ndresdju  33312  fmptcof2  33320  acunirnmpt2  33323  acunirnmpt2f  33324  aciunf1lem  33325  aciunf1  33326  ofpreima  33328  funcnv5mpt  33330  funcnv4mpt  33331  fnpreimac  33333  fpwrelmap  33392  xrofsup  33426  iundisjfi  33455  nnindf  33478  nn0min  33479  fprodex01  33483  fsumiunle  33487  prodindf  33496  gsummpt2d  33677  gsummptf1od  33683  gsummptfsf1o  33688  gsumhashmul  33695  suppgsumssiun  33700  gsumwrd2dccat  33706  isarchiofld  33827  elrgspnsubrunlem2  33876  nsgmgc  34030  nsgqusf1olem1  34031  nsgqusf1olem3  34033  nsgqusf1o  34034  elrspunidl  34045  elrspunsn  34046  deg1prod  34182  ply1gsumz  34198  ig1pmindeg  34201  mplvrpmga  34244  psrgsum  34247  psrmonprod  34251  esplylem  34265  esplyfv1  34268  esplyfval1  34272  esplyfvaln  34273  esplyind  34274  vieta  34279  exsslsb  34296  ply1degltdimlem  34321  fedgmullem2  34329  evls1fldgencl  34369  irngnzply1  34390  extdgfialglem2  34392  ply1annidllem  34400  algextdeglem6  34421  constrfin  34445  reff  34538  locfinreflem  34539  cmpcref  34549  zarclsiin  34570  zarcls  34573  zarcmplem  34580  ordtconnlem1  34623  qqhval2  34681  esumeq12dva  34731  esumeq2dv  34737  esumrnmpt  34751  esumpad  34754  esumpad2  34755  esumadd  34756  gsumesum  34758  esumlub  34759  esumsnf  34763  esumpr  34765  esumrnmpt2  34767  esumfzf  34768  esumfsup  34769  esumpcvgval  34777  esumpmono  34778  esumcocn  34779  hasheuni  34784  esumcvg  34785  esumgect  34789  esum2dlem  34791  esum2d  34792  esumiun  34793  ldsysgenld  34860  sigapildsyslem  34861  sigapildsys  34862  ldgenpisyslem1  34863  fiunelros  34874  measvunilem  34912  measvunilem0  34913  measvuni  34914  measiun  34918  measinblem  34920  voliune  34929  volfiniune  34930  volmeas  34931  ddemeas  34936  oms0  34996  omssubadd  34999  carsgclctunlem1  35016  carsggect  35017  omsmeas  35022  eulerpartlemgvv  35075  dstrvprob  35171  ballotlemodife  35197  reprsuc  35311  reprdifc  35323  breprexplema  35326  breprexplemc  35328  circlemethhgt  35339  hgt750lemd  35344  bnj919  35465  bnj1146  35488  bnj1379  35527  bnj1385  35529  bnj1400  35532  bnj1534  35550  bnj1542  35554  bnj110  35555  bnj121  35567  bnj124  35568  bnj130  35571  bnj207  35578  bnj571  35603  bnj605  35604  bnj580  35610  bnj607  35613  bnj611  35615  bnj873  35621  bnj849  35622  bnj900  35626  bnj916  35630  bnj1000  35638  bnj964  35640  bnj981  35647  bnj985v  35650  bnj985  35651  bnj1014  35658  bnj1123  35683  bnj1128  35687  bnj1228  35708  bnj1204  35709  bnj1279  35715  bnj1307  35720  bnj1321  35724  bnj1388  35730  bnj1398  35731  bnj1408  35733  bnj1417  35738  bnj1444  35740  bnj1445  35741  bnj1446  35742  bnj1449  35745  bnj1467  35751  bnj1489  35753  bnj1312  35755  bnj1497  35757  bnj1518  35761  bnj1525  35766  bnj1529  35767  dvelimalcased  35772  dvelimexcased  35774  reu6f  35776  rankse  35822  fineqvrep  35881  axsepg2  35907  axsepg3  35908  axsepg3ALT  35909  axpowg2  35914  axpowg3  35915  onvf1odlem2  36031  srepdflem1  36084  srepdflem2  36085  srepdf  36086  smrepsrep  36087  cvmcov  36194  untsucf  36652  dfon2lem3  36724  finminlem  37283  weiunpo  37430  weiunso  37431  weiunfr  37432  weiunse  37433  axtcond  37443  regsfromregtco  37503  regsfromsetind  37504  mh-inf3f1  37506  bj-nexdvt  37777  bj-cbvaldv  37888  bj-cbval2vv  37890  bj-cbvex2vv  37891  bj-cbvaldvav  37892  bj-cbvexdvav  37893  ax11-pm2  37925  bj-dvelimdv  37940  bj-nfeel2  37943  bj-ceqsalv  37983  bj-vtocl  38005  bj-inrab2  38018  currysetlem  38035  currysetlem1  38037  bj-axseprep  38180  bj-axreprepsep  38181  bj-opabco  38300  mptsnunlem  38452  exlimim  38456  exellim  38458  topdifinfindis  38460  topdifinffinlem  38461  icorempo  38465  isbasisrelowllem1  38469  isbasisrelowllem2  38470  relowlssretop  38477  finxpreclem2  38504  finxpreclem6  38510  fvineqsneu  38525  fvineqsneq  38526  wl-euequf  38697  wl-sb8eut  38701  wl-issetft  38705  phpreu  38718  ptrest  38728  ptrecube  38729  poimirlem2  38731  poimirlem23  38752  poimirlem24  38753  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  heicant  38764  mbfposadd  38776  itgabsnc  38798  itggt0cn  38799  ftc1anclem5  38806  upixp  38854  indexa  38858  indexdom  38859  filbcmb  38865  sdclem2  38867  sdclem1  38868  fdc1  38871  totbndbnd  38914  sbcalf  39237  sbcexf  39238  scottexf  39291  scott0f  39292  eqrelf  39381  ralrmo3  39487  disjqmap2  39949  fsumshftd  40200  riotasv2d  40205  riotasv2s  40206  riotasv3d  40208  glbconxN  40626  pmapglbx  41017  pmapglb2xN  41020  cdleme26ee  41608  cdleme31sn  41628  cdleme31sn1  41629  cdlemefr29exN  41650  cdlemefs32sn1aw  41662  cdleme43fsv1snlem  41668  cdleme41sn3a  41681  cdleme32fva  41685  cdleme32d  41692  cdleme32f  41694  cdleme40m  41715  cdleme40n  41716  cdleme42b  41726  cdlemk36  42161  cdlemk38  42163  cdlemkid  42184  cdlemk19x  42191  cdlemk11t  42194  dihvalcqpre  42483  mapdheq  42976  hdmap1eq  43049  hdmapval2lem  43079  lcmineqlem9  43278  lcmineqlem12  43281  aks4d1p1p2  43311  mndmolinv  43336  primrootsunit1  43338  primrootsunit  43339  primrootspoweq0  43347  aks6d1c1p5  43353  aks6d1c3  43364  aks6d1c4  43365  aks6d1c1rh  43366  aks6d1c2lem4  43368  aks6d1c2  43371  deg1gprod  43381  sticksstones1  43387  sticksstones11  43397  sticksstones16  43403  sticksstones22  43409  aks6d1c6lem2  43412  aks6d1c6isolem1  43415  aks6d1c6isolem2  43416  bcled  43419  bcle2d  43420  aks6d1c7lem3  43423  aks6d1c7  43425  rhmqusspan  43426  grpods  43435  unitscyglem1  43436  unitscyglem2  43437  unitscyglem3  43438  unitscyglem4  43439  unitscyglem5  43440  nfa1w  43877  mzpexpmpt  43947  eq0rabdioph  43978  rexrabdioph  43992  rexfrabdioph  43993  elnn0rabdioph  44001  dvdsrabdioph  44008  fphpd  44014  monotuz  44139  monotoddzz  44141  oddcomabszz  44142  setindtr  44222  dford4  44227  wdom2d2  44233  aomclem6  44252  aomclem8  44254  flcidc  44362  areaquad  44408  unielss  44410  onsucf1lem  44461  oaun3lem1  44566  nadd1suc  44584  rababg  44765  ss2iundv  44850  cbviuneq12dv  44852  gneispace  45324  mnringvald  45401  mnringmulrcld  45416  mnuprdlem4  45449  ismnushort  45475  binomcxplemdvsum  45529  binomcxplemnotnn0  45530  aaanv  45562  pm11.57  45563  pm11.58  45564  pm11.59  45565  pm11.71  45571  pm14.12  45594  ssralv2  45703  tratrb  45708  iunconnlem2  46106  modelaxreplem3  46163  modelaxrep  46164  permaxrep  46189  evth2f  46235  elunif  46236  fvelrnbf  46238  evthf  46247  fnchoice  46249  sumpair  46255  rfcnnnub  46256  refsum2cn  46258  uzwo4  46273  fiiuncl  46285  fiunicl  46287  elintdv  46299  ssd  46300  cbvmpo2  46315  cbvmpo1  46316  eliin2f  46322  eliuniin2  46338  cbvrabv2  46345  suprnmpt  46392  disjf1  46401  disjrnmpt2  46406  disjf1o  46409  disjinfi  46410  choicefi  46417  iunmapsn  46433  axccdom  46438  dmrelrnrel  46442  axccd  46444  fmptf  46454  rnmptlb  46458  rnmptbddlem  46459  rnmptbd2lem  46463  rnmptbdlem  46470  rnmptbd  46471  fmptff  46484  upbdrech  46524  ssfiunibd  46528  supxrgere  46548  iuneqfzuzlem  46549  supxrgelem  46552  supxrge  46553  suplesup  46554  infrpge  46566  xralrple2  46569  infxr  46581  infxrunb2  46582  infleinf  46586  xrralrecnnle  46597  xrralrecnnge  46604  supxrunb3  46613  supxrleubrnmpt  46619  infleinf2  46627  unb2ltle  46628  rexabslelem  46631  rexabsle  46632  allbutfiinf  46633  suprleubrnmpt  46635  infrnmptle  46636  infxrunb3rnmpt  46641  uzublem  46643  uzub  46644  supminfrnmpt  46658  infxrpnf  46659  supxrleubrnmptf  46664  infxrgelbrnmpt  46667  infrpgernmpt  46678  supminfxr2  46682  monoordxr  46695  monoord2xr  46697  caucvgbf  46702  cvgcaule  46704  rexanuz2nf  46705  iccshift  46733  iooshift  46737  iooiinicc  46757  iooiinioc  46771  fsummulc1f  46786  fsumnncl  46787  fsumf1of  46789  fsumiunss  46790  fsumreclf  46791  fsumlessf  46792  fsumsermpt  46794  fmul01  46795  fmuldfeqlem1  46797  fmuldfeq  46798  fmul01lt1lem1  46799  fmul01lt1lem2  46800  fmul01lt1  46801  fprodsplit1  46808  fprodexp  46809  fprodabs2  46810  mccllem  46812  mccl  46813  fprodcnlem  46814  fprodcn  46815  climexp  46820  climsuse  46823  climrecf  46824  climinff  46826  climaddf  46830  mullimc  46831  ellimcabssub0  46832  islptre  46834  climf  46837  mullimcf  46838  rexlim2d  46840  idlimc  46841  limcperiod  46843  limcrecl  46844  sumnnodd  46845  islpcn  46852  limsupre  46854  limcleqr  46857  neglimc  46860  addlimc  46861  0ellimcdiv  46862  limclner  46864  climsubmpt  46873  climreclf  46877  climf2  46879  fnlimcnv  46880  climeldmeqmpt  46881  clim2f2  46883  climfveqmpt  46884  fnlimfvre  46887  allbutfifvre  46888  climleltrp  46889  fnlimf  46891  fnlimabslt  46892  climfveqmpt3  46895  climeldmeqf  46896  limsupref  46898  limsupbnd1f  46899  climbddf  46900  climeqf  46901  climeldmeqmpt3  46902  limsuplesup  46912  limsuppnfd  46915  limsupub  46917  limsupres  46918  climinf2lem  46919  climinf2  46920  limsuppnf  46924  limsupubuzlem  46925  limsupubuz  46926  climinf2mpt  46927  climinfmpt  46928  climinf3  46929  limsupmnflem  46933  limsupmnf  46934  limsupequz  46936  limsupre2  46938  limsupmnfuzlem  46939  limsupmnfuz  46940  limsupequzmptf  46944  limsupre3lem  46945  limsupre3  46946  limsupre3uzlem  46948  limsupre3uz  46949  limsupreuz  46950  limsupvaluz2  46951  limsupreuzmpt  46952  supcnvlimsup  46953  climuzlem  46956  climuz  46957  climisp  46959  lmbr3  46960  climrescn  46961  climxrrelem  46962  climxrre  46963  liminfcl  46976  liminfval2  46981  limsup10exlem  46985  liminflelimsuplem  46988  limsupgtlem  46990  limsupgt  46991  climliminflimsupd  47014  liminfreuzlem  47015  liminfreuz  47016  liminfltlem  47017  liminflt  47018  limsupub2  47025  xlimpnfxnegmnf  47027  liminflbuz2  47028  liminfpnfuz  47029  liminflimsupxrre  47030  xlimmnfvlem1  47045  xlimmnfvlem2  47046  xlimmnfv  47047  xlimpnfvlem1  47049  xlimpnfvlem2  47050  xlimpnfv  47051  xlimmnf  47054  xlimpnf  47055  xlimmnfmpt  47056  xlimpnfmpt  47057  climxlim2lem  47058  dfxlim2  47061  cncfshift  47087  icccncfext  47100  cncficcgt0  47101  cncfiooicc  47107  cncfioobd  47110  fprodcncf  47113  fprodsubrecnncnvlem  47120  fprodaddrecnncnvlem  47122  dvmptmulf  47150  dvnmptdivc  47151  dvnmul  47156  dvmptfprodlem  47157  dvmptfprod  47158  dvnprodlem1  47159  dvnprodlem2  47160  iblsplitf  47183  iblspltprt  47186  itgioocnicc  47190  iblcncfioo  47191  itgspltprt  47192  itgperiod  47194  stoweidlem3  47216  stoweidlem14  47227  stoweidlem17  47230  stoweidlem19  47232  stoweidlem20  47233  stoweidlem26  47239  stoweidlem27  47240  stoweidlem28  47241  stoweidlem29  47242  stoweidlem31  47244  stoweidlem34  47247  stoweidlem35  47248  stoweidlem36  47249  stoweidlem39  47252  stoweidlem42  47255  stoweidlem43  47256  stoweidlem44  47257  stoweidlem46  47259  stoweidlem48  47261  stoweidlem49  47262  stoweidlem50  47263  stoweidlem51  47264  stoweidlem52  47265  stoweidlem53  47266  stoweidlem54  47267  stoweidlem56  47269  stoweidlem57  47270  stoweidlem59  47272  stoweidlem60  47273  stoweidlem61  47274  stoweidlem62  47275  stoweid  47276  wallispilem3  47280  stirlinglem13  47299  stirling  47302  fourierdlem16  47336  fourierdlem21  47341  fourierdlem22  47342  fourierdlem31  47351  fourierdlem39  47359  fourierdlem48  47367  fourierdlem51  47370  fourierdlem53  47372  fourierdlem68  47387  fourierdlem69  47388  fourierdlem71  47390  fourierdlem73  47392  fourierdlem77  47396  fourierdlem80  47399  fourierdlem81  47400  fourierdlem82  47401  fourierdlem83  47402  fourierdlem86  47405  fourierdlem87  47406  fourierdlem89  47408  fourierdlem91  47410  fourierdlem93  47412  fourierdlem94  47413  fourierdlem103  47422  fourierdlem104  47423  fourierdlem112  47431  fourierdlem113  47432  elaa2  47447  etransclem18  47465  etransclem22  47469  etransclem23  47470  etransclem32  47479  etransclem35  47482  etransclem44  47491  etransclem46  47493  etransclem48  47495  rrndistlt  47503  ioorrnopnlem  47517  saliuncl  47536  saliincl  47540  intsaluni  47542  salexct  47547  subsaliuncl  47571  sge00  47589  sge0revalmpt  47591  sge0sn  47592  sge0f1o  47595  sge0gerp  47608  sge0pnffigt  47609  sge0lefi  47611  sge0ltfirp  47613  sge0resrnlem  47616  sge0resplit  47619  sge0lempt  47623  sge0iunmptlemfi  47626  sge0p1  47627  sge0iunmptlemre  47628  sge0fodjrnlem  47629  sge0iunmpt  47631  sge0rpcpnf  47634  sge0ltfirpmpt2  47639  sge0isum  47640  sge0xp  47642  sge0ad2en  47644  sge0isummpt2  47645  sge0xaddlem1  47646  sge0xaddlem2  47647  sge0xadd  47648  sge0pnffsumgt  47655  sge0gtfsumgt  47656  sge0uzfsumgt  47657  sge0seq  47659  sge0reuz  47660  sge0reuzb  47661  iundjiun  47673  meadjiunlem  47678  meadjiun  47679  ismeannd  47680  voliunsge0lem  47685  meaiuninclem  47693  meaiunincf  47696  meaiuninc3v  47697  meaiuninc3  47698  meaiininclem  47699  meaiininc  47700  meaiininc2  47701  caragenfiiuncl  47728  omeiunltfirp  47732  carageniuncllem1  47734  carageniuncllem2  47735  caratheodorylem2  47740  0ome  47742  isomenndlem  47743  hoicvrrex  47769  ovnsupge0  47770  ovnlecvr  47771  ovnlerp  47775  ovncvrrp  47777  ovn0lem  47778  ovnsubaddlem1  47783  ovnsubaddlem2  47784  hoidmvcl  47795  hsphoidmvle2  47798  hsphoidmvle  47799  hoidmvval0  47800  sge0hsphoire  47802  hoidmvval0b  47803  hoidmv1lelem1  47804  hoidmv1lelem2  47805  hoidmv1lelem3  47806  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem4  47811  hoidmvlelem5  47812  hoidmvle  47813  ovnhoilem1  47814  ovnhoilem2  47815  ovnhoi  47816  ovnlecvr2  47823  hspdifhsp  47829  hoidifhspdmvle  47833  hoiqssbllem3  47837  hspmbllem1  47839  hspmbllem2  47840  opnvonmbllem1  47845  opnvonmbllem2  47846  ovnsubadd2lem  47858  ovolval5lem1  47865  ovnovollem1  47869  ovnovollem2  47870  hoimbl2  47878  vonhoire  47885  iinhoiicclem  47886  iinhoiicc  47887  iunhoiioolem  47888  iunhoiioo  47889  vonioolem1  47893  vonioolem2  47894  vonioo  47895  vonicclem1  47896  vonicclem2  47897  vonicc  47898  vonn0ioo2  47903  vonn0icc2  47905  vonct  47906  pimltmnf2f  47910  pimgtpnf2f  47918  salpreimagelt  47920  salpreimalegt  47922  pimltpnf2f  47925  pimgtmnf2  47927  pimdecfgtioc  47928  pimincfltioc  47929  pimdecfgtioo  47930  pimincfltioo  47931  preimageiingt  47933  preimaleiinlt  47934  salpreimagtge  47938  salpreimaltle  47939  salpreimalelt  47942  salpreimagtlt  47943  issmff  47947  sssmf  47951  mbfresmf  47952  cnfsmf  47953  incsmflem  47954  incsmf  47955  smfsssmf  47956  issmflelem  47957  issmfle  47958  smfconst  47962  issmfgtlem  47968  issmfgt  47969  smfpimltxrmptf  47971  smfmbfcex  47973  smfaddlem1  47976  smfaddlem2  47977  smfadd  47978  decsmflem  47979  decsmf  47980  smfpreimagtf  47981  issmfgelem  47982  issmfge  47983  smflimlem2  47985  smflimlem4  47987  smflim  47990  smfpimgtxr  47993  smfpimgtxrmptf  47997  smfpimioo  48000  smfresal  48001  smfrec  48002  smfres  48003  smfmullem2  48005  smfmullem4  48007  smfmul  48008  smfpimbor1lem2  48012  smf2id  48014  smfco  48015  smflim2  48019  smfpimcc  48021  smflimmpt  48023  smfsuplem1  48024  smfsuplem3  48026  smfsup  48027  smfsupmpt  48028  smfsupxr  48029  smfinflem  48030  smfinf  48031  smfinfmpt  48032  smflimsuplem3  48035  smflimsuplem4  48036  smflimsuplem5  48037  smflimsuplem7  48039  smflimsuplem8  48040  smflimsup  48041  smflimsupmpt  48042  smfliminflem  48043  smfliminf  48044  smfliminfmpt  48045  smfpimne2  48053  fsupdm  48055  smfsupdmmbllem  48057  smfsupdmmbl  48058  finfdm  48059  smfinfdmmbllem  48061  smfinfdmmbl  48062  tmachlem-agreesn  48160  or2expropbilem1  48305  or2expropbilem2  48306  or2expropbi  48307  cfsetsnfsetf  48331  cfsetsnfsetfo  48333  rexsb  48373  reuf1odnf  48381  2reu8i  48387  ffnafv  48444  tz6.12c-afv2  48515  f1oresf1o2  48564  iccelpart  48718  iccpartdisj  48722  dfich2  48743  ichbi12i  48745  ichnfimlem  48748  ich2exprop  48756  ichnreuop  48757  ichreuopeq  48758  sprsymrelfo  48782  reupr  48807  reuopreuprim  48811  mogoldbb  49086  2zrngagrp  49549  2zrngmmgm  49552  cbvmpox2  49651  ovmpordx  49655  1arymaptfo  49958  2arymaptfo  49969  mo0sn  50130  iinfssclem3  50373  iinfssc  50374  iinfsubc  50375  infsubc2  50378  iinfconstbas  50383  isthincd2lem1  50763  nfintd  51059  nfiund  51060  nfiundg  51061  iunord  51062  nfsetrecs  51067  pgindnf  51087  pgind  51088  aacllem  51217