Theorem nfv 1914

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

Syntax hints:  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfvd  1915  cbvaldw  2336  cbval2v  2341  dvelimhw  2343  pm11.53  2344  19.12vv  2345  eeanv  2347  eeeanv  2348  ee4anv  2349  sbnf2  2357  exsb  2358  2exsb  2359  sbbibvv  2361  cbvsbvf  2362  cleljustALT2  2364  spimv  2389  spimev  2391  chvarv  2395  cbvalv  2399  cbvexv  2400  cbvald  2406  cbvaldva  2408  cbvexdva  2409  cbval2  2410  axc16i  2435  dvelimnf  2452  sbel2x  2473  sbiedv  2503  2sbiev  2504  sbid2v  2508  sbhb  2520  2sb8e  2529  nfmod2  2552  nfmodv  2553  mof  2557  mo4f  2561  euf  2570  sb8eulem  2592  cbvmow  2597  sbmo  2608  moexexvw  2622  moexexv  2633  2mo  2642  2mosOLD  2644  2eu6  2651  axextmo  2706  nulmo  2707  abbib  2799  cleqh  2858  nfcv  2892  nfeqd  2903  nfeld  2904  nfabdw  2914  nfabd  2915  dvelimdc  2917  nfcvf  2919  cleqf  2921  r19.29af  3247  rexbidvALT  3253  rexbidvaALT  3254  2ralbida  3261  r19.12  3290  reean  3291  cbvrexsvw  3293  cbvralsvwOLD  3294  cbvralsvwOLDOLD  3295  cbvrexsvwOLD  3296  sbralieOLD  3330  cbvralf  3336  cbvralv  3340  cbvrexv  3341  cbvralsv  3342  cbvrexsv  3343  cbvrmow  3383  cbvreuwOLD  3389  cbvreu  3400  cbvrmov  3402  cbvreuv  3403  cbvrabwOLD  3445  cbvrab  3449  cbvexeqsetf  3465  ceqsex2  3504  vtocl2gaf  3548  vtocl2gafOLD  3549  vtocl3gaf  3550  vtocl3gafOLD  3551  spc2ed  3570  rspct  3577  rspc  3579  rspce  3580  eqvincf  3619  elrab3t  3661  ralab2  3671  rexab2  3673  mob2  3689  mob  3691  reu2  3699  rmo4f  3709  reu2eqd  3710  cdeqab1  3746  nfcdeq  3751  sbcco  3782  cbvsbcv  3792  elrabsf  3802  sbc2iegf  3831  reu8nf  3843  rmo2  3853  rmo3  3855  rmoanimALT  3861  nfcsb1d  3887  nfcsbd  3890  csbiebt  3894  csbie2t  3903  cbvrabcsfw  3906  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  cbvralv2  3911  cbvrexv2  3912  rspc2vd  3913  dfssf  3940  rabss3d  4047  eqrrabd  4052  uniiunlem  4053  ab0orv  4349  ab0orvALT  4350  sbcnestgw  4389  sbcnestg  4394  sbnfc2  4405  r19.3rzv  4465  r19.28zv  4467  r19.27zv  4472  2reu4lem  4488  nfifd  4521  reusngf  4641  reusng  4644  rexreusng  4646  reuprg0  4669  rabsnifsb  4689  euabsn  4693  nfunid  4880  eluniab  4888  nfint  4923  elintabOLD  4926  iuneqconst  4970  disjiun  5098  disjxun  5108  nfopabd  5178  cbvopab  5182  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  mpteq12da  5193  mpteq12f  5195  cbvmptf  5210  cbvmptfg  5211  axrep1  5238  axrep2  5240  axrep3  5241  axrep4OLD  5244  axrep5  5245  zfrepclf  5249  reusv2lem3  5358  reusv2lem4  5359  reusv2  5361  reusv3  5363  alxfr  5365  ralxfrALT  5373  axprlem3OLD  5386  axprlem4OLD  5387  axprlem5OLD  5388  copsex2t  5455  iunopeqop  5484  rexopabb  5491  opelopabaf  5507  nfso  5556  pofun  5567  isso2i  5586  nffr  5614  opeliunxp  5708  opeliun2xp  5709  opeliunxp2  5805  ralxpf  5813  dfdmf  5863  dfrnf  5917  elrnmpt1  5927  dfrel4  6167  reuop  6269  frpoinsg  6319  frpoins2g  6321  wfis2g  6331  nfiotadw  6470  nfiotad  6472  cbviotaw  6474  cbviota  6476  cbviotav  6477  sb8iota  6478  iota2d  6502  iota2  6503  dffun6f  6532  imadif  6603  funimaexgOLD  6607  isarep1  6609  isarep1OLD  6610  isarep2  6611  fv3  6879  tz6.12f  6887  tz6.12cOLD  6888  funimassd  6930  fvelimad  6931  feqmptdf  6934  fimarab  6938  opabiotafun  6944  funfv2f  6953  fvmptd  6978  fvmptd2f  6987  fvmptdv  6988  fvmptt  6991  fvopab5  7004  eqfnfv2f  7010  ralrnmptw  7069  ralrnmpt  7071  dffo3f  7081  f1ompt  7086  fompt  7093  ffnfv  7094  ffnfvf  7095  f1ossf1o  7103  fmptco  7104  elabrex  7219  elabrexg  7220  dff13f  7233  fsnex  7261  fliftfun  7290  cbvriotaw  7356  cbvriota  7360  cbvriotav  7361  riota2  7372  riotaeqimp  7373  riota5f  7375  oprabv  7452  nfoprab  7456  mpoeq123  7464  cbvoprab1  7479  cbvoprab2  7480  cbvoprab12  7481  cbvoprab3  7483  cbvmpox  7485  ralrnmpo  7531  ovmpodx  7543  ovmpodf  7548  ovmpodv  7549  ov3  7555  ovmpt3rab1  7650  ofrfval2  7677  onminex  7781  tfis  7834  tfis2  7836  tfisi  7838  tfinds  7839  tfindes  7842  findes  7879  fiun  7924  f1iun  7925  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfoprab4f  8038  fmpox  8049  offval22  8070  ovmptss  8075  ralxpes  8118  ralxp3  8120  ralxp3es  8121  frpoins3xpg  8122  frpoins3xp3g  8123  opeliunxp2f  8192  tposoprab  8244  fvmpocurryd  8253  nffrecs  8265  tfr3  8370  nfrdg  8385  tz7.48-1  8414  tz7.49  8416  naddsuc2  8668  eqerlem  8709  erovlem  8789  mptelixpg  8911  boxcutc  8917  dom2lem  8966  xpf1o  9109  mapxpen  9113  findcard2  9134  pssnn  9138  nneneq  9176  ac6sfi  9238  fiint  9284  fiintOLD  9285  indexfi  9318  wdom2d  9540  ixpiunwdom  9550  cantnflem1  9649  nfttrcld  9670  frinsg  9711  frins2  9714  r1val1  9746  rankuni2b  9813  scottexs  9847  scott0s  9848  dfac8clem  9992  acni2  10006  aceq1  10077  dfac5lem5  10087  kmlem15  10125  infpssrlem4  10266  fin23lem27  10288  hsmexlem2  10387  hsmexlem4  10389  axcc3  10398  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  ac6c4  10441  zorn2lem4  10459  zorn2lem5  10460  iunfo  10499  iundom2g  10500  uniimadomf  10505  konigthlem  10528  axrepndlem2  10553  axunnd  10556  axpowndlem2  10558  axpowndlem4  10560  axregndlem2  10563  axacndlem5  10571  zfcndrep  10574  zfcndinf  10578  pwfseqlem4a  10621  pwfseqlem4  10622  tskuni  10743  gruiin  10770  reclem2pr  11008  dedekind  11344  dedekindle  11345  fimaxre3  12136  nn0ind-raph  12641  uzind4s  12874  nnwof  12880  lbzbi  12902  fzrevral  13580  rabssnn0fi  13958  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0fiubex  13964  seqof2  14032  reuccatpfxs1  14719  cotr2g  14949  rlim2  15469  ello1mpt  15494  climeu  15528  o1compt  15560  summolem2a  15688  zsum  15691  sumss  15697  sumss2  15699  fsumcvg2  15700  fsumclf  15711  fsumsplitf  15715  fsumsplit1  15718  fsum2dlem  15743  fsum00  15771  o1fsum  15786  nfcprod1  15881  nfcprod  15882  prodmolem2a  15907  zprod  15910  fprod  15914  fprodntriv  15915  prodss  15920  fprodn0  15952  fprod2dlem  15953  fprodsplitf  15961  fprodsplit1f  15963  fprodle  15969  fprodmodd  15970  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  coprmprod  16638  coprmproddvdslem  16639  prmind2  16662  iserodd  16813  pcmpt  16870  pcmptdvds  16872  prmolefac  17024  mreexexd  17616  catpropd  17677  invfuc  17946  natpropd  17948  fucpropd  17949  initoeu2  17985  acsmapd  18520  symgval  19308  gsumsnd  19889  gsumsnf  19890  gsumunsnfd  19894  gsummptf1o  19900  gsummpt1n0  19902  gsum2d2lem  19910  gsumcom2  19912  gsummptnn0fz  19923  dprd2d2  19983  rngqiprngimf1  21217  gsummoncoe1  22202  gsumply1eq  22203  mdetralt2  22503  mdetunilem2  22507  madugsum  22537  gsummatr01lem4  22552  cpmatmcllem  22612  cayleyhamilton1  22786  neiptopnei  23026  neiptopreu  23027  neitr  23074  fiuncmp  23298  iunconnlem  23321  iunconn  23322  2ndcdisj  23350  dissnlocfin  23423  elptr2  23468  ptbasfi  23475  ptcld  23507  ptcldmpt  23508  ptclsg  23509  ptcnplem  23515  ptcnp  23516  cnmpt11  23557  cnmpt21  23565  cnmptcom  23572  imasnopn  23584  imasncld  23585  imasncls  23586  xkocnv  23708  elmptrab  23721  isfildlem  23751  alexsubALTlem3  23943  cnextfvval  23959  utopsnneiplem  24142  isucn2  24173  cfilucfil  24454  blval2  24457  restmetu  24465  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovoliunnul  25415  finiunmbl  25452  volfiniun  25455  iundisj  25456  iunmbl  25461  voliun  25462  iunmbl2  25465  mbfeqalem1  25549  mbfsup  25572  mbfinf  25573  mbflim  25576  itg2splitlem  25656  itg2split  25657  isibl2  25674  cbvitg  25684  itgeqa  25722  itgss3  25723  itgfsum  25735  itgabs  25743  itggt0  25752  itgcn  25753  limcmpt  25791  limciun  25802  dvmptfsum  25886  dvlipcn  25906  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem4  25943  dvfsumrlim  25945  dvfsum2  25948  itgsubst  25963  coeeq2  26154  dgrle  26155  ulmss  26313  leibpi  26859  rlimcnp  26882  rlimcnp2  26883  o1cxp  26892  lgamgulmlem2  26947  lgamgulmlem6  26951  fsumdvdscom  27102  lgseisenlem2  27294  2sqmo  27355  2sqreulem4  27372  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2  27650  istrkg2ld  28394  mptelee  28829  gropd  28965  grstructd  28966  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  ex-natded9.26  30355  isch3  31177  atom1d  32289  chirred  32331  sbc2iedf  32401  rspc2daf  32402  19.9d2r  32406  opreu2reuALT  32413  mo5f  32425  reuxfrdf  32427  foresf1o  32440  elabreximdv  32447  iinabrex  32505  cbvdisjf  32507  disjorf  32515  disjabrex  32518  iundisjf  32525  disjunsn  32530  brabgaf  32543  ac6sf2  32555  dfimafnf  32567  2ndresdju  32580  fmptcof2  32588  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1lem  32593  aciunf1  32594  ofpreima  32596  funcnv5mpt  32599  funcnv4mpt  32600  fnpreimac  32602  padct  32650  f1od2  32651  fpwrelmap  32663  xrofsup  32697  iundisjfi  32726  nnindf  32751  nn0min  32752  fprodex01  32757  fsumiunle  32761  prodindf  32793  gsummpt2d  32996  gsummptfsf1o  33001  gsumhashmul  33008  gsumwrd2dccat  33014  elrgspnsubrunlem2  33206  isarchiofld  33302  nsgmgc  33390  nsgqusf1olem1  33391  nsgqusf1olem3  33393  nsgqusf1o  33394  elrspunidl  33406  elrspunsn  33407  ply1gsumz  33571  ig1pmindeg  33574  exsslsb  33599  ply1degltdimlem  33625  fedgmullem2  33633  evls1fldgencl  33672  irngnzply1  33693  ply1annidllem  33698  algextdeglem6  33719  constrfin  33743  reff  33836  locfinreflem  33837  cmpcref  33847  zarclsiin  33868  zarcls  33871  zarcmplem  33878  ordtconnlem1  33921  qqhval2  33979  esumeq12dva  34029  esumeq2dv  34035  esumrnmpt  34049  esumpad  34052  esumpad2  34053  esumadd  34054  gsumesum  34056  esumlub  34057  esumsnf  34061  esumpr  34063  esumrnmpt2  34065  esumfzf  34066  esumfsup  34067  esumpcvgval  34075  esumpmono  34076  esumcocn  34077  hasheuni  34082  esumcvg  34083  esumgect  34087  esum2dlem  34089  esum2d  34090  esumiun  34091  ldsysgenld  34157  sigapildsyslem  34158  sigapildsys  34159  ldgenpisyslem1  34160  fiunelros  34171  measvunilem  34209  measvunilem0  34210  measvuni  34211  measiun  34215  measinblem  34217  voliune  34226  volfiniune  34227  volmeas  34228  ddemeas  34233  oms0  34295  omssubadd  34298  carsgclctunlem1  34315  carsggect  34316  omsmeas  34321  eulerpartlemgvv  34374  dstrvprob  34470  ballotlemodife  34496  reprsuc  34613  reprdifc  34625  breprexplema  34628  breprexplemc  34630  circlemethhgt  34641  hgt750lemd  34646  bnj919  34764  bnj1146  34788  bnj1379  34827  bnj1385  34829  bnj1400  34832  bnj1534  34850  bnj1542  34854  bnj110  34855  bnj121  34867  bnj124  34868  bnj130  34871  bnj207  34878  bnj571  34903  bnj605  34904  bnj580  34910  bnj607  34913  bnj611  34915  bnj873  34921  bnj849  34922  bnj900  34926  bnj916  34930  bnj1000  34938  bnj964  34940  bnj981  34947  bnj985v  34950  bnj985  34951  bnj1014  34958  bnj1123  34983  bnj1128  34987  bnj1228  35008  bnj1204  35009  bnj1279  35015  bnj1307  35020  bnj1321  35024  bnj1388  35030  bnj1398  35031  bnj1408  35033  bnj1417  35038  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1449  35045  bnj1467  35051  bnj1489  35053  bnj1312  35055  bnj1497  35057  bnj1518  35061  bnj1525  35066  bnj1529  35067  dvelimalcased  35072  dvelimexcased  35074  axsepg2  35079  axsepg2ALT  35080  fineqvrep  35092  onvf1odlem2  35098  cvmcov  35257  untsucf  35704  setinds2  35775  dfon2lem1  35778  dfon2lem3  35780  finminlem  36313  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  bj-nexdvt  36693  bj-cbvaldv  36794  bj-cbval2vv  36796  bj-cbvex2vv  36797  bj-cbvaldvav  36798  bj-cbvexdvav  36799  ax11-pm2  36831  bj-dvelimdv  36846  bj-nfeel2  36849  bj-ceqsalv  36889  bj-vtocl  36911  bj-inrab2  36923  currysetlem  36940  currysetlem1  36942  bj-opabco  37183  mptsnunlem  37333  exlimim  37337  exellim  37339  topdifinfindis  37341  topdifinffinlem  37342  icorempo  37346  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  finxpreclem2  37385  finxpreclem6  37391  fvineqsneu  37406  fvineqsneq  37407  wl-euequf  37569  wl-sb8eut  37573  wl-issetft  37577  phpreu  37605  matunitlindflem2  37618  ptrest  37620  ptrecube  37621  poimirlem2  37623  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  heicant  37656  mbfposadd  37668  itgabsnc  37690  itggt0cn  37691  ftc1anclem5  37698  upixp  37730  indexa  37734  indexdom  37735  filbcmb  37741  sdclem2  37743  sdclem1  37744  fdc1  37747  totbndbnd  37790  sbcalf  38115  sbcexf  38116  scottexf  38169  scott0f  38170  eqrelf  38251  fsumshftd  38952  riotasv2d  38957  riotasv2s  38958  riotasv3d  38960  glbconxN  39379  pmapglbx  39770  pmapglb2xN  39773  cdleme26ee  40361  cdleme31sn  40381  cdleme31sn1  40382  cdlemefr29exN  40403  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32fva  40438  cdleme32d  40445  cdleme32f  40447  cdleme40m  40468  cdleme40n  40469  cdleme42b  40479  cdlemk36  40914  cdlemk38  40916  cdlemkid  40937  cdlemk19x  40944  cdlemk11t  40947  dihvalcqpre  41236  mapdheq  41729  hdmap1eq  41802  hdmapval2lem  41832  lcmineqlem9  42032  lcmineqlem12  42035  aks4d1p1p2  42065  mndmolinv  42090  primrootsunit1  42092  primrootsunit  42093  primrootspoweq0  42101  aks6d1c1p5  42107  aks6d1c3  42118  aks6d1c4  42119  aks6d1c1rh  42120  aks6d1c2lem4  42122  aks6d1c2  42125  deg1gprod  42135  sticksstones1  42141  sticksstones11  42151  sticksstones16  42157  sticksstones22  42163  aks6d1c6lem2  42166  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  bcled  42173  bcle2d  42174  aks6d1c7lem3  42177  aks6d1c7  42179  rhmqusspan  42180  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  unitscyglem5  42194  nfa1w  42670  mzpexpmpt  42740  eq0rabdioph  42771  rexrabdioph  42789  rexfrabdioph  42790  elnn0rabdioph  42798  dvdsrabdioph  42805  fphpd  42811  monotuz  42937  monotoddzz  42939  oddcomabszz  42940  setindtr  43020  dford4  43025  wdom2d2  43031  aomclem6  43055  aomclem8  43057  flcidc  43166  areaquad  43212  unielss  43214  onsucf1lem  43265  oaun3lem1  43370  nadd1suc  43388  rababg  43570  ss2iundv  43656  cbviuneq12dv  43658  gneispace  44130  mnringvald  44209  mnringmulrcld  44224  nfscott  44235  scottabf  44236  scottab  44237  mnuprdlem4  44271  ismnushort  44297  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  aaanv  44384  pm11.57  44385  pm11.58  44386  pm11.59  44387  pm11.71  44393  pm14.12  44417  ssralv2  44528  tratrb  44533  iunconnlem2  44931  modelaxreplem3  44977  modelaxrep  44978  permaxrep  45003  evth2f  45016  elunif  45017  fvelrnbf  45019  evthf  45028  fnchoice  45030  sumpair  45036  rfcnnnub  45037  refsum2cn  45039  uzwo4  45054  fiiuncl  45066  fiunicl  45068  elintdv  45080  ssd  45081  cbvmpo2  45098  cbvmpo1  45099  eliin2f  45105  eliuniin2  45121  cbvrabv2  45128  suprnmpt  45175  disjf1  45184  disjrnmpt2  45189  disjf1o  45192  disjinfi  45193  choicefi  45201  iunmapsn  45218  axccdom  45223  dmrelrnrel  45227  axccd  45230  fmptf  45240  rnmptlb  45244  rnmptbddlem  45245  rnmptbd2lem  45249  rnmptbdlem  45256  rnmptbd  45257  fmptff  45270  upbdrech  45310  ssfiunibd  45314  supxrgere  45336  iuneqfzuzlem  45337  supxrgelem  45340  supxrge  45341  suplesup  45342  infrpge  45354  xralrple2  45357  infxr  45370  infxrunb2  45371  infleinf  45375  xrralrecnnle  45386  xrralrecnnge  45393  supxrunb3  45402  supxrleubrnmpt  45409  infleinf2  45417  unb2ltle  45418  rexabslelem  45421  rexabsle  45422  allbutfiinf  45423  suprleubrnmpt  45425  infrnmptle  45426  infxrunb3rnmpt  45431  uzublem  45433  uzub  45434  supminfrnmpt  45448  infxrpnf  45449  supxrleubrnmptf  45454  infxrgelbrnmpt  45457  infrpgernmpt  45468  supminfxr2  45472  monoordxr  45485  monoord2xr  45487  caucvgbf  45492  cvgcaule  45494  rexanuz2nf  45495  iccshift  45523  iooshift  45527  iooiinicc  45547  iooiinioc  45561  fsummulc1f  45576  fsumnncl  45577  fsumf1of  45579  fsumiunss  45580  fsumreclf  45581  fsumlessf  45582  fsumsermpt  45584  fmul01  45585  fmuldfeqlem1  45587  fmuldfeq  45588  fmul01lt1lem1  45589  fmul01lt1lem2  45590  fmul01lt1  45591  fprodsplit1  45598  fprodexp  45599  fprodabs2  45600  mccllem  45602  mccl  45603  fprodcnlem  45604  fprodcn  45605  climexp  45610  climsuse  45613  climrecf  45614  climinff  45616  climaddf  45620  mullimc  45621  ellimcabssub0  45622  islptre  45624  climf  45627  mullimcf  45628  rexlim2d  45630  idlimc  45631  limcperiod  45633  limcrecl  45634  sumnnodd  45635  islpcn  45644  limsupre  45646  limcleqr  45649  neglimc  45652  addlimc  45653  0ellimcdiv  45654  limclner  45656  climsubmpt  45665  climreclf  45669  climf2  45671  fnlimcnv  45672  climeldmeqmpt  45673  clim2f2  45675  climfveqmpt  45676  fnlimfvre  45679  allbutfifvre  45680  climleltrp  45681  fnlimf  45683  fnlimabslt  45684  climfveqmpt3  45687  climeldmeqf  45688  limsupref  45690  limsupbnd1f  45691  climbddf  45692  climeqf  45693  climeldmeqmpt3  45694  limsuplesup  45704  limsuppnfd  45707  limsupub  45709  limsupres  45710  climinf2lem  45711  climinf2  45712  limsuppnf  45716  limsupubuzlem  45717  limsupubuz  45718  climinf2mpt  45719  climinfmpt  45720  climinf3  45721  limsupmnflem  45725  limsupmnf  45726  limsupequz  45728  limsupre2  45730  limsupmnfuzlem  45731  limsupmnfuz  45732  limsupequzmptf  45736  limsupre3lem  45737  limsupre3  45738  limsupre3uzlem  45740  limsupre3uz  45741  limsupreuz  45742  limsupvaluz2  45743  limsupreuzmpt  45744  supcnvlimsup  45745  climuzlem  45748  climuz  45749  climisp  45751  lmbr3  45752  climrescn  45753  climxrrelem  45754  climxrre  45755  liminfcl  45768  liminfval2  45773  limsup10exlem  45777  liminflelimsuplem  45780  limsupgtlem  45782  limsupgt  45783  climliminflimsupd  45806  liminfreuzlem  45807  liminfreuz  45808  liminfltlem  45809  liminflt  45810  limsupub2  45817  xlimpnfxnegmnf  45819  liminflbuz2  45820  liminfpnfuz  45821  liminflimsupxrre  45822  xlimmnfvlem1  45837  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem1  45841  xlimpnfvlem2  45842  xlimpnfv  45843  xlimmnf  45846  xlimpnf  45847  xlimmnfmpt  45848  xlimpnfmpt  45849  climxlim2lem  45850  dfxlim2  45853  cncfshift  45879  icccncfext  45892  cncficcgt0  45893  cncfiooicc  45899  cncfioobd  45902  fprodcncf  45905  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvmptmulf  45942  dvnmptdivc  45943  dvnmul  45948  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  iblsplitf  45975  iblspltprt  45978  itgioocnicc  45982  iblcncfioo  45983  itgspltprt  45984  itgperiod  45986  stoweidlem3  46008  stoweidlem14  46019  stoweidlem17  46022  stoweidlem19  46024  stoweidlem20  46025  stoweidlem26  46031  stoweidlem27  46032  stoweidlem28  46033  stoweidlem29  46034  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem36  46041  stoweidlem39  46044  stoweidlem42  46047  stoweidlem43  46048  stoweidlem44  46049  stoweidlem46  46051  stoweidlem48  46053  stoweidlem49  46054  stoweidlem50  46055  stoweidlem51  46056  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem56  46061  stoweidlem57  46062  stoweidlem59  46064  stoweidlem60  46065  stoweidlem61  46066  stoweidlem62  46067  stoweid  46068  wallispilem3  46072  stirlinglem13  46091  stirling  46094  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem31  46143  fourierdlem39  46151  fourierdlem48  46159  fourierdlem51  46162  fourierdlem53  46164  fourierdlem68  46179  fourierdlem69  46180  fourierdlem71  46182  fourierdlem73  46184  fourierdlem77  46188  fourierdlem80  46191  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem86  46197  fourierdlem87  46198  fourierdlem89  46200  fourierdlem91  46202  fourierdlem93  46204  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  elaa2  46239  etransclem18  46257  etransclem22  46261  etransclem23  46262  etransclem32  46271  etransclem35  46274  etransclem44  46283  etransclem46  46285  etransclem48  46287  rrndistlt  46295  ioorrnopnlem  46309  saliuncl  46328  saliincl  46332  intsaluni  46334  salexct  46339  subsaliuncl  46363  sge00  46381  sge0revalmpt  46383  sge0sn  46384  sge0f1o  46387  sge0gerp  46400  sge0pnffigt  46401  sge0lefi  46403  sge0ltfirp  46405  sge0resrnlem  46408  sge0resplit  46411  sge0lempt  46415  sge0iunmptlemfi  46418  sge0p1  46419  sge0iunmptlemre  46420  sge0fodjrnlem  46421  sge0iunmpt  46423  sge0rpcpnf  46426  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xp  46434  sge0ad2en  46436  sge0isummpt2  46437  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0xadd  46440  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  sge0reuzb  46453  iundjiun  46465  meadjiunlem  46470  meadjiun  46471  ismeannd  46472  voliunsge0lem  46477  meaiuninclem  46485  meaiunincf  46488  meaiuninc3v  46489  meaiuninc3  46490  meaiininclem  46491  meaiininc  46492  meaiininc2  46493  caragenfiiuncl  46520  omeiunltfirp  46524  carageniuncllem1  46526  carageniuncllem2  46527  caratheodorylem2  46532  0ome  46534  isomenndlem  46535  hoicvrrex  46561  ovnsupge0  46562  ovnlecvr  46563  ovnlerp  46567  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  ovnsubaddlem2  46576  hoidmvcl  46587  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmvval0  46592  sge0hsphoire  46594  hoidmvval0b  46595  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem1  46606  ovnhoilem2  46607  ovnhoi  46608  ovnlecvr2  46615  hspdifhsp  46621  hoidifhspdmvle  46625  hoiqssbllem3  46629  hspmbllem1  46631  hspmbllem2  46632  opnvonmbllem1  46637  opnvonmbllem2  46638  ovnsubadd2lem  46650  ovolval5lem1  46657  ovnovollem1  46661  ovnovollem2  46662  hoimbl2  46670  vonhoire  46677  iinhoiicclem  46678  iinhoiicc  46679  iunhoiioolem  46680  iunhoiioo  46681  vonioolem1  46685  vonioolem2  46686  vonioo  46687  vonicclem1  46688  vonicclem2  46689  vonicc  46690  vonn0ioo2  46695  vonn0icc2  46697  vonct  46698  pimltmnf2f  46702  pimgtpnf2f  46710  salpreimagelt  46712  salpreimalegt  46714  pimltpnf2f  46717  pimgtmnf2  46719  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  preimageiingt  46725  preimaleiinlt  46726  salpreimagtge  46730  salpreimaltle  46731  salpreimalelt  46734  salpreimagtlt  46735  issmff  46739  sssmf  46743  mbfresmf  46744  cnfsmf  46745  incsmflem  46746  incsmf  46747  smfsssmf  46748  issmflelem  46749  issmfle  46750  smfconst  46754  issmfgtlem  46760  issmfgt  46761  smfpimltxrmptf  46763  smfmbfcex  46765  smfaddlem1  46768  smfaddlem2  46769  smfadd  46770  decsmflem  46771  decsmf  46772  smfpreimagtf  46773  issmfgelem  46774  issmfge  46775  smflimlem2  46777  smflimlem4  46779  smflim  46782  smfpimgtxr  46785  smfpimgtxrmptf  46789  smfpimioo  46792  smfresal  46793  smfrec  46794  smfres  46795  smfmullem2  46797  smfmullem4  46799  smfmul  46800  smfpimbor1lem2  46804  smf2id  46806  smfco  46807  smflim2  46811  smfpimcc  46813  smflimmpt  46815  smfsuplem1  46816  smfsuplem3  46818  smfsup  46819  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinf  46823  smfinfmpt  46824  smflimsuplem3  46827  smflimsuplem4  46828  smflimsuplem5  46829  smflimsuplem7  46831  smflimsuplem8  46832  smflimsup  46833  smflimsupmpt  46834  smfliminflem  46835  smfliminf  46836  smfliminfmpt  46837  smfpimne2  46845  fsupdm  46847  smfsupdmmbllem  46849  smfsupdmmbl  46850  finfdm  46851  smfinfdmmbllem  46853  smfinfdmmbl  46854  or2expropbilem1  47037  or2expropbilem2  47038  or2expropbi  47039  cfsetsnfsetf  47063  cfsetsnfsetfo  47065  rexsb  47104  reuf1odnf  47112  2reu8i  47118  ffnafv  47176  tz6.12c-afv2  47247  f1oresf1o2  47296  iccelpart  47438  iccpartdisj  47442  dfich2  47463  ichbi12i  47465  ichnfimlem  47468  ich2exprop  47476  ichnreuop  47477  ichreuopeq  47478  sprsymrelfo  47502  reupr  47527  reuopreuprim  47531  mogoldbb  47790  2zrngagrp  48241  2zrngmmgm  48244  cbvmpox2  48328  ovmpordx  48332  1arymaptfo  48636  2arymaptfo  48647  mo0sn  48808  iinfssclem3  49049  iinfssc  49050  iinfsubc  49051  infsubc2  49054  iinfconstbas  49059  isthincd2lem1  49418  nfintd  49666  nfiund  49667  nfiundg  49668  iunord  49669  spcdvw  49672  nfsetrecs  49679  setrec1lem2  49681  setrec1  49684  setrec2fun  49685  pgindnf  49709  pgind  49710  aacllem  49794