Theorem nfv 1918

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

Syntax hints:  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfvd  1919  nfsbvOLD  2329  cbvaldw  2337  cbval2v  2342  cbval2vOLD  2343  dvelimhw  2345  pm11.53  2346  19.12vv  2347  eeanv  2349  eeeanv  2350  sbnf2  2356  exsb  2357  2exsb  2358  sbbibvv  2360  sbievg  2361  cleljustALT2  2363  spimv  2390  spimev  2392  chvarv  2396  cbvalv  2400  cbvexv  2401  cbvald  2407  cbvaldva  2409  cbvexdva  2410  cbval2  2411  axc16i  2436  dvelimnf  2453  sbel2x  2474  sbiedv  2508  2sbiev  2509  sbid2v  2513  sbhb  2525  2sb8e  2535  nfmod2  2558  nfmodv  2559  mof  2563  mo4f  2567  euf  2576  sb8eulem  2598  cbvmow  2603  sbmo  2616  moexexvw  2630  moexexv  2641  2mo  2650  2mos  2651  2eu6  2658  axextmo  2713  nulmo  2714  abbi  2811  cleqh  2862  clelsb2  2867  clelabOLD  2883  nfcv  2906  nfeqd  2916  nfeld  2917  nfabdw  2929  nfabdwOLD  2930  nfabd  2931  dvelimdc  2933  nfcvf  2935  cleqf  2937  sbabelOLD  2941  2ralbida  3159  rexbidvaALT  3247  rexbidvALT  3249  r19.12  3252  r19.12OLD  3253  r19.29af  3259  reean  3291  rmobidva  3319  cbvralfwOLD  3359  cbvralf  3361  cbvreuw  3365  cbvrmow  3366  cbvreu  3370  cbvreuvwOLD  3376  cbvralv  3377  cbvrexv  3378  cbvreuv  3379  cbvrmov  3380  cbvralsvw  3391  cbvrexsvw  3392  cbvralsv  3393  cbvrexsv  3394  cbvrabw  3414  cbvrab  3415  abv  3433  abvALT  3434  issetf  3436  ceqsalvOLD  3458  ceqsralvOLD  3460  ceqsexvOLD  3470  ceqsex2  3472  vtoclgft  3482  vtocldOLD  3485  vtoclALT  3489  vtoclgOLD  3496  vtocl2gaf  3505  vtocl3gaf  3506  vtocl3gaOLD  3508  spc2ed  3530  rspct  3537  rspc  3539  rspce  3540  rspcvOLD  3548  rspcevOLD  3553  eqvincf  3572  ceqsexgvOLD  3577  clel2gOLD  3582  elabgtOLD  3597  elabgOLD  3601  elabOLD  3603  elrab3t  3616  ralab2  3627  ralab2OLD  3628  rexab2  3630  rexab2OLD  3631  mob2  3645  mob  3647  reu2  3655  rmo4f  3665  reu2eqd  3666  cdeqab1  3702  nfcdeq  3707  sbcco  3737  cbvsbcv  3748  sbciegOLD  3752  sbciedOLD  3757  elrabsf  3759  sbcbidvOLD  3771  sbcgOLD  3792  sbc2iegf  3794  sbc2ieOLD  3796  reu8nf  3806  rmo2  3816  rmo3  3818  rmoanimALT  3824  csbeq2dv  3835  nfcsb1d  3851  nfcsbd  3854  csbiebt  3858  csbiedOLD  3867  csbie2t  3869  cbvrabcsfw  3872  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  cbvralv2  3877  cbvrexv2  3878  rspc2vd  3879  dfss2f  3907  uniiunlem  4015  rspn0OLD  4284  ab0OLD  4306  ab0orv  4309  ab0orvALT  4310  sbcnestgw  4351  sbcnestg  4356  sbnfc2  4367  r19.3rzv  4426  r19.28zv  4428  r19.27zv  4433  2reu4lem  4453  nfifd  4485  reusngf  4605  reusng  4608  ralsngOLD  4610  rexsngOLD  4611  rexreusng  4612  ralprgOLD  4628  rexprgOLD  4630  reuprg0  4635  rabsnifsb  4655  euabsn  4659  nfunid  4842  eluniab  4851  nfint  4886  elintab  4887  iuneqconst  4932  iineq2dv  4946  disjiun  5057  disjxun  5068  nfopabd  5138  cbvopab  5142  cbvopabvOLD  5144  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  cbvopab1vOLD  5150  mpteq12da  5155  mpteq12dfOLD  5157  mpteq12f  5158  mpteq2dvaOLD  5171  cbvmptf  5179  cbvmptfg  5180  axrep1  5206  axrep2  5208  axrep3  5209  axrep4  5210  axrep5  5211  zfrepclf  5213  reusv2lem3  5318  reusv2lem4  5319  reusv2  5321  reusv3  5323  alxfr  5325  ralxfrALT  5333  axprlem3  5343  axprlem4  5344  axprlem5  5345  copsex2t  5400  copsex2gOLD  5402  iunopeqop  5429  rexopabb  5434  opelopabaf  5450  nfso  5500  pofun  5512  isso2i  5529  nffr  5554  opeliunxp  5645  opeliunxp2  5736  ralxpf  5744  dfdmf  5794  dfrnf  5848  elrnmpt1  5856  dfrel4  6083  reuop  6185  frpoinsg  6231  frpoins2g  6233  wfisgOLD  6242  wfis2g  6247  nfiotadw  6379  nfiotad  6381  cbviotaw  6383  cbviotavwOLD  6385  cbviota  6386  cbviotav  6387  sb8iota  6388  iota2d  6406  iota2  6407  dffun6f  6432  imadif  6502  funimaexg  6504  isarep1  6506  isarep2  6507  fv3  6774  tz6.12f  6780  tz6.12c  6781  fvelimad  6818  feqmptdf  6821  opabiotafun  6831  funfv2f  6839  fvmptd  6864  fvmptd2f  6873  fvmptdv  6874  fvmptt  6877  fvopab5  6889  eqfnfv2f  6895  ralrnmptw  6952  ralrnmpt  6954  f1ompt  6967  ffnfv  6974  ffnfvf  6975  f1ossf1o  6982  fmptco  6983  elabrex  7098  dff13f  7110  fsnex  7135  fliftfun  7163  cbvriotaw  7221  cbvriotavwOLD  7223  cbvriota  7226  cbvriotav  7227  riota2  7238  riotaeqimp  7239  riota5f  7241  oprabv  7313  nfoprab  7317  mpoeq123  7325  cbvoprab1  7340  cbvoprab2  7341  cbvoprab12  7342  cbvoprab12v  7343  cbvoprab3  7344  cbvoprab3v  7345  cbvmpox  7346  ralrnmpo  7390  ovmpodx  7402  ovmpodf  7407  ovmpodv  7408  ov3  7413  ovmpt3rab1  7505  ofrfval2  7532  onminex  7629  tfis  7676  tfis2  7678  tfisi  7680  tfinds  7681  tfindes  7684  peano5OLD  7715  findes  7723  fiun  7759  f1iun  7760  abrexex2g  7780  opabex3d  7781  opabex3rd  7782  opabex3  7783  dfoprab4f  7869  fmpox  7880  offval22  7899  ovmptss  7904  opeliunxp2f  7997  tposoprab  8049  fvmpocurryd  8058  nffrecs  8070  nfwrecsOLD  8104  tfr3  8201  nfrdg  8216  tz7.48-1  8244  tz7.49  8246  eqerlem  8490  erovlem  8560  mptelixpg  8681  boxcutc  8687  dom2lem  8735  xpf1o  8875  mapxpen  8879  nneneq  8896  findcard2  8909  pssnn  8913  pssnnOLD  8969  findcard2OLD  8986  ac6sfi  8988  fiint  9021  indexfi  9057  wdom2d  9269  ixpiunwdom  9279  cantnflem1  9377  trpredmintr  9409  frinsg  9440  frins2  9443  r1val1  9475  rankuni2b  9542  scottexs  9576  scott0s  9577  dfac8clem  9719  acni2  9733  aceq1  9804  dfac5lem5  9814  kmlem15  9851  infpssrlem4  9993  fin23lem27  10015  hsmexlem2  10114  hsmexlem4  10116  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  ac6c4  10168  zorn2lem4  10186  zorn2lem5  10187  iunfo  10226  iundom2g  10227  uniimadomf  10232  konigthlem  10255  axrepndlem2  10280  axunnd  10283  axpowndlem2  10285  axpowndlem4  10287  axregndlem2  10290  axacndlem5  10298  zfcndrep  10301  zfcndinf  10305  pwfseqlem4a  10348  pwfseqlem4  10349  tskuni  10470  gruiin  10497  reclem2pr  10735  dedekind  11068  dedekindle  11069  fimaxre3  11851  nn0ind-raph  12350  uzind4s  12577  nnwof  12583  lbzbi  12605  fzrevral  13270  rabssnn0fi  13634  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  fsuppmapnn0fiubex  13640  seqof2  13709  reuccatpfxs1  14388  cotr2g  14615  rlim2  15133  ello1mpt  15158  climeu  15192  o1compt  15224  summolem2a  15355  zsum  15358  sumss  15364  sumss2  15366  fsumcvg2  15367  fsumclf  15378  fsumsplitf  15382  fsumsplit1  15385  fsum2dlem  15410  fsum00  15438  o1fsum  15453  nfcprod1  15548  nfcprod  15549  prodmolem2a  15572  zprod  15575  fprod  15579  fprodntriv  15580  prodss  15585  fprodn0  15617  fprod2dlem  15618  fprodsplitf  15626  fprodsplit1f  15628  fprodle  15634  fprodmodd  15635  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  coprmprod  16294  coprmproddvdslem  16295  prmind2  16318  iserodd  16464  pcmpt  16521  pcmptdvds  16523  prmolefac  16675  mreexexd  17274  catpropd  17335  invfuc  17608  natpropd  17610  fucpropd  17611  initoeu2  17647  acsmapd  18187  symgval  18891  gsumsnd  19468  gsumsnf  19469  gsumunsnfd  19473  gsummptf1o  19479  gsummpt1n0  19481  gsum2d2lem  19489  gsumcom2  19491  gsummptnn0fz  19502  dprd2d2  19562  gsummoncoe1  21385  gsumply1eq  21386  mdetralt2  21666  mdetunilem2  21670  madugsum  21700  gsummatr01lem4  21715  cpmatmcllem  21775  cayleyhamilton1  21949  neiptopnei  22191  neiptopreu  22192  neitr  22239  fiuncmp  22463  iunconnlem  22486  iunconn  22487  2ndcdisj  22515  dissnlocfin  22588  elptr2  22633  ptbasfi  22640  ptcld  22672  ptcldmpt  22673  ptclsg  22674  ptcnplem  22680  ptcnp  22681  cnmpt11  22722  cnmpt21  22730  cnmptcom  22737  imasnopn  22749  imasncld  22750  imasncls  22751  xkocnv  22873  elmptrab  22886  isfildlem  22916  alexsubALTlem3  23108  cnextfvval  23124  utopsnneiplem  23307  isucn2  23339  cfilucfil  23621  blval2  23624  restmetu  23632  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  ovoliunnul  24576  finiunmbl  24613  volfiniun  24616  iundisj  24617  iunmbl  24622  voliun  24623  iunmbl2  24626  mbfeqalem1  24710  mbfsup  24733  mbfinf  24734  mbflim  24737  itg2splitlem  24818  itg2split  24819  isibl2  24836  cbvitg  24845  itgeqa  24883  itgss3  24884  itgfsum  24896  itgabs  24904  itggt0  24913  itgcn  24914  limcmpt  24952  limciun  24963  dvmptfsum  25044  dvlipcn  25063  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim  25100  dvfsum2  25103  itgsubst  25118  coeeq2  25308  dgrle  25309  ulmss  25461  leibpi  25997  rlimcnp  26020  rlimcnp2  26021  o1cxp  26029  lgamgulmlem2  26084  lgamgulmlem6  26088  fsumdvdscom  26239  lgseisenlem2  26429  2sqmo  26490  2sqreulem4  26507  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  istrkg2ld  26725  mptelee  27166  gropd  27304  grstructd  27305  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  ex-natded9.26  28684  isch3  29504  atom1d  30616  chirred  30658  sbc2iedf  30716  rspc2daf  30717  19.9d2r  30722  opreu2reuALT  30726  mo5f  30738  reuxfrdf  30740  eqrrabd  30750  foresf1o  30751  elabreximdv  30757  rabss3d  30762  iinabrex  30809  cbvdisjf  30811  disjorf  30819  disjabrex  30822  iundisjf  30829  disjunsn  30834  brabgaf  30849  ac6sf2  30861  dfimafnf  30872  fimarab  30881  2ndresdju  30887  fmptcof2  30896  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  aciunf1  30902  ofpreima  30904  funcnv5mpt  30907  funcnv4mpt  30908  fnpreimac  30910  padct  30956  cnvoprabOLD  30957  f1od2  30958  fpwrelmap  30970  xrofsup  30992  iundisjfi  31019  nnindf  31035  nn0min  31036  fprodex01  31041  fsumiunle  31045  gsummpt2d  31211  gsumhashmul  31218  isarchiofld  31418  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem3  31502  nsgqusf1o  31503  elrspunidl  31508  fedgmullem2  31613  reff  31691  locfinreflem  31692  cmpcref  31702  zarclsiin  31723  zarcls  31726  zarcmplem  31733  ordtconnlem1  31776  qqhval2  31832  prodindf  31891  esumeq12dva  31900  esumeq2dv  31906  esumrnmpt  31920  esumpad  31923  esumpad2  31924  esumadd  31925  gsumesum  31927  esumlub  31928  esumsnf  31932  esumpr  31934  esumrnmpt2  31936  esumfzf  31937  esumfsup  31938  esumpcvgval  31946  esumpmono  31947  esumcocn  31948  hasheuni  31953  esumcvg  31954  esumgect  31958  esum2dlem  31960  esum2d  31961  esumiun  31962  ldsysgenld  32028  sigapildsyslem  32029  sigapildsys  32030  ldgenpisyslem1  32031  fiunelros  32042  measvunilem  32080  measvunilem0  32081  measvuni  32082  measiun  32086  measinblem  32088  voliune  32097  volfiniune  32098  volmeas  32099  ddemeas  32104  oms0  32164  omssubadd  32167  carsgclctunlem1  32184  carsggect  32185  omsmeas  32190  eulerpartlemgvv  32243  dstrvprob  32338  ballotlemodife  32364  reprsuc  32495  reprdifc  32507  breprexplema  32510  breprexplemc  32512  circlemethhgt  32523  hgt750lemd  32528  bnj919  32647  bnj1146  32671  bnj1379  32710  bnj1385  32712  bnj1400  32715  bnj1534  32733  bnj1542  32737  bnj110  32738  bnj121  32750  bnj124  32751  bnj130  32754  bnj207  32761  bnj571  32786  bnj605  32787  bnj580  32793  bnj607  32796  bnj611  32798  bnj873  32804  bnj849  32805  bnj900  32809  bnj916  32813  bnj1000  32821  bnj964  32823  bnj981  32830  bnj985v  32833  bnj985  32834  bnj1014  32841  bnj1123  32866  bnj1128  32870  bnj1228  32891  bnj1204  32892  bnj1279  32898  bnj1307  32903  bnj1321  32907  bnj1388  32913  bnj1398  32914  bnj1408  32916  bnj1417  32921  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1449  32928  bnj1467  32934  bnj1489  32936  bnj1312  32938  bnj1497  32940  bnj1518  32944  bnj1525  32949  bnj1529  32950  fineqvrep  32964  cvmcov  33125  untsucf  33551  ralxpes  33581  ralxp3  33589  ralxp3es  33591  setinds2  33662  dfon2lem1  33665  dfon2lem3  33667  nfttrcld  33696  frpoins3xpg  33714  frpoins3xp3g  33715  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  finminlem  34434  bj-nexdvt  34807  bj-cbvaldv  34908  bj-cbval2vv  34910  bj-cbvex2vv  34911  bj-cbvaldvav  34912  bj-cbvexdvav  34913  ax11-pm2  34946  bj-dvelimdv  34962  bj-nfeel2  34965  bj-ceqsalv  35006  bj-vtocl  35028  bj-inrab2  35043  currysetlem  35061  currysetlem1  35063  bj-opabco  35286  mptsnunlem  35436  exlimim  35440  exellim  35442  topdifinfindis  35444  topdifinffinlem  35445  icorempo  35449  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  finxpreclem2  35488  finxpreclem6  35494  fvineqsneu  35509  fvineqsneq  35510  wl-euequf  35656  wl-sb8eut  35659  phpreu  35688  matunitlindflem2  35701  ptrest  35703  ptrecube  35704  poimirlem2  35706  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  heicant  35739  mbfposadd  35751  itgabsnc  35773  itggt0cn  35774  ftc1anclem5  35781  upixp  35814  indexa  35818  indexdom  35819  filbcmb  35825  sdclem2  35827  sdclem1  35828  fdc1  35831  totbndbnd  35874  sbcalf  36199  sbcexf  36200  scottexf  36253  scott0f  36254  eqrelf  36322  fsumshftd  36893  riotasv2d  36898  riotasv2s  36899  riotasv3d  36901  glbconxN  37319  pmapglbx  37710  pmapglb2xN  37713  cdleme26ee  38301  cdleme31sn  38321  cdleme31sn1  38322  cdlemefr29exN  38343  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32fva  38378  cdleme32d  38385  cdleme32f  38387  cdleme40m  38408  cdleme40n  38409  cdleme42b  38419  cdlemk36  38854  cdlemk38  38856  cdlemkid  38877  cdlemk19x  38884  cdlemk11t  38887  dihvalcqpre  39176  mapdheq  39669  hdmap1eq  39742  hdmapval2lem  39772  lcmineqlem9  39973  lcmineqlem12  39976  aks4d1p1p2  40006  sticksstones1  40030  sticksstones11  40040  sticksstones16  40046  sticksstones22  40052  metakunt33  40085  mzpexpmpt  40483  eq0rabdioph  40514  rexrabdioph  40532  rexfrabdioph  40533  elnn0rabdioph  40541  dvdsrabdioph  40548  fphpd  40554  monotuz  40679  monotoddzz  40681  oddcomabszz  40682  setindtr  40762  dford4  40767  wdom2d2  40773  aomclem6  40800  aomclem8  40802  flcidc  40915  areaquad  40963  rababg  41070  ss2iundv  41157  cbviuneq12dv  41159  gneispace  41633  mnringvald  41715  mnringmulrcld  41735  nfscott  41746  scottabf  41747  scottab  41748  mnuprdlem4  41782  ismnushort  41808  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  aaanv  41895  pm11.57  41896  pm11.58  41897  pm11.59  41898  pm11.71  41904  pm14.12  41928  ssralv2  42040  tratrb  42045  iunconnlem2  42444  evth2f  42447  elunif  42448  fvelrnbf  42450  evthf  42459  fnchoice  42461  sumpair  42467  rfcnnnub  42468  refsum2cn  42470  elabrexg  42478  uzwo4  42490  fiiuncl  42502  fiunicl  42504  elintdv  42518  ssd  42519  cbvmpo2  42536  cbvmpo1  42537  eliin2f  42543  eliuniin2  42558  cbvrabv2  42565  cbvrabv2w  42566  suprnmpt  42599  dffo3f  42606  disjf1  42609  disjrnmpt2  42615  disjf1o  42618  fompt  42619  disjinfi  42620  choicefi  42629  iunmapsn  42646  axccdom  42651  dmrelrnrel  42654  axccd  42657  funimassd  42659  fmptf  42672  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  rnmptbdlem  42690  rnmptbd  42691  upbdrech  42734  ssfiunibd  42738  supxrgere  42762  iuneqfzuzlem  42763  supxrgelem  42766  supxrge  42767  suplesup  42768  infrpge  42780  xralrple2  42783  infxr  42796  infxrunb2  42797  infleinf  42801  xrralrecnnle  42812  xrralrecnnge  42820  supxrunb3  42829  supxrleubrnmpt  42836  infleinf2  42844  unb2ltle  42845  rexabslelem  42848  rexabsle  42849  allbutfiinf  42850  suprleubrnmpt  42852  infrnmptle  42853  infxrunb3rnmpt  42858  uzublem  42860  uzub  42861  supminfrnmpt  42875  infxrpnf  42876  supxrleubrnmptf  42881  infxrgelbrnmpt  42884  infrpgernmpt  42895  supminfxr2  42899  monoordxr  42913  monoord2xr  42915  iccshift  42946  iooshift  42950  iooiinicc  42970  iooiinioc  42984  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumiunss  43006  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fmul01lt1  43017  fprodsplit1  43024  fprodexp  43025  fprodabs2  43026  mccllem  43028  mccl  43029  fprodcnlem  43030  fprodcn  43031  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  ellimcabssub0  43048  islptre  43050  climf  43053  mullimcf  43054  rexlim2d  43056  idlimc  43057  limcperiod  43059  limcrecl  43060  sumnnodd  43061  islpcn  43070  limsupre  43072  limcleqr  43075  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  climsubmpt  43091  climreclf  43095  climf2  43097  fnlimcnv  43098  climeldmeqmpt  43099  clim2f2  43101  climfveqmpt  43102  fnlimfvre  43105  allbutfifvre  43106  climleltrp  43107  fnlimf  43109  fnlimabslt  43110  climfveqmpt3  43113  climeldmeqf  43114  limsupref  43116  limsupbnd1f  43117  climbddf  43118  climeqf  43119  climeldmeqmpt3  43120  limsuplesup  43130  limsuppnfd  43133  limsupub  43135  limsupres  43136  climinf2lem  43137  climinf2  43138  limsuppnf  43142  limsupubuzlem  43143  limsupubuz  43144  climinf2mpt  43145  climinfmpt  43146  climinf3  43147  limsupmnflem  43151  limsupmnf  43152  limsupequz  43154  limsupre2  43156  limsupmnfuzlem  43157  limsupmnfuz  43158  limsupequzmptf  43162  limsupre3lem  43163  limsupre3  43164  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  limsupvaluz2  43169  limsupreuzmpt  43170  supcnvlimsup  43171  climuzlem  43174  climuz  43175  climisp  43177  lmbr3  43178  climrescn  43179  climxrrelem  43180  climxrre  43181  liminfcl  43194  liminfval2  43199  limsup10exlem  43203  liminflelimsuplem  43206  limsupgtlem  43208  limsupgt  43209  climliminflimsupd  43232  liminfreuzlem  43233  liminfreuz  43234  liminfltlem  43235  liminflt  43236  limsupub2  43243  xlimpnfxnegmnf  43245  liminflbuz2  43246  liminfpnfuz  43247  liminflimsupxrre  43248  xlimmnfvlem1  43263  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem1  43267  xlimpnfvlem2  43268  xlimpnfv  43269  xlimmnf  43272  xlimpnf  43273  xlimmnfmpt  43274  xlimpnfmpt  43275  climxlim2lem  43276  dfxlim2  43279  cncfshift  43305  icccncfext  43318  cncficcgt0  43319  cncfiooicc  43325  cncfioobd  43328  fprodcncf  43331  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvmptmulf  43368  dvnmptdivc  43369  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  iblsplitf  43401  iblspltprt  43404  itgioocnicc  43408  iblcncfioo  43409  itgspltprt  43410  itgperiod  43412  stoweidlem3  43434  stoweidlem14  43445  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem26  43457  stoweidlem27  43458  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem36  43467  stoweidlem39  43470  stoweidlem42  43473  stoweidlem43  43474  stoweidlem44  43475  stoweidlem46  43477  stoweidlem48  43479  stoweidlem49  43480  stoweidlem50  43481  stoweidlem51  43482  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem56  43487  stoweidlem57  43488  stoweidlem59  43490  stoweidlem60  43491  stoweidlem61  43492  stoweidlem62  43493  stoweid  43494  wallispilem3  43498  stirlinglem13  43517  stirling  43520  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem31  43569  fourierdlem39  43577  fourierdlem48  43585  fourierdlem51  43588  fourierdlem53  43590  fourierdlem68  43605  fourierdlem69  43606  fourierdlem71  43608  fourierdlem73  43610  fourierdlem77  43614  fourierdlem80  43617  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem86  43623  fourierdlem87  43624  fourierdlem89  43626  fourierdlem91  43628  fourierdlem93  43630  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  elaa2  43665  etransclem18  43683  etransclem22  43687  etransclem23  43688  etransclem32  43697  etransclem35  43700  etransclem44  43709  etransclem46  43711  etransclem48  43713  rrndistlt  43721  ioorrnopnlem  43735  intsaluni  43758  salexct  43763  subsaliuncl  43787  sge00  43804  sge0revalmpt  43806  sge0sn  43807  sge0f1o  43810  sge0gerp  43823  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resrnlem  43831  sge0resplit  43834  sge0lempt  43838  sge0iunmptlemfi  43841  sge0p1  43842  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0rpcpnf  43849  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xp  43857  sge0ad2en  43859  sge0isummpt2  43860  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0xadd  43863  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  sge0reuzb  43876  iundjiun  43888  meadjiunlem  43893  meadjiun  43894  ismeannd  43895  voliunsge0lem  43900  meaiuninclem  43908  meaiunincf  43911  meaiuninc3v  43912  meaiuninc3  43913  meaiininclem  43914  meaiininc  43915  meaiininc2  43916  caragenfiiuncl  43943  omeiunltfirp  43947  carageniuncllem1  43949  carageniuncllem2  43950  caratheodorylem2  43955  0ome  43957  isomenndlem  43958  hoicvrrex  43984  ovnsupge0  43985  ovnlecvr  43986  ovnlerp  43990  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubaddlem2  43999  hoidmvcl  44010  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmvval0  44015  sge0hsphoire  44017  hoidmvval0b  44018  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem1  44029  ovnhoilem2  44030  ovnhoi  44031  ovnlecvr2  44038  hspdifhsp  44044  hoidifhspdmvle  44048  hoiqssbllem3  44052  hspmbllem1  44054  hspmbllem2  44055  opnvonmbllem1  44060  opnvonmbllem2  44061  ovnsubadd2lem  44073  ovolval5lem1  44080  ovnovollem1  44084  ovnovollem2  44085  hoimbl2  44093  vonhoire  44100  iinhoiicclem  44101  iinhoiicc  44102  iunhoiioolem  44103  iunhoiioo  44104  vonioolem1  44108  vonioolem2  44109  vonioo  44110  vonicclem1  44111  vonicclem2  44112  vonicc  44113  vonn0ioo2  44118  vonn0icc2  44120  vonct  44121  pimltmnf2  44125  pimgtpnf2  44131  salpreimagelt  44132  salpreimalegt  44134  pimltpnf2  44137  pimgtmnf2  44138  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  salpreimagtge  44148  salpreimaltle  44149  salpreimalelt  44152  salpreimagtlt  44153  issmff  44157  sssmf  44161  mbfresmf  44162  cnfsmf  44163  incsmflem  44164  incsmf  44165  smfsssmf  44166  issmflelem  44167  issmfle  44168  smfconst  44172  issmfgtlem  44178  issmfgt  44179  smfpimltxrmpt  44181  smfmbfcex  44182  smfaddlem1  44185  smfaddlem2  44186  smfadd  44187  decsmflem  44188  decsmf  44189  smfpreimagtf  44190  issmfgelem  44191  issmfge  44192  smflimlem2  44194  smflimlem4  44196  smflim  44199  smfpimgtxr  44202  smfpimgtxrmpt  44206  smfpimioo  44208  smfresal  44209  smfrec  44210  smfres  44211  smfmullem2  44213  smfmullem4  44215  smfmul  44216  smfpimbor1lem2  44220  smf2id  44222  smfco  44223  smflim2  44226  smfpimcc  44228  smflimmpt  44230  smfsuplem1  44231  smfsuplem3  44233  smfsup  44234  smfsupmpt  44235  smfsupxr  44236  smfinflem  44237  smfinf  44238  smfinfmpt  44239  smflimsuplem3  44242  smflimsuplem4  44243  smflimsuplem5  44244  smflimsuplem7  44246  smflimsuplem8  44247  smflimsup  44248  smflimsupmpt  44249  smfliminflem  44250  smfliminf  44251  smfliminfmpt  44252  or2expropbilem1  44413  or2expropbilem2  44414  or2expropbi  44415  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  rexsb  44478  reuf1odnf  44486  2reu8i  44492  ffnafv  44550  tz6.12c-afv2  44621  f1oresf1o2  44670  iccelpart  44773  iccpartdisj  44777  dfich2  44798  ichbi12i  44800  ichnfimlem  44803  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  sprsymrelfo  44837  reupr  44862  reuopreuprim  44866  mogoldbb  45125  2zrngagrp  45389  2zrngmmgm  45392  opeliun2xp  45556  cbvmpox2  45559  ovmpordx  45563  1arymaptfo  45877  2arymaptfo  45888  mo0sn  46049  isthincd2lem1  46196  nfintd  46265  nfiund  46266  nfiundg  46267  iunord  46268  spcdvw  46271  nfsetrecs  46278  setrec1lem2  46280  setrec1  46283  setrec2fun  46284  aacllem  46391