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  sbralieOLD  3318  cbvralf  3323  cbvralv  3327  cbvrexv  3328  cbvralsv  3329  cbvrexsv  3330  cbvrmow  3368  cbvreu  3382  cbvrmov  3384  cbvreuv  3385  cbvrabwOLD  3426  cbvrab  3429  cbvexeqsetf  3445  ceqsex2  3482  vtocl2gaf  3523  vtocl2gafOLD  3524  vtocl3gaf  3525  vtocl3gafOLD  3526  spc2ed  3544  rspct  3551  rspc  3553  rspce  3554  eqvincf  3593  elrab3t  3634  ralab2  3644  rexab2  3646  mob2  3662  mob  3664  reu2  3672  rmo4f  3682  reu2eqd  3683  cdeqab1  3719  nfcdeq  3724  sbcco  3755  cbvsbcv  3765  elrabsf  3775  sbc2iegf  3804  reu8nf  3816  rmo2  3826  rmo3  3828  rmoanimALT  3834  nfcsb1d  3860  nfcsbd  3863  csbiebt  3867  csbie2t  3876  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  cbvralv2  3884  cbvrexv2  3885  rspc2vd  3886  dfssf  3913  rabss3d  4022  eqrrabd  4027  uniiunlem  4028  ab0orv  4324  ab0orvALT  4325  sbcnestgw  4364  sbcnestg  4369  sbnfc2  4380  r19.3rzvOLD  4445  r19.28zv  4447  r19.27zv  4452  2reu4lem  4464  nfifd  4497  reusngf  4619  reusng  4622  rexreusng  4624  reuprg0  4647  rabsnifsb  4667  euabsn  4671  nfunid  4857  eluniab  4865  nfint  4900  iuneqconst  4946  disjiun  5074  disjxun  5084  nfopabd  5154  cbvopab  5158  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  mpteq12da  5169  mpteq12f  5171  cbvmptf  5186  cbvmptfg  5187  axrep1  5214  axrep2  5216  axrep3  5217  axrep4OLD  5220  axrep5  5221  zfrepclf  5227  reusv2lem3  5339  reusv2lem4  5340  reusv2  5342  reusv3  5344  alxfr  5346  ralxfrALT  5354  axprlem3OLD  5368  axprlem4OLD  5369  axprlem5OLD  5370  copsex2t  5442  iunopeqop  5471  rexopabb  5478  opelopabaf  5494  nfso  5541  pofun  5552  isso2i  5571  nffr  5599  opeliunxp  5693  opeliun2xp  5694  opeliunxp2  5789  ralxpf  5797  dfdmf  5847  dfrnf  5901  elrnmpt1  5911  dfrel4  6151  reuop  6253  frpoinsg  6303  frpoins2g  6305  wfis2g  6315  nfiotadw  6453  nfiotad  6455  cbviotaw  6457  cbviota  6459  cbviotav  6460  sb8iota  6461  iota2d  6482  iota2  6483  dffun6f  6509  imadif  6578  isarep1  6583  isarep2  6584  fv3  6854  tz6.12f  6861  funimassd  6902  fvelimad  6903  feqmptdf  6906  fimarab  6910  opabiotafun  6916  funfv2f  6925  fvmptd  6951  fvmptd2f  6960  fvmptdv  6961  fvmptt  6964  fvopab5  6977  eqfnfv2f  6983  ralrnmptw  7042  ralrnmpt  7044  dffo3f  7054  f1ompt  7059  fompt  7066  ffnfv  7067  ffnfvf  7068  f1ossf1o  7077  fmptco  7078  elabrex  7192  elabrexg  7193  dff13f  7205  fsnex  7233  fliftfun  7262  cbvriotaw  7328  cbvriota  7332  cbvriotav  7333  riota2  7344  riotaeqimp  7345  riota5f  7347  oprabv  7422  nfoprab  7426  mpoeq123  7434  cbvoprab1  7449  cbvoprab2  7450  cbvoprab12  7451  cbvoprab3  7453  cbvmpox  7455  ralrnmpo  7501  ovmpodx  7513  ovmpodf  7518  ovmpodv  7519  ov3  7525  ovmpt3rab1  7620  ofrfval2  7647  onminex  7751  tfis  7801  tfis2  7803  tfisi  7805  tfinds  7806  tfindes  7809  findes  7846  fiun  7891  f1iun  7892  abrexex2g  7912  opabex3d  7913  opabex3rd  7914  opabex3  7915  dfoprab4f  8004  fmpox  8015  offval22  8033  ovmptss  8038  ralxpes  8081  ralxp3  8083  ralxp3es  8084  frpoins3xpg  8085  frpoins3xp3g  8086  opeliunxp2f  8155  tposoprab  8207  fvmpocurryd  8216  nffrecs  8228  tfr3  8333  nfrdg  8348  tz7.48-1  8377  tz7.49  8379  naddsuc2  8632  eqerlem  8674  erovlem  8755  mptelixpg  8878  boxcutc  8884  dom2lem  8934  xpf1o  9072  mapxpen  9076  findcard2  9094  pssnn  9098  nneneq  9135  ac6sfi  9189  fiint  9232  indexfi  9265  wdom2d  9490  ixpiunwdom  9500  cantnflem1  9605  nfttrcld  9626  setinds2  9667  frinsg  9670  frins2  9673  r1val1  9705  rankuni2b  9772  scottexs  9806  scott0s  9807  dfac8clem  9949  acni2  9963  aceq1  10034  dfac5lem5  10044  kmlem15  10082  infpssrlem4  10223  fin23lem27  10245  hsmexlem2  10344  hsmexlem4  10346  axcc3  10355  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  axdc4lem  10372  ac6c4  10398  zorn2lem4  10416  zorn2lem5  10417  iunfo  10456  iundom2g  10457  uniimadomf  10462  konigthlem  10486  axrepndlem2  10511  axunnd  10514  axpowndlem2  10516  axpowndlem4  10518  axregndlem2  10521  axacndlem5  10529  zfcndrep  10532  zfcndinf  10536  pwfseqlem4a  10579  pwfseqlem4  10580  tskuni  10701  gruiin  10728  reclem2pr  10966  dedekind  11304  dedekindle  11305  fimaxre3  12097  nn0ind-raph  12624  uzind4s  12853  nnwof  12859  lbzbi  12881  fzrevral  13561  rabssnn0fi  13943  fsuppmapnn0fiublem  13947  fsuppmapnn0fiub  13948  fsuppmapnn0fiubex  13949  seqof2  14017  reuccatpfxs1  14704  cotr2g  14933  rlim2  15453  ello1mpt  15478  climeu  15512  o1compt  15544  summolem2a  15672  zsum  15675  sumss  15681  sumss2  15683  fsumcvg2  15684  fsumclf  15695  fsumsplitf  15699  fsumsplit1  15702  fsum2dlem  15727  fsum00  15756  o1fsum  15771  nfcprod1  15868  nfcprod  15869  prodmolem2a  15894  zprod  15897  fprod  15901  fprodntriv  15902  prodss  15907  fprodn0  15939  fprod2dlem  15940  fprodsplitf  15948  fprodsplit1f  15950  fprodle  15956  fprodmodd  15957  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2  16604  coprmprod  16625  coprmproddvdslem  16626  prmind2  16649  iserodd  16801  pcmpt  16858  pcmptdvds  16860  prmolefac  17012  mreexexd  17609  catpropd  17670  invfuc  17939  natpropd  17941  fucpropd  17942  initoeu2  17978  acsmapd  18515  nfchnd  18572  symgval  19341  gsumsnd  19922  gsumsnf  19923  gsumunsnfd  19927  gsummptf1o  19933  gsummpt1n0  19935  gsum2d2lem  19943  gsumcom2  19945  gsummptnn0fz  19956  dprd2d2  20016  rngqiprngimf1  21294  gsummoncoe1  22287  gsumply1eq  22288  mdetralt2  22588  mdetunilem2  22592  madugsum  22622  gsummatr01lem4  22637  cpmatmcllem  22697  cayleyhamilton1  22871  neiptopnei  23111  neiptopreu  23112  neitr  23159  fiuncmp  23383  iunconnlem  23406  iunconn  23407  2ndcdisj  23435  dissnlocfin  23508  elptr2  23553  ptbasfi  23560  ptcld  23592  ptcldmpt  23593  ptclsg  23594  ptcnplem  23600  ptcnp  23601  cnmpt11  23642  cnmpt21  23650  cnmptcom  23657  imasnopn  23669  imasncld  23670  imasncls  23671  xkocnv  23793  elmptrab  23806  isfildlem  23836  alexsubALTlem3  24028  cnextfvval  24044  utopsnneiplem  24226  isucn2  24257  cfilucfil  24538  blval2  24541  restmetu  24549  ovoliunlem3  25485  ovoliun  25486  ovoliun2  25487  ovoliunnul  25488  finiunmbl  25525  volfiniun  25528  iundisj  25529  iunmbl  25534  voliun  25535  iunmbl2  25538  mbfeqalem1  25622  mbfsup  25645  mbfinf  25646  mbflim  25649  itg2splitlem  25729  itg2split  25730  isibl2  25747  cbvitg  25757  itgeqa  25795  itgss3  25796  itgfsum  25808  itgabs  25816  itggt0  25825  itgcn  25826  limcmpt  25864  limciun  25875  dvmptfsum  25956  dvlipcn  25975  dvfsumlem2  26008  dvfsumlem4  26010  dvfsumrlim  26012  dvfsum2  26015  itgsubst  26030  coeeq2  26221  dgrle  26222  ulmss  26379  leibpi  26923  rlimcnp  26946  rlimcnp2  26947  o1cxp  26956  lgamgulmlem2  27011  lgamgulmlem6  27015  fsumdvdscom  27166  lgseisenlem2  27357  2sqmo  27418  2sqreulem4  27435  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  nosupbnd1  27696  nosupbnd2  27698  noinfbnd1  27711  noinfbnd2  27713  bdayiun  27925  bdaypw2n0bndlem  28473  istrkg2ld  28546  mpteleeOLD  28982  gropd  29118  grstructd  29119  clwwlknonclwlknonf1o  30451  dlwwlknondlwlknonf1o  30454  ex-natded9.26  30508  isch3  31331  atom1d  32443  chirred  32485  sbc2iedf  32553  rspc2daf  32554  19.9d2r  32558  opreu2reuALT  32565  mo5f  32577  reuxfrdf  32579  foresf1o  32593  elabreximdv  32600  iinabrex  32658  cbvdisjf  32660  disjorf  32668  disjabrex  32671  iundisjf  32678  disjunsn  32683  brabgaf  32698  ac6sf2  32714  dfimafnf  32728  2ndresdju  32741  fmptcof2  32749  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1lem  32754  aciunf1  32755  ofpreima  32757  funcnv5mpt  32759  funcnv4mpt  32760  fnpreimac  32762  f1od2  32811  fpwrelmap  32825  xrofsup  32859  iundisjfi  32888  nnindf  32912  nn0min  32913  fprodex01  32917  fsumiunle  32921  prodindf  32941  gsummpt2d  33129  gsummptf1od  33135  gsummptfsf1o  33140  gsumhashmul  33147  suppgsumssiun  33152  gsumwrd2dccat  33158  isarchiofld  33279  elrgspnsubrunlem2  33328  nsgmgc  33491  nsgqusf1olem1  33492  nsgqusf1olem3  33494  nsgqusf1o  33495  elrspunidl  33507  elrspunsn  33508  deg1prod  33662  ply1gsumz  33678  ig1pmindeg  33681  mplvrpmga  33708  psrgsum  33711  psrmonprod  33715  esplylem  33729  esplyfv1  33732  esplyfval1  33736  esplyfvaln  33737  esplyind  33738  vieta  33743  exsslsb  33760  ply1degltdimlem  33786  fedgmullem2  33794  evls1fldgencl  33834  irngnzply1  33855  extdgfialglem2  33857  ply1annidllem  33865  algextdeglem6  33886  constrfin  33910  reff  34003  locfinreflem  34004  cmpcref  34014  zarclsiin  34035  zarcls  34038  zarcmplem  34045  ordtconnlem1  34088  qqhval2  34146  esumeq12dva  34196  esumeq2dv  34202  esumrnmpt  34216  esumpad  34219  esumpad2  34220  esumadd  34221  gsumesum  34223  esumlub  34224  esumsnf  34228  esumpr  34230  esumrnmpt2  34232  esumfzf  34233  esumfsup  34234  esumpcvgval  34242  esumpmono  34243  esumcocn  34244  hasheuni  34249  esumcvg  34250  esumgect  34254  esum2dlem  34256  esum2d  34257  esumiun  34258  ldsysgenld  34324  sigapildsyslem  34325  sigapildsys  34326  ldgenpisyslem1  34327  fiunelros  34338  measvunilem  34376  measvunilem0  34377  measvuni  34378  measiun  34382  measinblem  34384  voliune  34393  volfiniune  34394  volmeas  34395  ddemeas  34400  oms0  34461  omssubadd  34464  carsgclctunlem1  34481  carsggect  34482  omsmeas  34487  eulerpartlemgvv  34540  dstrvprob  34636  ballotlemodife  34662  reprsuc  34779  reprdifc  34791  breprexplema  34794  breprexplemc  34796  circlemethhgt  34807  hgt750lemd  34812  bnj919  34930  bnj1146  34953  bnj1379  34992  bnj1385  34994  bnj1400  34997  bnj1534  35015  bnj1542  35019  bnj110  35020  bnj121  35032  bnj124  35033  bnj130  35036  bnj207  35043  bnj571  35068  bnj605  35069  bnj580  35075  bnj607  35078  bnj611  35080  bnj873  35086  bnj849  35087  bnj900  35091  bnj916  35095  bnj1000  35103  bnj964  35105  bnj981  35112  bnj985v  35115  bnj985  35116  bnj1014  35123  bnj1123  35148  bnj1128  35152  bnj1228  35173  bnj1204  35174  bnj1279  35180  bnj1307  35185  bnj1321  35189  bnj1388  35195  bnj1398  35196  bnj1408  35198  bnj1417  35203  bnj1444  35205  bnj1445  35206  bnj1446  35207  bnj1449  35210  bnj1467  35216  bnj1489  35218  bnj1312  35220  bnj1497  35222  bnj1518  35226  bnj1525  35231  bnj1529  35232  dvelimalcased  35237  dvelimexcased  35239  axsepg2  35245  axsepg2ALT  35246  fineqvrep  35278  onvf1odlem2  35306  cvmcov  35465  untsucf  35912  dfon2lem1  35983  dfon2lem3  35985  finminlem  36520  weiunpo  36667  weiunso  36668  weiunfr  36669  weiunse  36670  axtcond  36680  regsfromregtco  36740  regsfromsetind  36741  bj-nexdvt  37015  bj-cbvaldv  37126  bj-cbval2vv  37128  bj-cbvex2vv  37129  bj-cbvaldvav  37130  bj-cbvexdvav  37131  ax11-pm2  37163  bj-dvelimdv  37178  bj-nfeel2  37181  bj-ceqsalv  37221  bj-vtocl  37243  bj-inrab2  37255  currysetlem  37272  currysetlem1  37274  bj-axseprep  37401  bj-axreprepsep  37402  bj-opabco  37522  mptsnunlem  37672  exlimim  37676  exellim  37678  topdifinfindis  37680  topdifinffinlem  37681  icorempo  37685  isbasisrelowllem1  37689  isbasisrelowllem2  37690  relowlssretop  37697  finxpreclem2  37724  finxpreclem6  37730  fvineqsneu  37745  fvineqsneq  37746  wl-euequf  37917  wl-sb8eut  37921  wl-issetft  37925  phpreu  37943  matunitlindflem2  37956  ptrest  37958  ptrecube  37959  poimirlem2  37961  poimirlem23  37982  poimirlem24  37983  poimirlem25  37984  poimirlem26  37985  poimirlem27  37986  poimirlem28  37987  heicant  37994  mbfposadd  38006  itgabsnc  38028  itggt0cn  38029  ftc1anclem5  38036  upixp  38068  indexa  38072  indexdom  38073  filbcmb  38079  sdclem2  38081  sdclem1  38082  fdc1  38085  totbndbnd  38128  sbcalf  38453  sbcexf  38454  scottexf  38507  scott0f  38508  eqrelf  38597  ralrmo3  38703  disjqmap2  39165  fsumshftd  39416  riotasv2d  39421  riotasv2s  39422  riotasv3d  39424  glbconxN  39842  pmapglbx  40233  pmapglb2xN  40236  cdleme26ee  40824  cdleme31sn  40844  cdleme31sn1  40845  cdlemefr29exN  40866  cdlemefs32sn1aw  40878  cdleme43fsv1snlem  40884  cdleme41sn3a  40897  cdleme32fva  40901  cdleme32d  40908  cdleme32f  40910  cdleme40m  40931  cdleme40n  40932  cdleme42b  40942  cdlemk36  41377  cdlemk38  41379  cdlemkid  41400  cdlemk19x  41407  cdlemk11t  41410  dihvalcqpre  41699  mapdheq  42192  hdmap1eq  42265  hdmapval2lem  42295  lcmineqlem9  42494  lcmineqlem12  42497  aks4d1p1p2  42527  mndmolinv  42552  primrootsunit1  42554  primrootsunit  42555  primrootspoweq0  42563  aks6d1c1p5  42569  aks6d1c3  42580  aks6d1c4  42581  aks6d1c1rh  42582  aks6d1c2lem4  42584  aks6d1c2  42587  deg1gprod  42597  sticksstones1  42603  sticksstones11  42613  sticksstones16  42619  sticksstones22  42625  aks6d1c6lem2  42628  aks6d1c6isolem1  42631  aks6d1c6isolem2  42632  bcled  42635  bcle2d  42636  aks6d1c7lem3  42639  aks6d1c7  42641  rhmqusspan  42642  grpods  42651  unitscyglem1  42652  unitscyglem2  42653  unitscyglem3  42654  unitscyglem4  42655  unitscyglem5  42656  nfa1w  43126  mzpexpmpt  43195  eq0rabdioph  43226  rexrabdioph  43244  rexfrabdioph  43245  elnn0rabdioph  43253  dvdsrabdioph  43260  fphpd  43266  monotuz  43391  monotoddzz  43393  oddcomabszz  43394  setindtr  43474  dford4  43479  wdom2d2  43485  aomclem6  43509  aomclem8  43511  flcidc  43620  areaquad  43666  unielss  43668  onsucf1lem  43719  oaun3lem1  43824  nadd1suc  43842  rababg  44023  ss2iundv  44109  cbviuneq12dv  44111  gneispace  44583  mnringvald  44662  mnringmulrcld  44677  nfscott  44688  scottabf  44689  scottab  44690  mnuprdlem4  44724  ismnushort  44750  binomcxplemdvsum  44804  binomcxplemnotnn0  44805  aaanv  44837  pm11.57  44838  pm11.58  44839  pm11.59  44840  pm11.71  44846  pm14.12  44870  ssralv2  44980  tratrb  44985  iunconnlem2  45383  modelaxreplem3  45429  modelaxrep  45430  permaxrep  45455  evth2f  45468  elunif  45469  fvelrnbf  45471  evthf  45480  fnchoice  45482  sumpair  45488  rfcnnnub  45489  refsum2cn  45491  uzwo4  45506  fiiuncl  45518  fiunicl  45520  elintdv  45532  ssd  45533  cbvmpo2  45549  cbvmpo1  45550  eliin2f  45556  eliuniin2  45572  cbvrabv2  45579  suprnmpt  45626  disjf1  45635  disjrnmpt2  45640  disjf1o  45643  disjinfi  45644  choicefi  45651  iunmapsn  45668  axccdom  45673  dmrelrnrel  45677  axccd  45680  fmptf  45690  rnmptlb  45694  rnmptbddlem  45695  rnmptbd2lem  45699  rnmptbdlem  45706  rnmptbd  45707  fmptff  45720  upbdrech  45760  ssfiunibd  45764  supxrgere  45785  iuneqfzuzlem  45786  supxrgelem  45789  supxrge  45790  suplesup  45791  infrpge  45803  xralrple2  45806  infxr  45818  infxrunb2  45819  infleinf  45823  xrralrecnnle  45834  xrralrecnnge  45841  supxrunb3  45850  supxrleubrnmpt  45856  infleinf2  45864  unb2ltle  45865  rexabslelem  45868  rexabsle  45869  allbutfiinf  45870  suprleubrnmpt  45872  infrnmptle  45873  infxrunb3rnmpt  45878  uzublem  45880  uzub  45881  supminfrnmpt  45895  infxrpnf  45896  supxrleubrnmptf  45901  infxrgelbrnmpt  45904  infrpgernmpt  45915  supminfxr2  45919  monoordxr  45932  monoord2xr  45934  caucvgbf  45939  cvgcaule  45941  rexanuz2nf  45942  iccshift  45970  iooshift  45974  iooiinicc  45994  iooiinioc  46008  fsummulc1f  46023  fsumnncl  46024  fsumf1of  46026  fsumiunss  46027  fsumreclf  46028  fsumlessf  46029  fsumsermpt  46031  fmul01  46032  fmuldfeqlem1  46034  fmuldfeq  46035  fmul01lt1lem1  46036  fmul01lt1lem2  46037  fmul01lt1  46038  fprodsplit1  46045  fprodexp  46046  fprodabs2  46047  mccllem  46049  mccl  46050  fprodcnlem  46051  fprodcn  46052  climexp  46057  climsuse  46060  climrecf  46061  climinff  46063  climaddf  46067  mullimc  46068  ellimcabssub0  46069  islptre  46071  climf  46074  mullimcf  46075  rexlim2d  46077  idlimc  46078  limcperiod  46080  limcrecl  46081  sumnnodd  46082  islpcn  46089  limsupre  46091  limcleqr  46094  neglimc  46097  addlimc  46098  0ellimcdiv  46099  limclner  46101  climsubmpt  46110  climreclf  46114  climf2  46116  fnlimcnv  46117  climeldmeqmpt  46118  clim2f2  46120  climfveqmpt  46121  fnlimfvre  46124  allbutfifvre  46125  climleltrp  46126  fnlimf  46128  fnlimabslt  46129  climfveqmpt3  46132  climeldmeqf  46133  limsupref  46135  limsupbnd1f  46136  climbddf  46137  climeqf  46138  climeldmeqmpt3  46139  limsuplesup  46149  limsuppnfd  46152  limsupub  46154  limsupres  46155  climinf2lem  46156  climinf2  46157  limsuppnf  46161  limsupubuzlem  46162  limsupubuz  46163  climinf2mpt  46164  climinfmpt  46165  climinf3  46166  limsupmnflem  46170  limsupmnf  46171  limsupequz  46173  limsupre2  46175  limsupmnfuzlem  46176  limsupmnfuz  46177  limsupequzmptf  46181  limsupre3lem  46182  limsupre3  46183  limsupre3uzlem  46185  limsupre3uz  46186  limsupreuz  46187  limsupvaluz2  46188  limsupreuzmpt  46189  supcnvlimsup  46190  climuzlem  46193  climuz  46194  climisp  46196  lmbr3  46197  climrescn  46198  climxrrelem  46199  climxrre  46200  liminfcl  46213  liminfval2  46218  limsup10exlem  46222  liminflelimsuplem  46225  limsupgtlem  46227  limsupgt  46228  climliminflimsupd  46251  liminfreuzlem  46252  liminfreuz  46253  liminfltlem  46254  liminflt  46255  limsupub2  46262  xlimpnfxnegmnf  46264  liminflbuz2  46265  liminfpnfuz  46266  liminflimsupxrre  46267  xlimmnfvlem1  46282  xlimmnfvlem2  46283  xlimmnfv  46284  xlimpnfvlem1  46286  xlimpnfvlem2  46287  xlimpnfv  46288  xlimmnf  46291  xlimpnf  46292  xlimmnfmpt  46293  xlimpnfmpt  46294  climxlim2lem  46295  dfxlim2  46298  cncfshift  46324  icccncfext  46337  cncficcgt0  46338  cncfiooicc  46344  cncfioobd  46347  fprodcncf  46350  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  dvmptmulf  46387  dvnmptdivc  46388  dvnmul  46393  dvmptfprodlem  46394  dvmptfprod  46395  dvnprodlem1  46396  dvnprodlem2  46397  iblsplitf  46420  iblspltprt  46423  itgioocnicc  46427  iblcncfioo  46428  itgspltprt  46429  itgperiod  46431  stoweidlem3  46453  stoweidlem14  46464  stoweidlem17  46467  stoweidlem19  46469  stoweidlem20  46470  stoweidlem26  46476  stoweidlem27  46477  stoweidlem28  46478  stoweidlem29  46479  stoweidlem31  46481  stoweidlem34  46484  stoweidlem35  46485  stoweidlem36  46486  stoweidlem39  46489  stoweidlem42  46492  stoweidlem43  46493  stoweidlem44  46494  stoweidlem46  46496  stoweidlem48  46498  stoweidlem49  46499  stoweidlem50  46500  stoweidlem51  46501  stoweidlem52  46502  stoweidlem53  46503  stoweidlem54  46504  stoweidlem56  46506  stoweidlem57  46507  stoweidlem59  46509  stoweidlem60  46510  stoweidlem61  46511  stoweidlem62  46512  stoweid  46513  wallispilem3  46517  stirlinglem13  46536  stirling  46539  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem31  46588  fourierdlem39  46596  fourierdlem48  46604  fourierdlem51  46607  fourierdlem53  46609  fourierdlem68  46624  fourierdlem69  46625  fourierdlem71  46627  fourierdlem73  46629  fourierdlem77  46633  fourierdlem80  46636  fourierdlem81  46637  fourierdlem82  46638  fourierdlem83  46639  fourierdlem86  46642  fourierdlem87  46643  fourierdlem89  46645  fourierdlem91  46647  fourierdlem93  46649  fourierdlem94  46650  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  elaa2  46684  etransclem18  46702  etransclem22  46706  etransclem23  46707  etransclem32  46716  etransclem35  46719  etransclem44  46728  etransclem46  46730  etransclem48  46732  rrndistlt  46740  ioorrnopnlem  46754  saliuncl  46773  saliincl  46777  intsaluni  46779  salexct  46784  subsaliuncl  46808  sge00  46826  sge0revalmpt  46828  sge0sn  46829  sge0f1o  46832  sge0gerp  46845  sge0pnffigt  46846  sge0lefi  46848  sge0ltfirp  46850  sge0resrnlem  46853  sge0resplit  46856  sge0lempt  46860  sge0iunmptlemfi  46863  sge0p1  46864  sge0iunmptlemre  46865  sge0fodjrnlem  46866  sge0iunmpt  46868  sge0rpcpnf  46871  sge0ltfirpmpt2  46876  sge0isum  46877  sge0xp  46879  sge0ad2en  46881  sge0isummpt2  46882  sge0xaddlem1  46883  sge0xaddlem2  46884  sge0xadd  46885  sge0pnffsumgt  46892  sge0gtfsumgt  46893  sge0uzfsumgt  46894  sge0seq  46896  sge0reuz  46897  sge0reuzb  46898  iundjiun  46910  meadjiunlem  46915  meadjiun  46916  ismeannd  46917  voliunsge0lem  46922  meaiuninclem  46930  meaiunincf  46933  meaiuninc3v  46934  meaiuninc3  46935  meaiininclem  46936  meaiininc  46937  meaiininc2  46938  caragenfiiuncl  46965  omeiunltfirp  46969  carageniuncllem1  46971  carageniuncllem2  46972  caratheodorylem2  46977  0ome  46979  isomenndlem  46980  hoicvrrex  47006  ovnsupge0  47007  ovnlecvr  47008  ovnlerp  47012  ovncvrrp  47014  ovn0lem  47015  ovnsubaddlem1  47020  ovnsubaddlem2  47021  hoidmvcl  47032  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmvval0  47037  sge0hsphoire  47039  hoidmvval0b  47040  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoidmvlelem5  47049  hoidmvle  47050  ovnhoilem1  47051  ovnhoilem2  47052  ovnhoi  47053  ovnlecvr2  47060  hspdifhsp  47066  hoidifhspdmvle  47070  hoiqssbllem3  47074  hspmbllem1  47076  hspmbllem2  47077  opnvonmbllem1  47082  opnvonmbllem2  47083  ovnsubadd2lem  47095  ovolval5lem1  47102  ovnovollem1  47106  ovnovollem2  47107  hoimbl2  47115  vonhoire  47122  iinhoiicclem  47123  iinhoiicc  47124  iunhoiioolem  47125  iunhoiioo  47126  vonioolem1  47130  vonioolem2  47131  vonioo  47132  vonicclem1  47133  vonicclem2  47134  vonicc  47135  vonn0ioo2  47140  vonn0icc2  47142  vonct  47143  pimltmnf2f  47147  pimgtpnf2f  47155  salpreimagelt  47157  salpreimalegt  47159  pimltpnf2f  47162  pimgtmnf2  47164  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  preimageiingt  47170  preimaleiinlt  47171  salpreimagtge  47175  salpreimaltle  47176  salpreimalelt  47179  salpreimagtlt  47180  issmff  47184  sssmf  47188  mbfresmf  47189  cnfsmf  47190  incsmflem  47191  incsmf  47192  smfsssmf  47193  issmflelem  47194  issmfle  47195  smfconst  47199  issmfgtlem  47205  issmfgt  47206  smfpimltxrmptf  47208  smfmbfcex  47210  smfaddlem1  47213  smfaddlem2  47214  smfadd  47215  decsmflem  47216  decsmf  47217  smfpreimagtf  47218  issmfgelem  47219  issmfge  47220  smflimlem2  47222  smflimlem4  47224  smflim  47227  smfpimgtxr  47230  smfpimgtxrmptf  47234  smfpimioo  47237  smfresal  47238  smfrec  47239  smfres  47240  smfmullem2  47242  smfmullem4  47244  smfmul  47245  smfpimbor1lem2  47249  smf2id  47251  smfco  47252  smflim2  47256  smfpimcc  47258  smflimmpt  47260  smfsuplem1  47261  smfsuplem3  47263  smfsup  47264  smfsupmpt  47265  smfsupxr  47266  smfinflem  47267  smfinf  47268  smfinfmpt  47269  smflimsuplem3  47272  smflimsuplem4  47273  smflimsuplem5  47274  smflimsuplem7  47276  smflimsuplem8  47277  smflimsup  47278  smflimsupmpt  47279  smfliminflem  47280  smfliminf  47281  smfliminfmpt  47282  smfpimne2  47290  fsupdm  47292  smfsupdmmbllem  47294  smfsupdmmbl  47295  finfdm  47296  smfinfdmmbllem  47298  smfinfdmmbl  47299  or2expropbilem1  47496  or2expropbilem2  47497  or2expropbi  47498  cfsetsnfsetf  47522  cfsetsnfsetfo  47524  rexsb  47563  reuf1odnf  47571  2reu8i  47577  ffnafv  47635  tz6.12c-afv2  47706  f1oresf1o2  47755  iccelpart  47909  iccpartdisj  47913  dfich2  47934  ichbi12i  47936  ichnfimlem  47939  ich2exprop  47947  ichnreuop  47948  ichreuopeq  47949  sprsymrelfo  47973  reupr  47998  reuopreuprim  48002  mogoldbb  48277  2zrngagrp  48741  2zrngmmgm  48744  cbvmpox2  48828  ovmpordx  48832  1arymaptfo  49135  2arymaptfo  49146  mo0sn  49307  iinfssclem3  49547  iinfssc  49548  iinfsubc  49549  infsubc2  49552  iinfconstbas  49557  isthincd2lem1  49916  nfintd  50164  nfiund  50165  nfiundg  50166  iunord  50167  spcdvw  50170  nfsetrecs  50177  setrec1lem2  50179  setrec1  50182  setrec2fun  50183  pgindnf  50207  pgind  50208  aacllem  50292