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  2343  cbval2v  2348  dvelimhw  2350  pm11.53  2351  19.12vv  2352  eeanv  2354  eeeanv  2355  ee4anv  2356  sbnf2  2363  exsb  2364  2exsb  2365  sbbibvv  2367  cbvsbvf  2368  cleljustALT2  2370  spimv  2395  spimev  2397  chvarv  2401  cbvalv  2405  cbvexv  2406  cbvald  2412  cbvaldva  2414  cbvexdva  2415  cbval2  2416  axc16i  2441  dvelimnf  2458  sbel2x  2479  sbiedv  2509  2sbiev  2510  sbid2v  2514  sbhb  2526  2sb8e  2535  nfmod2  2559  nfmodv  2560  mof  2564  mo4f  2568  euf  2577  sb8eulem  2599  cbvmow  2604  sbmo  2615  moexexvw  2629  moexexv  2640  2mo  2649  2mosOLD  2651  2eu6  2658  axextmo  2713  nulmo  2714  abbib  2806  cleqh  2866  nfcv  2899  nfeqd  2910  nfeld  2911  nfabdw  2921  nfabd  2922  dvelimdc  2924  nfcvf  2926  cleqf  2928  r19.29af  3247  rexbidvALT  3253  rexbidvaALT  3254  2ralbida  3261  r19.12  3287  reean  3288  cbvrexsvw  3290  cbvralsvwOLD  3291  cbvralsvwOLDOLD  3292  cbvrexsvwOLD  3293  sbralieOLD  3326  cbvralf  3332  cbvralv  3336  cbvrexv  3337  cbvralsv  3338  cbvrexsv  3339  cbvrmow  3377  cbvreu  3393  cbvrmov  3395  cbvreuv  3396  cbvrabwOLD  3437  cbvrab  3441  cbvexeqsetf  3457  ceqsex2  3495  vtocl2gaf  3536  vtocl2gafOLD  3537  vtocl3gaf  3538  vtocl3gafOLD  3539  spc2ed  3557  rspct  3564  rspc  3566  rspce  3567  eqvincf  3606  elrab3t  3647  ralab2  3657  rexab2  3659  mob2  3675  mob  3677  reu2  3685  rmo4f  3695  reu2eqd  3696  cdeqab1  3732  nfcdeq  3737  sbcco  3768  cbvsbcv  3778  elrabsf  3788  sbc2iegf  3817  reu8nf  3829  rmo2  3839  rmo3  3841  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  3926  rabss3d  4035  eqrrabd  4040  uniiunlem  4041  ab0orv  4337  ab0orvALT  4338  sbcnestgw  4377  sbcnestg  4382  sbnfc2  4393  r19.3rzvOLD  4459  r19.28zv  4461  r19.27zv  4466  2reu4lem  4478  nfifd  4511  reusngf  4633  reusng  4636  rexreusng  4638  reuprg0  4661  rabsnifsb  4681  euabsn  4685  nfunid  4871  eluniab  4879  nfint  4914  iuneqconst  4960  disjiun  5088  disjxun  5098  nfopabd  5168  cbvopab  5172  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  mpteq12da  5183  mpteq12f  5185  cbvmptf  5200  cbvmptfg  5201  axrep1  5227  axrep2  5229  axrep3  5230  axrep4OLD  5233  axrep5  5234  zfrepclf  5240  reusv2lem3  5349  reusv2lem4  5350  reusv2  5352  reusv3  5354  alxfr  5356  ralxfrALT  5364  axprlem3OLD  5377  axprlem4OLD  5378  axprlem5OLD  5379  copsex2t  5450  iunopeqop  5479  rexopabb  5486  opelopabaf  5502  nfso  5549  pofun  5560  isso2i  5579  nffr  5607  opeliunxp  5701  opeliun2xp  5702  opeliunxp2  5797  ralxpf  5805  dfdmf  5855  dfrnf  5909  elrnmpt1  5919  dfrel4  6159  reuop  6261  frpoinsg  6311  frpoins2g  6313  wfis2g  6323  nfiotadw  6461  nfiotad  6463  cbviotaw  6465  cbviota  6467  cbviotav  6468  sb8iota  6469  iota2d  6490  iota2  6491  dffun6f  6517  imadif  6586  isarep1  6591  isarep2  6592  fv3  6862  tz6.12f  6869  funimassd  6910  fvelimad  6911  feqmptdf  6914  fimarab  6918  opabiotafun  6924  funfv2f  6933  fvmptd  6959  fvmptd2f  6968  fvmptdv  6969  fvmptt  6972  fvopab5  6985  eqfnfv2f  6991  ralrnmptw  7050  ralrnmpt  7052  dffo3f  7062  f1ompt  7067  fompt  7074  ffnfv  7075  ffnfvf  7076  f1ossf1o  7085  fmptco  7086  elabrex  7200  elabrexg  7201  dff13f  7213  fsnex  7241  fliftfun  7270  cbvriotaw  7336  cbvriota  7340  cbvriotav  7341  riota2  7352  riotaeqimp  7353  riota5f  7355  oprabv  7430  nfoprab  7434  mpoeq123  7442  cbvoprab1  7457  cbvoprab2  7458  cbvoprab12  7459  cbvoprab3  7461  cbvmpox  7463  ralrnmpo  7509  ovmpodx  7521  ovmpodf  7526  ovmpodv  7527  ov3  7533  ovmpt3rab1  7628  ofrfval2  7655  onminex  7759  tfis  7809  tfis2  7811  tfisi  7813  tfinds  7814  tfindes  7817  findes  7854  fiun  7899  f1iun  7900  abrexex2g  7920  opabex3d  7921  opabex3rd  7922  opabex3  7923  dfoprab4f  8012  fmpox  8023  offval22  8042  ovmptss  8047  ralxpes  8090  ralxp3  8092  ralxp3es  8093  frpoins3xpg  8094  frpoins3xp3g  8095  opeliunxp2f  8164  tposoprab  8216  fvmpocurryd  8225  nffrecs  8237  tfr3  8342  nfrdg  8357  tz7.48-1  8386  tz7.49  8388  naddsuc2  8641  eqerlem  8683  erovlem  8764  mptelixpg  8887  boxcutc  8893  dom2lem  8943  xpf1o  9081  mapxpen  9085  findcard2  9103  pssnn  9107  nneneq  9144  ac6sfi  9198  fiint  9241  indexfi  9274  wdom2d  9499  ixpiunwdom  9509  cantnflem1  9612  nfttrcld  9633  setinds2  9674  frinsg  9677  frins2  9680  r1val1  9712  rankuni2b  9779  scottexs  9813  scott0s  9814  dfac8clem  9956  acni2  9970  aceq1  10041  dfac5lem5  10051  kmlem15  10089  infpssrlem4  10230  fin23lem27  10252  hsmexlem2  10351  hsmexlem4  10353  axcc3  10362  domtriomlem  10366  axdc3lem2  10375  axdc3lem4  10377  axdc4lem  10379  ac6c4  10405  zorn2lem4  10423  zorn2lem5  10424  iunfo  10463  iundom2g  10464  uniimadomf  10469  konigthlem  10493  axrepndlem2  10518  axunnd  10521  axpowndlem2  10523  axpowndlem4  10525  axregndlem2  10528  axacndlem5  10536  zfcndrep  10539  zfcndinf  10543  pwfseqlem4a  10586  pwfseqlem4  10587  tskuni  10708  gruiin  10735  reclem2pr  10973  dedekind  11310  dedekindle  11311  fimaxre3  12102  nn0ind-raph  12606  uzind4s  12835  nnwof  12841  lbzbi  12863  fzrevral  13542  rabssnn0fi  13923  fsuppmapnn0fiublem  13927  fsuppmapnn0fiub  13928  fsuppmapnn0fiubex  13929  seqof2  13997  reuccatpfxs1  14684  cotr2g  14913  rlim2  15433  ello1mpt  15458  climeu  15492  o1compt  15524  summolem2a  15652  zsum  15655  sumss  15661  sumss2  15663  fsumcvg2  15664  fsumclf  15675  fsumsplitf  15679  fsumsplit1  15682  fsum2dlem  15707  fsum00  15735  o1fsum  15750  nfcprod1  15845  nfcprod  15846  prodmolem2a  15871  zprod  15874  fprod  15878  fprodntriv  15879  prodss  15884  fprodn0  15916  fprod2dlem  15917  fprodsplitf  15925  fprodsplit1f  15927  fprodle  15933  fprodmodd  15934  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2  16581  coprmprod  16602  coprmproddvdslem  16603  prmind2  16626  iserodd  16777  pcmpt  16834  pcmptdvds  16836  prmolefac  16988  mreexexd  17585  catpropd  17646  invfuc  17915  natpropd  17917  fucpropd  17918  initoeu2  17954  acsmapd  18491  nfchnd  18548  symgval  19317  gsumsnd  19898  gsumsnf  19899  gsumunsnfd  19903  gsummptf1o  19909  gsummpt1n0  19911  gsum2d2lem  19919  gsumcom2  19921  gsummptnn0fz  19932  dprd2d2  19992  rngqiprngimf1  21272  gsummoncoe1  22269  gsumply1eq  22270  mdetralt2  22570  mdetunilem2  22574  madugsum  22604  gsummatr01lem4  22619  cpmatmcllem  22679  cayleyhamilton1  22853  neiptopnei  23093  neiptopreu  23094  neitr  23141  fiuncmp  23365  iunconnlem  23388  iunconn  23389  2ndcdisj  23417  dissnlocfin  23490  elptr2  23535  ptbasfi  23542  ptcld  23574  ptcldmpt  23575  ptclsg  23576  ptcnplem  23582  ptcnp  23583  cnmpt11  23624  cnmpt21  23632  cnmptcom  23639  imasnopn  23651  imasncld  23652  imasncls  23653  xkocnv  23775  elmptrab  23788  isfildlem  23818  alexsubALTlem3  24010  cnextfvval  24026  utopsnneiplem  24208  isucn2  24239  cfilucfil  24520  blval2  24523  restmetu  24531  ovoliunlem3  25478  ovoliun  25479  ovoliun2  25480  ovoliunnul  25481  finiunmbl  25518  volfiniun  25521  iundisj  25522  iunmbl  25527  voliun  25528  iunmbl2  25531  mbfeqalem1  25615  mbfsup  25638  mbfinf  25639  mbflim  25642  itg2splitlem  25722  itg2split  25723  isibl2  25740  cbvitg  25750  itgeqa  25788  itgss3  25789  itgfsum  25801  itgabs  25809  itggt0  25818  itgcn  25819  limcmpt  25857  limciun  25868  dvmptfsum  25952  dvlipcn  25972  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  dvfsumrlim  26011  dvfsum2  26014  itgsubst  26029  coeeq2  26220  dgrle  26221  ulmss  26379  leibpi  26925  rlimcnp  26948  rlimcnp2  26949  o1cxp  26958  lgamgulmlem2  27013  lgamgulmlem6  27017  fsumdvdscom  27168  lgseisenlem2  27360  2sqmo  27421  2sqreulem4  27438  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  nosupbnd1  27699  nosupbnd2  27701  noinfbnd1  27714  noinfbnd2  27716  bdayiun  27928  bdaypw2n0bndlem  28476  istrkg2ld  28549  istrkg2ldOLD  28550  mpteleeOLD  28986  gropd  29122  grstructd  29123  clwwlknonclwlknonf1o  30455  dlwwlknondlwlknonf1o  30458  ex-natded9.26  30512  isch3  31335  atom1d  32447  chirred  32489  sbc2iedf  32557  rspc2daf  32558  19.9d2r  32562  opreu2reuALT  32569  mo5f  32581  reuxfrdf  32583  foresf1o  32597  elabreximdv  32604  iinabrex  32662  cbvdisjf  32664  disjorf  32672  disjabrex  32675  iundisjf  32682  disjunsn  32687  brabgaf  32702  ac6sf2  32718  dfimafnf  32732  2ndresdju  32745  fmptcof2  32753  acunirnmpt2  32756  acunirnmpt2f  32757  aciunf1lem  32758  aciunf1  32759  ofpreima  32761  funcnv5mpt  32763  funcnv4mpt  32764  fnpreimac  32766  f1od2  32815  fpwrelmap  32829  xrofsup  32864  iundisjfi  32893  nnindf  32917  nn0min  32918  fprodex01  32923  fsumiunle  32927  prodindf  32961  gsummpt2d  33149  gsummptf1od  33155  gsummptfsf1o  33160  gsumhashmul  33167  suppgsumssiun  33172  gsumwrd2dccat  33178  isarchiofld  33299  elrgspnsubrunlem2  33348  nsgmgc  33511  nsgqusf1olem1  33512  nsgqusf1olem3  33514  nsgqusf1o  33515  elrspunidl  33527  elrspunsn  33528  deg1prod  33682  ply1gsumz  33698  ig1pmindeg  33701  mplvrpmga  33728  psrgsum  33731  psrmonprod  33735  esplylem  33749  esplyfv1  33752  esplyfval1  33756  esplyfvaln  33757  esplyind  33758  vieta  33763  exsslsb  33780  ply1degltdimlem  33806  fedgmullem2  33814  evls1fldgencl  33854  irngnzply1  33875  extdgfialglem2  33877  ply1annidllem  33885  algextdeglem6  33906  constrfin  33930  reff  34023  locfinreflem  34024  cmpcref  34034  zarclsiin  34055  zarcls  34058  zarcmplem  34065  ordtconnlem1  34108  qqhval2  34166  esumeq12dva  34216  esumeq2dv  34222  esumrnmpt  34236  esumpad  34239  esumpad2  34240  esumadd  34241  gsumesum  34243  esumlub  34244  esumsnf  34248  esumpr  34250  esumrnmpt2  34252  esumfzf  34253  esumfsup  34254  esumpcvgval  34262  esumpmono  34263  esumcocn  34264  hasheuni  34269  esumcvg  34270  esumgect  34274  esum2dlem  34276  esum2d  34277  esumiun  34278  ldsysgenld  34344  sigapildsyslem  34345  sigapildsys  34346  ldgenpisyslem1  34347  fiunelros  34358  measvunilem  34396  measvunilem0  34397  measvuni  34398  measiun  34402  measinblem  34404  voliune  34413  volfiniune  34414  volmeas  34415  ddemeas  34420  oms0  34481  omssubadd  34484  carsgclctunlem1  34501  carsggect  34502  omsmeas  34507  eulerpartlemgvv  34560  dstrvprob  34656  ballotlemodife  34682  reprsuc  34799  reprdifc  34811  breprexplema  34814  breprexplemc  34816  circlemethhgt  34827  hgt750lemd  34832  bnj919  34950  bnj1146  34973  bnj1379  35012  bnj1385  35014  bnj1400  35017  bnj1534  35035  bnj1542  35039  bnj110  35040  bnj121  35052  bnj124  35053  bnj130  35056  bnj207  35063  bnj571  35088  bnj605  35089  bnj580  35095  bnj607  35098  bnj611  35100  bnj873  35106  bnj849  35107  bnj900  35111  bnj916  35115  bnj1000  35123  bnj964  35125  bnj981  35132  bnj985v  35135  bnj985  35136  bnj1014  35143  bnj1123  35168  bnj1128  35172  bnj1228  35193  bnj1204  35194  bnj1279  35200  bnj1307  35205  bnj1321  35209  bnj1388  35215  bnj1398  35216  bnj1408  35218  bnj1417  35223  bnj1444  35225  bnj1445  35226  bnj1446  35227  bnj1449  35230  bnj1467  35236  bnj1489  35238  bnj1312  35240  bnj1497  35242  bnj1518  35246  bnj1525  35251  bnj1529  35252  dvelimalcased  35257  dvelimexcased  35259  axsepg2  35265  axsepg2ALT  35266  fineqvrep  35298  onvf1odlem2  35326  cvmcov  35485  untsucf  35932  dfon2lem1  36003  dfon2lem3  36005  finminlem  36540  weiunpo  36687  weiunso  36688  weiunfr  36689  weiunse  36690  regsfromregtr  36696  regsfromsetind  36697  bj-nexdvt  36963  bj-cbvaldv  37074  bj-cbval2vv  37076  bj-cbvex2vv  37077  bj-cbvaldvav  37078  bj-cbvexdvav  37079  ax11-pm2  37111  bj-dvelimdv  37126  bj-nfeel2  37129  bj-ceqsalv  37169  bj-vtocl  37191  bj-inrab2  37203  currysetlem  37220  currysetlem1  37222  bj-axseprep  37349  bj-axreprepsep  37350  bj-opabco  37470  mptsnunlem  37620  exlimim  37624  exellim  37626  topdifinfindis  37628  topdifinffinlem  37629  icorempo  37633  isbasisrelowllem1  37637  isbasisrelowllem2  37638  relowlssretop  37645  finxpreclem2  37672  finxpreclem6  37678  fvineqsneu  37693  fvineqsneq  37694  wl-euequf  37858  wl-sb8eut  37862  wl-issetft  37866  phpreu  37884  matunitlindflem2  37897  ptrest  37899  ptrecube  37900  poimirlem2  37902  poimirlem23  37923  poimirlem24  37924  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  heicant  37935  mbfposadd  37947  itgabsnc  37969  itggt0cn  37970  ftc1anclem5  37977  upixp  38009  indexa  38013  indexdom  38014  filbcmb  38020  sdclem2  38022  sdclem1  38023  fdc1  38026  totbndbnd  38069  sbcalf  38394  sbcexf  38395  scottexf  38448  scott0f  38449  eqrelf  38538  ralrmo3  38644  disjqmap2  39106  fsumshftd  39357  riotasv2d  39362  riotasv2s  39363  riotasv3d  39365  glbconxN  39783  pmapglbx  40174  pmapglb2xN  40177  cdleme26ee  40765  cdleme31sn  40785  cdleme31sn1  40786  cdlemefr29exN  40807  cdlemefs32sn1aw  40819  cdleme43fsv1snlem  40825  cdleme41sn3a  40838  cdleme32fva  40842  cdleme32d  40849  cdleme32f  40851  cdleme40m  40872  cdleme40n  40873  cdleme42b  40883  cdlemk36  41318  cdlemk38  41320  cdlemkid  41341  cdlemk19x  41348  cdlemk11t  41351  dihvalcqpre  41640  mapdheq  42133  hdmap1eq  42206  hdmapval2lem  42236  lcmineqlem9  42436  lcmineqlem12  42439  aks4d1p1p2  42469  mndmolinv  42494  primrootsunit1  42496  primrootsunit  42497  primrootspoweq0  42505  aks6d1c1p5  42511  aks6d1c3  42522  aks6d1c4  42523  aks6d1c1rh  42524  aks6d1c2lem4  42526  aks6d1c2  42529  deg1gprod  42539  sticksstones1  42545  sticksstones11  42555  sticksstones16  42561  sticksstones22  42567  aks6d1c6lem2  42570  aks6d1c6isolem1  42573  aks6d1c6isolem2  42574  bcled  42577  bcle2d  42578  aks6d1c7lem3  42581  aks6d1c7  42583  rhmqusspan  42584  grpods  42593  unitscyglem1  42594  unitscyglem2  42595  unitscyglem3  42596  unitscyglem4  42597  unitscyglem5  42598  nfa1w  43062  mzpexpmpt  43131  eq0rabdioph  43162  rexrabdioph  43180  rexfrabdioph  43181  elnn0rabdioph  43189  dvdsrabdioph  43196  fphpd  43202  monotuz  43327  monotoddzz  43329  oddcomabszz  43330  setindtr  43410  dford4  43415  wdom2d2  43421  aomclem6  43445  aomclem8  43447  flcidc  43556  areaquad  43602  unielss  43604  onsucf1lem  43655  oaun3lem1  43760  nadd1suc  43778  rababg  43959  ss2iundv  44045  cbviuneq12dv  44047  gneispace  44519  mnringvald  44598  mnringmulrcld  44613  nfscott  44624  scottabf  44625  scottab  44626  mnuprdlem4  44660  ismnushort  44686  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  aaanv  44773  pm11.57  44774  pm11.58  44775  pm11.59  44776  pm11.71  44782  pm14.12  44806  ssralv2  44916  tratrb  44921  iunconnlem2  45319  modelaxreplem3  45365  modelaxrep  45366  permaxrep  45391  evth2f  45404  elunif  45405  fvelrnbf  45407  evthf  45416  fnchoice  45418  sumpair  45424  rfcnnnub  45425  refsum2cn  45427  uzwo4  45442  fiiuncl  45454  fiunicl  45456  elintdv  45468  ssd  45469  cbvmpo2  45485  cbvmpo1  45486  eliin2f  45492  eliuniin2  45508  cbvrabv2  45515  suprnmpt  45562  disjf1  45571  disjrnmpt2  45576  disjf1o  45579  disjinfi  45580  choicefi  45587  iunmapsn  45604  axccdom  45609  dmrelrnrel  45613  axccd  45616  fmptf  45626  rnmptlb  45630  rnmptbddlem  45631  rnmptbd2lem  45635  rnmptbdlem  45642  rnmptbd  45643  fmptff  45656  upbdrech  45696  ssfiunibd  45700  supxrgere  45721  iuneqfzuzlem  45722  supxrgelem  45725  supxrge  45726  suplesup  45727  infrpge  45739  xralrple2  45742  infxr  45754  infxrunb2  45755  infleinf  45759  xrralrecnnle  45770  xrralrecnnge  45777  supxrunb3  45786  supxrleubrnmpt  45793  infleinf2  45801  unb2ltle  45802  rexabslelem  45805  rexabsle  45806  allbutfiinf  45807  suprleubrnmpt  45809  infrnmptle  45810  infxrunb3rnmpt  45815  uzublem  45817  uzub  45818  supminfrnmpt  45832  infxrpnf  45833  supxrleubrnmptf  45838  infxrgelbrnmpt  45841  infrpgernmpt  45852  supminfxr2  45856  monoordxr  45869  monoord2xr  45871  caucvgbf  45876  cvgcaule  45878  rexanuz2nf  45879  iccshift  45907  iooshift  45911  iooiinicc  45931  iooiinioc  45945  fsummulc1f  45960  fsumnncl  45961  fsumf1of  45963  fsumiunss  45964  fsumreclf  45965  fsumlessf  45966  fsumsermpt  45968  fmul01  45969  fmuldfeqlem1  45971  fmuldfeq  45972  fmul01lt1lem1  45973  fmul01lt1lem2  45974  fmul01lt1  45975  fprodsplit1  45982  fprodexp  45983  fprodabs2  45984  mccllem  45986  mccl  45987  fprodcnlem  45988  fprodcn  45989  climexp  45994  climsuse  45997  climrecf  45998  climinff  46000  climaddf  46004  mullimc  46005  ellimcabssub0  46006  islptre  46008  climf  46011  mullimcf  46012  rexlim2d  46014  idlimc  46015  limcperiod  46017  limcrecl  46018  sumnnodd  46019  islpcn  46026  limsupre  46028  limcleqr  46031  neglimc  46034  addlimc  46035  0ellimcdiv  46036  limclner  46038  climsubmpt  46047  climreclf  46051  climf2  46053  fnlimcnv  46054  climeldmeqmpt  46055  clim2f2  46057  climfveqmpt  46058  fnlimfvre  46061  allbutfifvre  46062  climleltrp  46063  fnlimf  46065  fnlimabslt  46066  climfveqmpt3  46069  climeldmeqf  46070  limsupref  46072  limsupbnd1f  46073  climbddf  46074  climeqf  46075  climeldmeqmpt3  46076  limsuplesup  46086  limsuppnfd  46089  limsupub  46091  limsupres  46092  climinf2lem  46093  climinf2  46094  limsuppnf  46098  limsupubuzlem  46099  limsupubuz  46100  climinf2mpt  46101  climinfmpt  46102  climinf3  46103  limsupmnflem  46107  limsupmnf  46108  limsupequz  46110  limsupre2  46112  limsupmnfuzlem  46113  limsupmnfuz  46114  limsupequzmptf  46118  limsupre3lem  46119  limsupre3  46120  limsupre3uzlem  46122  limsupre3uz  46123  limsupreuz  46124  limsupvaluz2  46125  limsupreuzmpt  46126  supcnvlimsup  46127  climuzlem  46130  climuz  46131  climisp  46133  lmbr3  46134  climrescn  46135  climxrrelem  46136  climxrre  46137  liminfcl  46150  liminfval2  46155  limsup10exlem  46159  liminflelimsuplem  46162  limsupgtlem  46164  limsupgt  46165  climliminflimsupd  46188  liminfreuzlem  46189  liminfreuz  46190  liminfltlem  46191  liminflt  46192  limsupub2  46199  xlimpnfxnegmnf  46201  liminflbuz2  46202  liminfpnfuz  46203  liminflimsupxrre  46204  xlimmnfvlem1  46219  xlimmnfvlem2  46220  xlimmnfv  46221  xlimpnfvlem1  46223  xlimpnfvlem2  46224  xlimpnfv  46225  xlimmnf  46228  xlimpnf  46229  xlimmnfmpt  46230  xlimpnfmpt  46231  climxlim2lem  46232  dfxlim2  46235  cncfshift  46261  icccncfext  46274  cncficcgt0  46275  cncfiooicc  46281  cncfioobd  46284  fprodcncf  46287  fprodsubrecnncnvlem  46294  fprodaddrecnncnvlem  46296  dvmptmulf  46324  dvnmptdivc  46325  dvnmul  46330  dvmptfprodlem  46331  dvmptfprod  46332  dvnprodlem1  46333  dvnprodlem2  46334  iblsplitf  46357  iblspltprt  46360  itgioocnicc  46364  iblcncfioo  46365  itgspltprt  46366  itgperiod  46368  stoweidlem3  46390  stoweidlem14  46401  stoweidlem17  46404  stoweidlem19  46406  stoweidlem20  46407  stoweidlem26  46413  stoweidlem27  46414  stoweidlem28  46415  stoweidlem29  46416  stoweidlem31  46418  stoweidlem34  46421  stoweidlem35  46422  stoweidlem36  46423  stoweidlem39  46426  stoweidlem42  46429  stoweidlem43  46430  stoweidlem44  46431  stoweidlem46  46433  stoweidlem48  46435  stoweidlem49  46436  stoweidlem50  46437  stoweidlem51  46438  stoweidlem52  46439  stoweidlem53  46440  stoweidlem54  46441  stoweidlem56  46443  stoweidlem57  46444  stoweidlem59  46446  stoweidlem60  46447  stoweidlem61  46448  stoweidlem62  46449  stoweid  46450  wallispilem3  46454  stirlinglem13  46473  stirling  46476  fourierdlem16  46510  fourierdlem21  46515  fourierdlem22  46516  fourierdlem31  46525  fourierdlem39  46533  fourierdlem48  46541  fourierdlem51  46544  fourierdlem53  46546  fourierdlem68  46561  fourierdlem69  46562  fourierdlem71  46564  fourierdlem73  46566  fourierdlem77  46570  fourierdlem80  46573  fourierdlem81  46574  fourierdlem82  46575  fourierdlem83  46576  fourierdlem86  46579  fourierdlem87  46580  fourierdlem89  46582  fourierdlem91  46584  fourierdlem93  46586  fourierdlem94  46587  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem113  46606  elaa2  46621  etransclem18  46639  etransclem22  46643  etransclem23  46644  etransclem32  46653  etransclem35  46656  etransclem44  46665  etransclem46  46667  etransclem48  46669  rrndistlt  46677  ioorrnopnlem  46691  saliuncl  46710  saliincl  46714  intsaluni  46716  salexct  46721  subsaliuncl  46745  sge00  46763  sge0revalmpt  46765  sge0sn  46766  sge0f1o  46769  sge0gerp  46782  sge0pnffigt  46783  sge0lefi  46785  sge0ltfirp  46787  sge0resrnlem  46790  sge0resplit  46793  sge0lempt  46797  sge0iunmptlemfi  46800  sge0p1  46801  sge0iunmptlemre  46802  sge0fodjrnlem  46803  sge0iunmpt  46805  sge0rpcpnf  46808  sge0ltfirpmpt2  46813  sge0isum  46814  sge0xp  46816  sge0ad2en  46818  sge0isummpt2  46819  sge0xaddlem1  46820  sge0xaddlem2  46821  sge0xadd  46822  sge0pnffsumgt  46829  sge0gtfsumgt  46830  sge0uzfsumgt  46831  sge0seq  46833  sge0reuz  46834  sge0reuzb  46835  iundjiun  46847  meadjiunlem  46852  meadjiun  46853  ismeannd  46854  voliunsge0lem  46859  meaiuninclem  46867  meaiunincf  46870  meaiuninc3v  46871  meaiuninc3  46872  meaiininclem  46873  meaiininc  46874  meaiininc2  46875  caragenfiiuncl  46902  omeiunltfirp  46906  carageniuncllem1  46908  carageniuncllem2  46909  caratheodorylem2  46914  0ome  46916  isomenndlem  46917  hoicvrrex  46943  ovnsupge0  46944  ovnlecvr  46945  ovnlerp  46949  ovncvrrp  46951  ovn0lem  46952  ovnsubaddlem1  46957  ovnsubaddlem2  46958  hoidmvcl  46969  hsphoidmvle2  46972  hsphoidmvle  46973  hoidmvval0  46974  sge0hsphoire  46976  hoidmvval0b  46977  hoidmv1lelem1  46978  hoidmv1lelem2  46979  hoidmv1lelem3  46980  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem3  46984  hoidmvlelem4  46985  hoidmvlelem5  46986  hoidmvle  46987  ovnhoilem1  46988  ovnhoilem2  46989  ovnhoi  46990  ovnlecvr2  46997  hspdifhsp  47003  hoidifhspdmvle  47007  hoiqssbllem3  47011  hspmbllem1  47013  hspmbllem2  47014  opnvonmbllem1  47019  opnvonmbllem2  47020  ovnsubadd2lem  47032  ovolval5lem1  47039  ovnovollem1  47043  ovnovollem2  47044  hoimbl2  47052  vonhoire  47059  iinhoiicclem  47060  iinhoiicc  47061  iunhoiioolem  47062  iunhoiioo  47063  vonioolem1  47067  vonioolem2  47068  vonioo  47069  vonicclem1  47070  vonicclem2  47071  vonicc  47072  vonn0ioo2  47077  vonn0icc2  47079  vonct  47080  pimltmnf2f  47084  pimgtpnf2f  47092  salpreimagelt  47094  salpreimalegt  47096  pimltpnf2f  47099  pimgtmnf2  47101  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  preimageiingt  47107  preimaleiinlt  47108  salpreimagtge  47112  salpreimaltle  47113  salpreimalelt  47116  salpreimagtlt  47117  issmff  47121  sssmf  47125  mbfresmf  47126  cnfsmf  47127  incsmflem  47128  incsmf  47129  smfsssmf  47130  issmflelem  47131  issmfle  47132  smfconst  47136  issmfgtlem  47142  issmfgt  47143  smfpimltxrmptf  47145  smfmbfcex  47147  smfaddlem1  47150  smfaddlem2  47151  smfadd  47152  decsmflem  47153  decsmf  47154  smfpreimagtf  47155  issmfgelem  47156  issmfge  47157  smflimlem2  47159  smflimlem4  47161  smflim  47164  smfpimgtxr  47167  smfpimgtxrmptf  47171  smfpimioo  47174  smfresal  47175  smfrec  47176  smfres  47177  smfmullem2  47179  smfmullem4  47181  smfmul  47182  smfpimbor1lem2  47186  smf2id  47188  smfco  47189  smflim2  47193  smfpimcc  47195  smflimmpt  47197  smfsuplem1  47198  smfsuplem3  47200  smfsup  47201  smfsupmpt  47202  smfsupxr  47203  smfinflem  47204  smfinf  47205  smfinfmpt  47206  smflimsuplem3  47209  smflimsuplem4  47210  smflimsuplem5  47211  smflimsuplem7  47213  smflimsuplem8  47214  smflimsup  47215  smflimsupmpt  47216  smfliminflem  47217  smfliminf  47218  smfliminfmpt  47219  smfpimne2  47227  fsupdm  47229  smfsupdmmbllem  47231  smfsupdmmbl  47232  finfdm  47233  smfinfdmmbllem  47235  smfinfdmmbl  47236  or2expropbilem1  47421  or2expropbilem2  47422  or2expropbi  47423  cfsetsnfsetf  47447  cfsetsnfsetfo  47449  rexsb  47488  reuf1odnf  47496  2reu8i  47502  ffnafv  47560  tz6.12c-afv2  47631  f1oresf1o2  47680  iccelpart  47822  iccpartdisj  47826  dfich2  47847  ichbi12i  47849  ichnfimlem  47852  ich2exprop  47860  ichnreuop  47861  ichreuopeq  47862  sprsymrelfo  47886  reupr  47911  reuopreuprim  47915  mogoldbb  48174  2zrngagrp  48638  2zrngmmgm  48641  cbvmpox2  48725  ovmpordx  48729  1arymaptfo  49032  2arymaptfo  49043  mo0sn  49204  iinfssclem3  49444  iinfssc  49445  iinfsubc  49446  infsubc2  49449  iinfconstbas  49454  isthincd2lem1  49813  nfintd  50061  nfiund  50062  nfiundg  50063  iunord  50064  spcdvw  50067  nfsetrecs  50074  setrec1lem2  50076  setrec1  50079  setrec2fun  50080  pgindnf  50104  pgind  50105  aacllem  50189