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  2356  exsb  2357  2exsb  2358  sbbibvv  2360  cbvsbvf  2361  cleljustALT2  2363  spimv  2388  spimev  2390  chvarv  2394  cbvalv  2398  cbvexv  2399  cbvald  2405  cbvaldva  2407  cbvexdva  2408  cbval2  2409  axc16i  2434  dvelimnf  2451  sbel2x  2472  sbiedv  2502  2sbiev  2503  sbid2v  2507  sbhb  2519  2sb8e  2528  nfmod2  2551  nfmodv  2552  mof  2556  mo4f  2560  euf  2569  sb8eulem  2591  cbvmow  2596  sbmo  2607  moexexvw  2621  moexexv  2632  2mo  2641  2mosOLD  2643  2eu6  2650  axextmo  2705  nulmo  2706  abbib  2798  cleqh  2857  nfcv  2891  nfeqd  2902  nfeld  2903  nfabdw  2913  nfabd  2914  dvelimdc  2916  nfcvf  2918  cleqf  2920  r19.29af  3238  rexbidvALT  3244  rexbidvaALT  3245  2ralbida  3252  r19.12  3278  reean  3279  cbvrexsvw  3281  cbvralsvwOLD  3282  cbvralsvwOLDOLD  3283  cbvrexsvwOLD  3284  sbralieOLD  3317  cbvralf  3323  cbvralv  3327  cbvrexv  3328  cbvralsv  3329  cbvrexsv  3330  cbvrmow  3370  cbvreu  3386  cbvrmov  3388  cbvreuv  3389  cbvrabwOLD  3431  cbvrab  3435  cbvexeqsetf  3451  ceqsex2  3490  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  spc2ed  3556  rspct  3563  rspc  3565  rspce  3566  eqvincf  3605  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  4032  eqrrabd  4037  uniiunlem  4038  ab0orv  4334  ab0orvALT  4335  sbcnestgw  4374  sbcnestg  4379  sbnfc2  4390  r19.3rzv  4450  r19.28zv  4452  r19.27zv  4457  2reu4lem  4473  nfifd  4506  reusngf  4626  reusng  4629  rexreusng  4631  reuprg0  4654  rabsnifsb  4674  euabsn  4678  nfunid  4864  eluniab  4872  nfint  4906  elintabOLD  4909  iuneqconst  4953  disjiun  5080  disjxun  5090  nfopabd  5160  cbvopab  5164  cbvopab1  5166  cbvopab1g  5167  cbvopab2  5168  cbvopab1s  5169  mpteq12da  5175  mpteq12f  5177  cbvmptf  5192  cbvmptfg  5193  axrep1  5219  axrep2  5221  axrep3  5222  axrep4OLD  5225  axrep5  5226  zfrepclf  5230  reusv2lem3  5339  reusv2lem4  5340  reusv2  5342  reusv3  5344  alxfr  5346  ralxfrALT  5354  axprlem3OLD  5367  axprlem4OLD  5368  axprlem5OLD  5369  copsex2t  5435  iunopeqop  5464  rexopabb  5471  opelopabaf  5487  nfso  5534  pofun  5545  isso2i  5564  nffr  5592  opeliunxp  5686  opeliun2xp  5687  opeliunxp2  5781  ralxpf  5789  dfdmf  5839  dfrnf  5892  elrnmpt1  5902  dfrel4  6140  reuop  6241  frpoinsg  6291  frpoins2g  6293  wfis2g  6303  nfiotadw  6441  nfiotad  6443  cbviotaw  6445  cbviota  6447  cbviotav  6448  sb8iota  6449  iota2d  6470  iota2  6471  dffun6f  6497  imadif  6566  isarep1  6571  isarep2  6572  fv3  6840  tz6.12f  6847  funimassd  6889  fvelimad  6890  feqmptdf  6893  fimarab  6897  opabiotafun  6903  funfv2f  6912  fvmptd  6937  fvmptd2f  6946  fvmptdv  6947  fvmptt  6950  fvopab5  6963  eqfnfv2f  6969  ralrnmptw  7028  ralrnmpt  7030  dffo3f  7040  f1ompt  7045  fompt  7052  ffnfv  7053  ffnfvf  7054  f1ossf1o  7062  fmptco  7063  elabrex  7178  elabrexg  7179  dff13f  7192  fsnex  7220  fliftfun  7249  cbvriotaw  7315  cbvriota  7319  cbvriotav  7320  riota2  7331  riotaeqimp  7332  riota5f  7334  oprabv  7409  nfoprab  7413  mpoeq123  7421  cbvoprab1  7436  cbvoprab2  7437  cbvoprab12  7438  cbvoprab3  7440  cbvmpox  7442  ralrnmpo  7488  ovmpodx  7500  ovmpodf  7505  ovmpodv  7506  ov3  7512  ovmpt3rab1  7607  ofrfval2  7634  onminex  7738  tfis  7788  tfis2  7790  tfisi  7792  tfinds  7793  tfindes  7796  findes  7833  fiun  7878  f1iun  7879  abrexex2g  7899  opabex3d  7900  opabex3rd  7901  opabex3  7902  dfoprab4f  7991  fmpox  8002  offval22  8021  ovmptss  8026  ralxpes  8069  ralxp3  8071  ralxp3es  8072  frpoins3xpg  8073  frpoins3xp3g  8074  opeliunxp2f  8143  tposoprab  8195  fvmpocurryd  8204  nffrecs  8216  tfr3  8321  nfrdg  8336  tz7.48-1  8365  tz7.49  8367  naddsuc2  8619  eqerlem  8660  erovlem  8740  mptelixpg  8862  boxcutc  8868  dom2lem  8917  xpf1o  9056  mapxpen  9060  findcard2  9078  pssnn  9082  nneneq  9120  ac6sfi  9173  fiint  9216  fiintOLD  9217  indexfi  9250  wdom2d  9472  ixpiunwdom  9482  cantnflem1  9585  nfttrcld  9606  frinsg  9647  frins2  9650  r1val1  9682  rankuni2b  9749  scottexs  9783  scott0s  9784  dfac8clem  9926  acni2  9940  aceq1  10011  dfac5lem5  10021  kmlem15  10059  infpssrlem4  10200  fin23lem27  10222  hsmexlem2  10321  hsmexlem4  10323  axcc3  10332  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  ac6c4  10375  zorn2lem4  10393  zorn2lem5  10394  iunfo  10433  iundom2g  10434  uniimadomf  10439  konigthlem  10462  axrepndlem2  10487  axunnd  10490  axpowndlem2  10492  axpowndlem4  10494  axregndlem2  10497  axacndlem5  10505  zfcndrep  10508  zfcndinf  10512  pwfseqlem4a  10555  pwfseqlem4  10556  tskuni  10677  gruiin  10704  reclem2pr  10942  dedekind  11279  dedekindle  11280  fimaxre3  12071  nn0ind-raph  12576  uzind4s  12809  nnwof  12815  lbzbi  12837  fzrevral  13515  rabssnn0fi  13893  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fsuppmapnn0fiubex  13899  seqof2  13967  reuccatpfxs1  14653  cotr2g  14883  rlim2  15403  ello1mpt  15428  climeu  15462  o1compt  15494  summolem2a  15622  zsum  15625  sumss  15631  sumss2  15633  fsumcvg2  15634  fsumclf  15645  fsumsplitf  15649  fsumsplit1  15652  fsum2dlem  15677  fsum00  15705  o1fsum  15720  nfcprod1  15815  nfcprod  15816  prodmolem2a  15841  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  fprodn0  15886  fprod2dlem  15887  fprodsplitf  15895  fprodsplit1f  15897  fprodle  15903  fprodmodd  15904  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  coprmprod  16572  coprmproddvdslem  16573  prmind2  16596  iserodd  16747  pcmpt  16804  pcmptdvds  16806  prmolefac  16958  mreexexd  17554  catpropd  17615  invfuc  17884  natpropd  17886  fucpropd  17887  initoeu2  17923  acsmapd  18460  symgval  19250  gsumsnd  19831  gsumsnf  19832  gsumunsnfd  19836  gsummptf1o  19842  gsummpt1n0  19844  gsum2d2lem  19852  gsumcom2  19854  gsummptnn0fz  19865  dprd2d2  19925  rngqiprngimf1  21207  gsummoncoe1  22193  gsumply1eq  22194  mdetralt2  22494  mdetunilem2  22498  madugsum  22528  gsummatr01lem4  22543  cpmatmcllem  22603  cayleyhamilton1  22777  neiptopnei  23017  neiptopreu  23018  neitr  23065  fiuncmp  23289  iunconnlem  23312  iunconn  23313  2ndcdisj  23341  dissnlocfin  23414  elptr2  23459  ptbasfi  23466  ptcld  23498  ptcldmpt  23499  ptclsg  23500  ptcnplem  23506  ptcnp  23507  cnmpt11  23548  cnmpt21  23556  cnmptcom  23563  imasnopn  23575  imasncld  23576  imasncls  23577  xkocnv  23699  elmptrab  23712  isfildlem  23742  alexsubALTlem3  23934  cnextfvval  23950  utopsnneiplem  24133  isucn2  24164  cfilucfil  24445  blval2  24448  restmetu  24456  ovoliunlem3  25403  ovoliun  25404  ovoliun2  25405  ovoliunnul  25406  finiunmbl  25443  volfiniun  25446  iundisj  25447  iunmbl  25452  voliun  25453  iunmbl2  25456  mbfeqalem1  25540  mbfsup  25563  mbfinf  25564  mbflim  25567  itg2splitlem  25647  itg2split  25648  isibl2  25665  cbvitg  25675  itgeqa  25713  itgss3  25714  itgfsum  25726  itgabs  25734  itggt0  25743  itgcn  25744  limcmpt  25782  limciun  25793  dvmptfsum  25877  dvlipcn  25897  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  dvfsumrlim  25936  dvfsum2  25939  itgsubst  25954  coeeq2  26145  dgrle  26146  ulmss  26304  leibpi  26850  rlimcnp  26873  rlimcnp2  26874  o1cxp  26883  lgamgulmlem2  26938  lgamgulmlem6  26942  fsumdvdscom  27093  lgseisenlem2  27285  2sqmo  27346  2sqreulem4  27363  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  nosupbnd1  27624  nosupbnd2  27626  noinfbnd1  27639  noinfbnd2  27641  bdayiun  27829  istrkg2ld  28405  mptelee  28840  gropd  28976  grstructd  28977  clwwlknonclwlknonf1o  30306  dlwwlknondlwlknonf1o  30309  ex-natded9.26  30363  isch3  31185  atom1d  32297  chirred  32339  sbc2iedf  32409  rspc2daf  32410  19.9d2r  32414  opreu2reuALT  32421  mo5f  32433  reuxfrdf  32435  foresf1o  32448  elabreximdv  32455  iinabrex  32513  cbvdisjf  32515  disjorf  32523  disjabrex  32526  iundisjf  32533  disjunsn  32538  brabgaf  32553  ac6sf2  32566  dfimafnf  32579  2ndresdju  32592  fmptcof2  32600  acunirnmpt2  32603  acunirnmpt2f  32604  aciunf1lem  32605  aciunf1  32606  ofpreima  32608  funcnv5mpt  32611  funcnv4mpt  32612  fnpreimac  32614  padct  32662  f1od2  32663  fpwrelmap  32676  xrofsup  32710  iundisjfi  32739  nnindf  32764  nn0min  32765  fprodex01  32770  fsumiunle  32774  prodindf  32806  gsummpt2d  33002  gsummptfsf1o  33007  gsumhashmul  33014  gsumwrd2dccat  33020  isarchiofld  33141  elrgspnsubrunlem2  33188  nsgmgc  33349  nsgqusf1olem1  33350  nsgqusf1olem3  33352  nsgqusf1o  33353  elrspunidl  33365  elrspunsn  33366  ply1gsumz  33531  ig1pmindeg  33534  mplvrpmga  33546  exsslsb  33563  ply1degltdimlem  33589  fedgmullem2  33597  evls1fldgencl  33637  irngnzply1  33658  extdgfialglem2  33660  ply1annidllem  33668  algextdeglem6  33689  constrfin  33713  reff  33806  locfinreflem  33807  cmpcref  33817  zarclsiin  33838  zarcls  33841  zarcmplem  33848  ordtconnlem1  33891  qqhval2  33949  esumeq12dva  33999  esumeq2dv  34005  esumrnmpt  34019  esumpad  34022  esumpad2  34023  esumadd  34024  gsumesum  34026  esumlub  34027  esumsnf  34031  esumpr  34033  esumrnmpt2  34035  esumfzf  34036  esumfsup  34037  esumpcvgval  34045  esumpmono  34046  esumcocn  34047  hasheuni  34052  esumcvg  34053  esumgect  34057  esum2dlem  34059  esum2d  34060  esumiun  34061  ldsysgenld  34127  sigapildsyslem  34128  sigapildsys  34129  ldgenpisyslem1  34130  fiunelros  34141  measvunilem  34179  measvunilem0  34180  measvuni  34181  measiun  34185  measinblem  34187  voliune  34196  volfiniune  34197  volmeas  34198  ddemeas  34203  oms0  34265  omssubadd  34268  carsgclctunlem1  34285  carsggect  34286  omsmeas  34291  eulerpartlemgvv  34344  dstrvprob  34440  ballotlemodife  34466  reprsuc  34583  reprdifc  34595  breprexplema  34598  breprexplemc  34600  circlemethhgt  34611  hgt750lemd  34616  bnj919  34734  bnj1146  34758  bnj1379  34797  bnj1385  34799  bnj1400  34802  bnj1534  34820  bnj1542  34824  bnj110  34825  bnj121  34837  bnj124  34838  bnj130  34841  bnj207  34848  bnj571  34873  bnj605  34874  bnj580  34880  bnj607  34883  bnj611  34885  bnj873  34891  bnj849  34892  bnj900  34896  bnj916  34900  bnj1000  34908  bnj964  34910  bnj981  34917  bnj985v  34920  bnj985  34921  bnj1014  34928  bnj1123  34953  bnj1128  34957  bnj1228  34978  bnj1204  34979  bnj1279  34985  bnj1307  34990  bnj1321  34994  bnj1388  35000  bnj1398  35001  bnj1408  35003  bnj1417  35008  bnj1444  35010  bnj1445  35011  bnj1446  35012  bnj1449  35015  bnj1467  35021  bnj1489  35023  bnj1312  35025  bnj1497  35027  bnj1518  35031  bnj1525  35036  bnj1529  35037  dvelimalcased  35042  dvelimexcased  35044  axsepg2  35049  axsepg2ALT  35050  fineqvrep  35070  onvf1odlem2  35081  cvmcov  35240  untsucf  35687  setinds2  35758  dfon2lem1  35761  dfon2lem3  35763  finminlem  36296  weiunpo  36443  weiunso  36444  weiunfr  36445  weiunse  36446  bj-nexdvt  36676  bj-cbvaldv  36777  bj-cbval2vv  36779  bj-cbvex2vv  36780  bj-cbvaldvav  36781  bj-cbvexdvav  36782  ax11-pm2  36814  bj-dvelimdv  36829  bj-nfeel2  36832  bj-ceqsalv  36872  bj-vtocl  36894  bj-inrab2  36906  currysetlem  36923  currysetlem1  36925  bj-opabco  37166  mptsnunlem  37316  exlimim  37320  exellim  37322  topdifinfindis  37324  topdifinffinlem  37325  icorempo  37329  isbasisrelowllem1  37333  isbasisrelowllem2  37334  relowlssretop  37341  finxpreclem2  37368  finxpreclem6  37374  fvineqsneu  37389  fvineqsneq  37390  wl-euequf  37552  wl-sb8eut  37556  wl-issetft  37560  phpreu  37588  matunitlindflem2  37601  ptrest  37603  ptrecube  37604  poimirlem2  37606  poimirlem23  37627  poimirlem24  37628  poimirlem25  37629  poimirlem26  37630  poimirlem27  37631  poimirlem28  37632  heicant  37639  mbfposadd  37651  itgabsnc  37673  itggt0cn  37674  ftc1anclem5  37681  upixp  37713  indexa  37717  indexdom  37718  filbcmb  37724  sdclem2  37726  sdclem1  37727  fdc1  37730  totbndbnd  37773  sbcalf  38098  sbcexf  38099  scottexf  38152  scott0f  38153  eqrelf  38234  fsumshftd  38935  riotasv2d  38940  riotasv2s  38941  riotasv3d  38943  glbconxN  39361  pmapglbx  39752  pmapglb2xN  39755  cdleme26ee  40343  cdleme31sn  40363  cdleme31sn1  40364  cdlemefr29exN  40385  cdlemefs32sn1aw  40397  cdleme43fsv1snlem  40403  cdleme41sn3a  40416  cdleme32fva  40420  cdleme32d  40427  cdleme32f  40429  cdleme40m  40450  cdleme40n  40451  cdleme42b  40461  cdlemk36  40896  cdlemk38  40898  cdlemkid  40919  cdlemk19x  40926  cdlemk11t  40929  dihvalcqpre  41218  mapdheq  41711  hdmap1eq  41784  hdmapval2lem  41814  lcmineqlem9  42014  lcmineqlem12  42017  aks4d1p1p2  42047  mndmolinv  42072  primrootsunit1  42074  primrootsunit  42075  primrootspoweq0  42083  aks6d1c1p5  42089  aks6d1c3  42100  aks6d1c4  42101  aks6d1c1rh  42102  aks6d1c2lem4  42104  aks6d1c2  42107  deg1gprod  42117  sticksstones1  42123  sticksstones11  42133  sticksstones16  42139  sticksstones22  42145  aks6d1c6lem2  42148  aks6d1c6isolem1  42151  aks6d1c6isolem2  42152  bcled  42155  bcle2d  42156  aks6d1c7lem3  42159  aks6d1c7  42161  rhmqusspan  42162  grpods  42171  unitscyglem1  42172  unitscyglem2  42173  unitscyglem3  42174  unitscyglem4  42175  unitscyglem5  42176  nfa1w  42652  mzpexpmpt  42722  eq0rabdioph  42753  rexrabdioph  42771  rexfrabdioph  42772  elnn0rabdioph  42780  dvdsrabdioph  42787  fphpd  42793  monotuz  42918  monotoddzz  42920  oddcomabszz  42921  setindtr  43001  dford4  43006  wdom2d2  43012  aomclem6  43036  aomclem8  43038  flcidc  43147  areaquad  43193  unielss  43195  onsucf1lem  43246  oaun3lem1  43351  nadd1suc  43369  rababg  43551  ss2iundv  43637  cbviuneq12dv  43639  gneispace  44111  mnringvald  44190  mnringmulrcld  44205  nfscott  44216  scottabf  44217  scottab  44218  mnuprdlem4  44252  ismnushort  44278  binomcxplemdvsum  44332  binomcxplemnotnn0  44333  aaanv  44365  pm11.57  44366  pm11.58  44367  pm11.59  44368  pm11.71  44374  pm14.12  44398  ssralv2  44509  tratrb  44514  iunconnlem2  44912  modelaxreplem3  44958  modelaxrep  44959  permaxrep  44984  evth2f  44997  elunif  44998  fvelrnbf  45000  evthf  45009  fnchoice  45011  sumpair  45017  rfcnnnub  45018  refsum2cn  45020  uzwo4  45035  fiiuncl  45047  fiunicl  45049  elintdv  45061  ssd  45062  cbvmpo2  45079  cbvmpo1  45080  eliin2f  45086  eliuniin2  45102  cbvrabv2  45109  suprnmpt  45156  disjf1  45165  disjrnmpt2  45170  disjf1o  45173  disjinfi  45174  choicefi  45182  iunmapsn  45199  axccdom  45204  dmrelrnrel  45208  axccd  45211  fmptf  45221  rnmptlb  45225  rnmptbddlem  45226  rnmptbd2lem  45230  rnmptbdlem  45237  rnmptbd  45238  fmptff  45251  upbdrech  45291  ssfiunibd  45295  supxrgere  45317  iuneqfzuzlem  45318  supxrgelem  45321  supxrge  45322  suplesup  45323  infrpge  45335  xralrple2  45338  infxr  45350  infxrunb2  45351  infleinf  45355  xrralrecnnle  45366  xrralrecnnge  45373  supxrunb3  45382  supxrleubrnmpt  45389  infleinf2  45397  unb2ltle  45398  rexabslelem  45401  rexabsle  45402  allbutfiinf  45403  suprleubrnmpt  45405  infrnmptle  45406  infxrunb3rnmpt  45411  uzublem  45413  uzub  45414  supminfrnmpt  45428  infxrpnf  45429  supxrleubrnmptf  45434  infxrgelbrnmpt  45437  infrpgernmpt  45448  supminfxr2  45452  monoordxr  45465  monoord2xr  45467  caucvgbf  45472  cvgcaule  45474  rexanuz2nf  45475  iccshift  45503  iooshift  45507  iooiinicc  45527  iooiinioc  45541  fsummulc1f  45556  fsumnncl  45557  fsumf1of  45559  fsumiunss  45560  fsumreclf  45561  fsumlessf  45562  fsumsermpt  45564  fmul01  45565  fmuldfeqlem1  45567  fmuldfeq  45568  fmul01lt1lem1  45569  fmul01lt1lem2  45570  fmul01lt1  45571  fprodsplit1  45578  fprodexp  45579  fprodabs2  45580  mccllem  45582  mccl  45583  fprodcnlem  45584  fprodcn  45585  climexp  45590  climsuse  45593  climrecf  45594  climinff  45596  climaddf  45600  mullimc  45601  ellimcabssub0  45602  islptre  45604  climf  45607  mullimcf  45608  rexlim2d  45610  idlimc  45611  limcperiod  45613  limcrecl  45614  sumnnodd  45615  islpcn  45624  limsupre  45626  limcleqr  45629  neglimc  45632  addlimc  45633  0ellimcdiv  45634  limclner  45636  climsubmpt  45645  climreclf  45649  climf2  45651  fnlimcnv  45652  climeldmeqmpt  45653  clim2f2  45655  climfveqmpt  45656  fnlimfvre  45659  allbutfifvre  45660  climleltrp  45661  fnlimf  45663  fnlimabslt  45664  climfveqmpt3  45667  climeldmeqf  45668  limsupref  45670  limsupbnd1f  45671  climbddf  45672  climeqf  45673  climeldmeqmpt3  45674  limsuplesup  45684  limsuppnfd  45687  limsupub  45689  limsupres  45690  climinf2lem  45691  climinf2  45692  limsuppnf  45696  limsupubuzlem  45697  limsupubuz  45698  climinf2mpt  45699  climinfmpt  45700  climinf3  45701  limsupmnflem  45705  limsupmnf  45706  limsupequz  45708  limsupre2  45710  limsupmnfuzlem  45711  limsupmnfuz  45712  limsupequzmptf  45716  limsupre3lem  45717  limsupre3  45718  limsupre3uzlem  45720  limsupre3uz  45721  limsupreuz  45722  limsupvaluz2  45723  limsupreuzmpt  45724  supcnvlimsup  45725  climuzlem  45728  climuz  45729  climisp  45731  lmbr3  45732  climrescn  45733  climxrrelem  45734  climxrre  45735  liminfcl  45748  liminfval2  45753  limsup10exlem  45757  liminflelimsuplem  45760  limsupgtlem  45762  limsupgt  45763  climliminflimsupd  45786  liminfreuzlem  45787  liminfreuz  45788  liminfltlem  45789  liminflt  45790  limsupub2  45797  xlimpnfxnegmnf  45799  liminflbuz2  45800  liminfpnfuz  45801  liminflimsupxrre  45802  xlimmnfvlem1  45817  xlimmnfvlem2  45818  xlimmnfv  45819  xlimpnfvlem1  45821  xlimpnfvlem2  45822  xlimpnfv  45823  xlimmnf  45826  xlimpnf  45827  xlimmnfmpt  45828  xlimpnfmpt  45829  climxlim2lem  45830  dfxlim2  45833  cncfshift  45859  icccncfext  45872  cncficcgt0  45873  cncfiooicc  45879  cncfioobd  45882  fprodcncf  45885  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  dvmptmulf  45922  dvnmptdivc  45923  dvnmul  45928  dvmptfprodlem  45929  dvmptfprod  45930  dvnprodlem1  45931  dvnprodlem2  45932  iblsplitf  45955  iblspltprt  45958  itgioocnicc  45962  iblcncfioo  45963  itgspltprt  45964  itgperiod  45966  stoweidlem3  45988  stoweidlem14  45999  stoweidlem17  46002  stoweidlem19  46004  stoweidlem20  46005  stoweidlem26  46011  stoweidlem27  46012  stoweidlem28  46013  stoweidlem29  46014  stoweidlem31  46016  stoweidlem34  46019  stoweidlem35  46020  stoweidlem36  46021  stoweidlem39  46024  stoweidlem42  46027  stoweidlem43  46028  stoweidlem44  46029  stoweidlem46  46031  stoweidlem48  46033  stoweidlem49  46034  stoweidlem50  46035  stoweidlem51  46036  stoweidlem52  46037  stoweidlem53  46038  stoweidlem54  46039  stoweidlem56  46041  stoweidlem57  46042  stoweidlem59  46044  stoweidlem60  46045  stoweidlem61  46046  stoweidlem62  46047  stoweid  46048  wallispilem3  46052  stirlinglem13  46071  stirling  46074  fourierdlem16  46108  fourierdlem21  46113  fourierdlem22  46114  fourierdlem31  46123  fourierdlem39  46131  fourierdlem48  46139  fourierdlem51  46142  fourierdlem53  46144  fourierdlem68  46159  fourierdlem69  46160  fourierdlem71  46162  fourierdlem73  46164  fourierdlem77  46168  fourierdlem80  46171  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem86  46177  fourierdlem87  46178  fourierdlem89  46180  fourierdlem91  46182  fourierdlem93  46184  fourierdlem94  46185  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  fourierdlem113  46204  elaa2  46219  etransclem18  46237  etransclem22  46241  etransclem23  46242  etransclem32  46251  etransclem35  46254  etransclem44  46263  etransclem46  46265  etransclem48  46267  rrndistlt  46275  ioorrnopnlem  46289  saliuncl  46308  saliincl  46312  intsaluni  46314  salexct  46319  subsaliuncl  46343  sge00  46361  sge0revalmpt  46363  sge0sn  46364  sge0f1o  46367  sge0gerp  46380  sge0pnffigt  46381  sge0lefi  46383  sge0ltfirp  46385  sge0resrnlem  46388  sge0resplit  46391  sge0lempt  46395  sge0iunmptlemfi  46398  sge0p1  46399  sge0iunmptlemre  46400  sge0fodjrnlem  46401  sge0iunmpt  46403  sge0rpcpnf  46406  sge0ltfirpmpt2  46411  sge0isum  46412  sge0xp  46414  sge0ad2en  46416  sge0isummpt2  46417  sge0xaddlem1  46418  sge0xaddlem2  46419  sge0xadd  46420  sge0pnffsumgt  46427  sge0gtfsumgt  46428  sge0uzfsumgt  46429  sge0seq  46431  sge0reuz  46432  sge0reuzb  46433  iundjiun  46445  meadjiunlem  46450  meadjiun  46451  ismeannd  46452  voliunsge0lem  46457  meaiuninclem  46465  meaiunincf  46468  meaiuninc3v  46469  meaiuninc3  46470  meaiininclem  46471  meaiininc  46472  meaiininc2  46473  caragenfiiuncl  46500  omeiunltfirp  46504  carageniuncllem1  46506  carageniuncllem2  46507  caratheodorylem2  46512  0ome  46514  isomenndlem  46515  hoicvrrex  46541  ovnsupge0  46542  ovnlecvr  46543  ovnlerp  46547  ovncvrrp  46549  ovn0lem  46550  ovnsubaddlem1  46555  ovnsubaddlem2  46556  hoidmvcl  46567  hsphoidmvle2  46570  hsphoidmvle  46571  hoidmvval0  46572  sge0hsphoire  46574  hoidmvval0b  46575  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  hoidmvlelem5  46584  hoidmvle  46585  ovnhoilem1  46586  ovnhoilem2  46587  ovnhoi  46588  ovnlecvr2  46595  hspdifhsp  46601  hoidifhspdmvle  46605  hoiqssbllem3  46609  hspmbllem1  46611  hspmbllem2  46612  opnvonmbllem1  46617  opnvonmbllem2  46618  ovnsubadd2lem  46630  ovolval5lem1  46637  ovnovollem1  46641  ovnovollem2  46642  hoimbl2  46650  vonhoire  46657  iinhoiicclem  46658  iinhoiicc  46659  iunhoiioolem  46660  iunhoiioo  46661  vonioolem1  46665  vonioolem2  46666  vonioo  46667  vonicclem1  46668  vonicclem2  46669  vonicc  46670  vonn0ioo2  46675  vonn0icc2  46677  vonct  46678  pimltmnf2f  46682  pimgtpnf2f  46690  salpreimagelt  46692  salpreimalegt  46694  pimltpnf2f  46697  pimgtmnf2  46699  pimdecfgtioc  46700  pimincfltioc  46701  pimdecfgtioo  46702  pimincfltioo  46703  preimageiingt  46705  preimaleiinlt  46706  salpreimagtge  46710  salpreimaltle  46711  salpreimalelt  46714  salpreimagtlt  46715  issmff  46719  sssmf  46723  mbfresmf  46724  cnfsmf  46725  incsmflem  46726  incsmf  46727  smfsssmf  46728  issmflelem  46729  issmfle  46730  smfconst  46734  issmfgtlem  46740  issmfgt  46741  smfpimltxrmptf  46743  smfmbfcex  46745  smfaddlem1  46748  smfaddlem2  46749  smfadd  46750  decsmflem  46751  decsmf  46752  smfpreimagtf  46753  issmfgelem  46754  issmfge  46755  smflimlem2  46757  smflimlem4  46759  smflim  46762  smfpimgtxr  46765  smfpimgtxrmptf  46769  smfpimioo  46772  smfresal  46773  smfrec  46774  smfres  46775  smfmullem2  46777  smfmullem4  46779  smfmul  46780  smfpimbor1lem2  46784  smf2id  46786  smfco  46787  smflim2  46791  smfpimcc  46793  smflimmpt  46795  smfsuplem1  46796  smfsuplem3  46798  smfsup  46799  smfsupmpt  46800  smfsupxr  46801  smfinflem  46802  smfinf  46803  smfinfmpt  46804  smflimsuplem3  46807  smflimsuplem4  46808  smflimsuplem5  46809  smflimsuplem7  46811  smflimsuplem8  46812  smflimsup  46813  smflimsupmpt  46814  smfliminflem  46815  smfliminf  46816  smfliminfmpt  46817  smfpimne2  46825  fsupdm  46827  smfsupdmmbllem  46829  smfsupdmmbl  46830  finfdm  46831  smfinfdmmbllem  46833  smfinfdmmbl  46834  or2expropbilem1  47020  or2expropbilem2  47021  or2expropbi  47022  cfsetsnfsetf  47046  cfsetsnfsetfo  47048  rexsb  47087  reuf1odnf  47095  2reu8i  47101  ffnafv  47159  tz6.12c-afv2  47230  f1oresf1o2  47279  iccelpart  47421  iccpartdisj  47425  dfich2  47446  ichbi12i  47448  ichnfimlem  47451  ich2exprop  47459  ichnreuop  47460  ichreuopeq  47461  sprsymrelfo  47485  reupr  47510  reuopreuprim  47514  mogoldbb  47773  2zrngagrp  48237  2zrngmmgm  48240  cbvmpox2  48324  ovmpordx  48328  1arymaptfo  48632  2arymaptfo  48643  mo0sn  48804  iinfssclem3  49045  iinfssc  49046  iinfsubc  49047  infsubc2  49050  iinfconstbas  49055  isthincd2lem1  49414  nfintd  49662  nfiund  49663  nfiundg  49664  iunord  49665  spcdvw  49668  nfsetrecs  49675  setrec1lem2  49677  setrec1  49680  setrec2fun  49681  pgindnf  49705  pgind  49706  aacllem  49790