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  3246  rexbidvALT  3252  rexbidvaALT  3253  2ralbida  3260  r19.12  3288  reean  3289  cbvrexsvw  3291  cbvralsvwOLD  3292  cbvralsvwOLDOLD  3293  cbvrexsvwOLD  3294  sbralieOLD  3328  cbvralf  3334  cbvralv  3338  cbvrexv  3339  cbvralsv  3340  cbvrexsv  3341  cbvrmow  3381  cbvreu  3397  cbvrmov  3399  cbvreuv  3400  cbvrabwOLD  3442  cbvrab  3446  cbvexeqsetf  3462  ceqsex2  3501  vtocl2gaf  3545  vtocl2gafOLD  3546  vtocl3gaf  3547  vtocl3gafOLD  3548  spc2ed  3567  rspct  3574  rspc  3576  rspce  3577  eqvincf  3616  elrab3t  3658  ralab2  3668  rexab2  3670  mob2  3686  mob  3688  reu2  3696  rmo4f  3706  reu2eqd  3707  cdeqab1  3743  nfcdeq  3748  sbcco  3779  cbvsbcv  3789  elrabsf  3799  sbc2iegf  3828  reu8nf  3840  rmo2  3850  rmo3  3852  rmoanimALT  3858  nfcsb1d  3884  nfcsbd  3887  csbiebt  3891  csbie2t  3900  cbvrabcsfw  3903  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  cbvralv2  3908  cbvrexv2  3909  rspc2vd  3910  dfssf  3937  rabss3d  4044  eqrrabd  4049  uniiunlem  4050  ab0orv  4346  ab0orvALT  4347  sbcnestgw  4386  sbcnestg  4391  sbnfc2  4402  r19.3rzv  4462  r19.28zv  4464  r19.27zv  4469  2reu4lem  4485  nfifd  4518  reusngf  4638  reusng  4641  rexreusng  4643  reuprg0  4666  rabsnifsb  4686  euabsn  4690  nfunid  4877  eluniab  4885  nfint  4920  elintabOLD  4923  iuneqconst  4967  disjiun  5095  disjxun  5105  nfopabd  5175  cbvopab  5179  cbvopab1  5181  cbvopab1g  5182  cbvopab2  5183  cbvopab1s  5184  mpteq12da  5190  mpteq12f  5192  cbvmptf  5207  cbvmptfg  5208  axrep1  5235  axrep2  5237  axrep3  5238  axrep4OLD  5241  axrep5  5242  zfrepclf  5246  reusv2lem3  5355  reusv2lem4  5356  reusv2  5358  reusv3  5360  alxfr  5362  ralxfrALT  5370  axprlem3OLD  5383  axprlem4OLD  5384  axprlem5OLD  5385  copsex2t  5452  iunopeqop  5481  rexopabb  5488  opelopabaf  5504  nfso  5553  pofun  5564  isso2i  5583  nffr  5611  opeliunxp  5705  opeliun2xp  5706  opeliunxp2  5802  ralxpf  5810  dfdmf  5860  dfrnf  5914  elrnmpt1  5924  dfrel4  6164  reuop  6266  frpoinsg  6316  frpoins2g  6318  wfis2g  6328  nfiotadw  6467  nfiotad  6469  cbviotaw  6471  cbviota  6473  cbviotav  6474  sb8iota  6475  iota2d  6499  iota2  6500  dffun6f  6529  imadif  6600  funimaexgOLD  6604  isarep1  6606  isarep1OLD  6607  isarep2  6608  fv3  6876  tz6.12f  6884  tz6.12cOLD  6885  funimassd  6927  fvelimad  6928  feqmptdf  6931  fimarab  6935  opabiotafun  6941  funfv2f  6950  fvmptd  6975  fvmptd2f  6984  fvmptdv  6985  fvmptt  6988  fvopab5  7001  eqfnfv2f  7007  ralrnmptw  7066  ralrnmpt  7068  dffo3f  7078  f1ompt  7083  fompt  7090  ffnfv  7091  ffnfvf  7092  f1ossf1o  7100  fmptco  7101  elabrex  7216  elabrexg  7217  dff13f  7230  fsnex  7258  fliftfun  7287  cbvriotaw  7353  cbvriota  7357  cbvriotav  7358  riota2  7369  riotaeqimp  7370  riota5f  7372  oprabv  7449  nfoprab  7453  mpoeq123  7461  cbvoprab1  7476  cbvoprab2  7477  cbvoprab12  7478  cbvoprab3  7480  cbvmpox  7482  ralrnmpo  7528  ovmpodx  7540  ovmpodf  7545  ovmpodv  7546  ov3  7552  ovmpt3rab1  7647  ofrfval2  7674  onminex  7778  tfis  7831  tfis2  7833  tfisi  7835  tfinds  7836  tfindes  7839  findes  7876  fiun  7921  f1iun  7922  abrexex2g  7943  opabex3d  7944  opabex3rd  7945  opabex3  7946  dfoprab4f  8035  fmpox  8046  offval22  8067  ovmptss  8072  ralxpes  8115  ralxp3  8117  ralxp3es  8118  frpoins3xpg  8119  frpoins3xp3g  8120  opeliunxp2f  8189  tposoprab  8241  fvmpocurryd  8250  nffrecs  8262  tfr3  8367  nfrdg  8382  tz7.48-1  8411  tz7.49  8413  naddsuc2  8665  eqerlem  8706  erovlem  8786  mptelixpg  8908  boxcutc  8914  dom2lem  8963  xpf1o  9103  mapxpen  9107  findcard2  9128  pssnn  9132  nneneq  9170  ac6sfi  9231  fiint  9277  fiintOLD  9278  indexfi  9311  wdom2d  9533  ixpiunwdom  9543  cantnflem1  9642  nfttrcld  9663  frinsg  9704  frins2  9707  r1val1  9739  rankuni2b  9806  scottexs  9840  scott0s  9841  dfac8clem  9985  acni2  9999  aceq1  10070  dfac5lem5  10080  kmlem15  10118  infpssrlem4  10259  fin23lem27  10281  hsmexlem2  10380  hsmexlem4  10382  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  ac6c4  10434  zorn2lem4  10452  zorn2lem5  10453  iunfo  10492  iundom2g  10493  uniimadomf  10498  konigthlem  10521  axrepndlem2  10546  axunnd  10549  axpowndlem2  10551  axpowndlem4  10553  axregndlem2  10556  axacndlem5  10564  zfcndrep  10567  zfcndinf  10571  pwfseqlem4a  10614  pwfseqlem4  10615  tskuni  10736  gruiin  10763  reclem2pr  11001  dedekind  11337  dedekindle  11338  fimaxre3  12129  nn0ind-raph  12634  uzind4s  12867  nnwof  12873  lbzbi  12895  fzrevral  13573  rabssnn0fi  13951  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  seqof2  14025  reuccatpfxs1  14712  cotr2g  14942  rlim2  15462  ello1mpt  15487  climeu  15521  o1compt  15553  summolem2a  15681  zsum  15684  sumss  15690  sumss2  15692  fsumcvg2  15693  fsumclf  15704  fsumsplitf  15708  fsumsplit1  15711  fsum2dlem  15736  fsum00  15764  o1fsum  15779  nfcprod1  15874  nfcprod  15875  prodmolem2a  15900  zprod  15903  fprod  15907  fprodntriv  15908  prodss  15913  fprodn0  15945  fprod2dlem  15946  fprodsplitf  15954  fprodsplit1f  15956  fprodle  15962  fprodmodd  15963  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  coprmprod  16631  coprmproddvdslem  16632  prmind2  16655  iserodd  16806  pcmpt  16863  pcmptdvds  16865  prmolefac  17017  mreexexd  17609  catpropd  17670  invfuc  17939  natpropd  17941  fucpropd  17942  initoeu2  17978  acsmapd  18513  symgval  19301  gsumsnd  19882  gsumsnf  19883  gsumunsnfd  19887  gsummptf1o  19893  gsummpt1n0  19895  gsum2d2lem  19903  gsumcom2  19905  gsummptnn0fz  19916  dprd2d2  19976  rngqiprngimf1  21210  gsummoncoe1  22195  gsumply1eq  22196  mdetralt2  22496  mdetunilem2  22500  madugsum  22530  gsummatr01lem4  22545  cpmatmcllem  22605  cayleyhamilton1  22779  neiptopnei  23019  neiptopreu  23020  neitr  23067  fiuncmp  23291  iunconnlem  23314  iunconn  23315  2ndcdisj  23343  dissnlocfin  23416  elptr2  23461  ptbasfi  23468  ptcld  23500  ptcldmpt  23501  ptclsg  23502  ptcnplem  23508  ptcnp  23509  cnmpt11  23550  cnmpt21  23558  cnmptcom  23565  imasnopn  23577  imasncld  23578  imasncls  23579  xkocnv  23701  elmptrab  23714  isfildlem  23744  alexsubALTlem3  23936  cnextfvval  23952  utopsnneiplem  24135  isucn2  24166  cfilucfil  24447  blval2  24450  restmetu  24458  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  finiunmbl  25445  volfiniun  25448  iundisj  25449  iunmbl  25454  voliun  25455  iunmbl2  25458  mbfeqalem1  25542  mbfsup  25565  mbfinf  25566  mbflim  25569  itg2splitlem  25649  itg2split  25650  isibl2  25667  cbvitg  25677  itgeqa  25715  itgss3  25716  itgfsum  25728  itgabs  25736  itggt0  25745  itgcn  25746  limcmpt  25784  limciun  25795  dvmptfsum  25879  dvlipcn  25899  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsumrlim  25938  dvfsum2  25941  itgsubst  25956  coeeq2  26147  dgrle  26148  ulmss  26306  leibpi  26852  rlimcnp  26875  rlimcnp2  26876  o1cxp  26885  lgamgulmlem2  26940  lgamgulmlem6  26944  fsumdvdscom  27095  lgseisenlem2  27287  2sqmo  27348  2sqreulem4  27365  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  istrkg2ld  28387  mptelee  28822  gropd  28958  grstructd  28959  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  ex-natded9.26  30348  isch3  31170  atom1d  32282  chirred  32324  sbc2iedf  32394  rspc2daf  32395  19.9d2r  32399  opreu2reuALT  32406  mo5f  32418  reuxfrdf  32420  foresf1o  32433  elabreximdv  32440  iinabrex  32498  cbvdisjf  32500  disjorf  32508  disjabrex  32511  iundisjf  32518  disjunsn  32523  brabgaf  32536  ac6sf2  32548  dfimafnf  32560  2ndresdju  32573  fmptcof2  32581  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  aciunf1  32587  ofpreima  32589  funcnv5mpt  32592  funcnv4mpt  32593  fnpreimac  32595  padct  32643  f1od2  32644  fpwrelmap  32656  xrofsup  32690  iundisjfi  32719  nnindf  32744  nn0min  32745  fprodex01  32750  fsumiunle  32754  prodindf  32786  gsummpt2d  32989  gsummptfsf1o  32994  gsumhashmul  33001  gsumwrd2dccat  33007  elrgspnsubrunlem2  33199  isarchiofld  33295  nsgmgc  33383  nsgqusf1olem1  33384  nsgqusf1olem3  33386  nsgqusf1o  33387  elrspunidl  33399  elrspunsn  33400  ply1gsumz  33564  ig1pmindeg  33567  exsslsb  33592  ply1degltdimlem  33618  fedgmullem2  33626  evls1fldgencl  33665  irngnzply1  33686  ply1annidllem  33691  algextdeglem6  33712  constrfin  33736  reff  33829  locfinreflem  33830  cmpcref  33840  zarclsiin  33861  zarcls  33864  zarcmplem  33871  ordtconnlem1  33914  qqhval2  33972  esumeq12dva  34022  esumeq2dv  34028  esumrnmpt  34042  esumpad  34045  esumpad2  34046  esumadd  34047  gsumesum  34049  esumlub  34050  esumsnf  34054  esumpr  34056  esumrnmpt2  34058  esumfzf  34059  esumfsup  34060  esumpcvgval  34068  esumpmono  34069  esumcocn  34070  hasheuni  34075  esumcvg  34076  esumgect  34080  esum2dlem  34082  esum2d  34083  esumiun  34084  ldsysgenld  34150  sigapildsyslem  34151  sigapildsys  34152  ldgenpisyslem1  34153  fiunelros  34164  measvunilem  34202  measvunilem0  34203  measvuni  34204  measiun  34208  measinblem  34210  voliune  34219  volfiniune  34220  volmeas  34221  ddemeas  34226  oms0  34288  omssubadd  34291  carsgclctunlem1  34308  carsggect  34309  omsmeas  34314  eulerpartlemgvv  34367  dstrvprob  34463  ballotlemodife  34489  reprsuc  34606  reprdifc  34618  breprexplema  34621  breprexplemc  34623  circlemethhgt  34634  hgt750lemd  34639  bnj919  34757  bnj1146  34781  bnj1379  34820  bnj1385  34822  bnj1400  34825  bnj1534  34843  bnj1542  34847  bnj110  34848  bnj121  34860  bnj124  34861  bnj130  34864  bnj207  34871  bnj571  34896  bnj605  34897  bnj580  34903  bnj607  34906  bnj611  34908  bnj873  34914  bnj849  34915  bnj900  34919  bnj916  34923  bnj1000  34931  bnj964  34933  bnj981  34940  bnj985v  34943  bnj985  34944  bnj1014  34951  bnj1123  34976  bnj1128  34980  bnj1228  35001  bnj1204  35002  bnj1279  35008  bnj1307  35013  bnj1321  35017  bnj1388  35023  bnj1398  35024  bnj1408  35026  bnj1417  35031  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1449  35038  bnj1467  35044  bnj1489  35046  bnj1312  35048  bnj1497  35050  bnj1518  35054  bnj1525  35059  bnj1529  35060  dvelimalcased  35065  dvelimexcased  35067  axsepg2  35072  axsepg2ALT  35073  fineqvrep  35085  onvf1odlem2  35091  cvmcov  35250  untsucf  35697  setinds2  35768  dfon2lem1  35771  dfon2lem3  35773  finminlem  36306  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  bj-nexdvt  36686  bj-cbvaldv  36787  bj-cbval2vv  36789  bj-cbvex2vv  36790  bj-cbvaldvav  36791  bj-cbvexdvav  36792  ax11-pm2  36824  bj-dvelimdv  36839  bj-nfeel2  36842  bj-ceqsalv  36882  bj-vtocl  36904  bj-inrab2  36916  currysetlem  36933  currysetlem1  36935  bj-opabco  37176  mptsnunlem  37326  exlimim  37330  exellim  37332  topdifinfindis  37334  topdifinffinlem  37335  icorempo  37339  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  finxpreclem2  37378  finxpreclem6  37384  fvineqsneu  37399  fvineqsneq  37400  wl-euequf  37562  wl-sb8eut  37566  wl-issetft  37570  phpreu  37598  matunitlindflem2  37611  ptrest  37613  ptrecube  37614  poimirlem2  37616  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  heicant  37649  mbfposadd  37661  itgabsnc  37683  itggt0cn  37684  ftc1anclem5  37691  upixp  37723  indexa  37727  indexdom  37728  filbcmb  37734  sdclem2  37736  sdclem1  37737  fdc1  37740  totbndbnd  37783  sbcalf  38108  sbcexf  38109  scottexf  38162  scott0f  38163  eqrelf  38244  fsumshftd  38945  riotasv2d  38950  riotasv2s  38951  riotasv3d  38953  glbconxN  39372  pmapglbx  39763  pmapglb2xN  39766  cdleme26ee  40354  cdleme31sn  40374  cdleme31sn1  40375  cdlemefr29exN  40396  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32fva  40431  cdleme32d  40438  cdleme32f  40440  cdleme40m  40461  cdleme40n  40462  cdleme42b  40472  cdlemk36  40907  cdlemk38  40909  cdlemkid  40930  cdlemk19x  40937  cdlemk11t  40940  dihvalcqpre  41229  mapdheq  41722  hdmap1eq  41795  hdmapval2lem  41825  lcmineqlem9  42025  lcmineqlem12  42028  aks4d1p1p2  42058  mndmolinv  42083  primrootsunit1  42085  primrootsunit  42086  primrootspoweq0  42094  aks6d1c1p5  42100  aks6d1c3  42111  aks6d1c4  42112  aks6d1c1rh  42113  aks6d1c2lem4  42115  aks6d1c2  42118  deg1gprod  42128  sticksstones1  42134  sticksstones11  42144  sticksstones16  42150  sticksstones22  42156  aks6d1c6lem2  42159  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  bcled  42166  bcle2d  42167  aks6d1c7lem3  42170  aks6d1c7  42172  rhmqusspan  42173  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  unitscyglem5  42187  nfa1w  42663  mzpexpmpt  42733  eq0rabdioph  42764  rexrabdioph  42782  rexfrabdioph  42783  elnn0rabdioph  42791  dvdsrabdioph  42798  fphpd  42804  monotuz  42930  monotoddzz  42932  oddcomabszz  42933  setindtr  43013  dford4  43018  wdom2d2  43024  aomclem6  43048  aomclem8  43050  flcidc  43159  areaquad  43205  unielss  43207  onsucf1lem  43258  oaun3lem1  43363  nadd1suc  43381  rababg  43563  ss2iundv  43649  cbviuneq12dv  43651  gneispace  44123  mnringvald  44202  mnringmulrcld  44217  nfscott  44228  scottabf  44229  scottab  44230  mnuprdlem4  44264  ismnushort  44290  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  aaanv  44377  pm11.57  44378  pm11.58  44379  pm11.59  44380  pm11.71  44386  pm14.12  44410  ssralv2  44521  tratrb  44526  iunconnlem2  44924  modelaxreplem3  44970  modelaxrep  44971  permaxrep  44996  evth2f  45009  elunif  45010  fvelrnbf  45012  evthf  45021  fnchoice  45023  sumpair  45029  rfcnnnub  45030  refsum2cn  45032  uzwo4  45047  fiiuncl  45059  fiunicl  45061  elintdv  45073  ssd  45074  cbvmpo2  45091  cbvmpo1  45092  eliin2f  45098  eliuniin2  45114  cbvrabv2  45121  suprnmpt  45168  disjf1  45177  disjrnmpt2  45182  disjf1o  45185  disjinfi  45186  choicefi  45194  iunmapsn  45211  axccdom  45216  dmrelrnrel  45220  axccd  45223  fmptf  45233  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  rnmptbdlem  45249  rnmptbd  45250  fmptff  45263  upbdrech  45303  ssfiunibd  45307  supxrgere  45329  iuneqfzuzlem  45330  supxrgelem  45333  supxrge  45334  suplesup  45335  infrpge  45347  xralrple2  45350  infxr  45363  infxrunb2  45364  infleinf  45368  xrralrecnnle  45379  xrralrecnnge  45386  supxrunb3  45395  supxrleubrnmpt  45402  infleinf2  45410  unb2ltle  45411  rexabslelem  45414  rexabsle  45415  allbutfiinf  45416  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  uzublem  45426  uzub  45427  supminfrnmpt  45441  infxrpnf  45442  supxrleubrnmptf  45447  infxrgelbrnmpt  45450  infrpgernmpt  45461  supminfxr2  45465  monoordxr  45478  monoord2xr  45480  caucvgbf  45485  cvgcaule  45487  rexanuz2nf  45488  iccshift  45516  iooshift  45520  iooiinicc  45540  iooiinioc  45554  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumiunss  45573  fsumreclf  45574  fsumlessf  45575  fsumsermpt  45577  fmul01  45578  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fmul01lt1  45584  fprodsplit1  45591  fprodexp  45592  fprodabs2  45593  mccllem  45595  mccl  45596  fprodcnlem  45597  fprodcn  45598  climexp  45603  climsuse  45606  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  ellimcabssub0  45615  islptre  45617  climf  45620  mullimcf  45621  rexlim2d  45623  idlimc  45624  limcperiod  45626  limcrecl  45627  sumnnodd  45628  islpcn  45637  limsupre  45639  limcleqr  45642  neglimc  45645  addlimc  45646  0ellimcdiv  45647  limclner  45649  climsubmpt  45658  climreclf  45662  climf2  45664  fnlimcnv  45665  climeldmeqmpt  45666  clim2f2  45668  climfveqmpt  45669  fnlimfvre  45672  allbutfifvre  45673  climleltrp  45674  fnlimf  45676  fnlimabslt  45677  climfveqmpt3  45680  climeldmeqf  45681  limsupref  45683  limsupbnd1f  45684  climbddf  45685  climeqf  45686  climeldmeqmpt3  45687  limsuplesup  45697  limsuppnfd  45700  limsupub  45702  limsupres  45703  climinf2lem  45704  climinf2  45705  limsuppnf  45709  limsupubuzlem  45710  limsupubuz  45711  climinf2mpt  45712  climinfmpt  45713  climinf3  45714  limsupmnflem  45718  limsupmnf  45719  limsupequz  45721  limsupre2  45723  limsupmnfuzlem  45724  limsupmnfuz  45725  limsupequzmptf  45729  limsupre3lem  45730  limsupre3  45731  limsupre3uzlem  45733  limsupre3uz  45734  limsupreuz  45735  limsupvaluz2  45736  limsupreuzmpt  45737  supcnvlimsup  45738  climuzlem  45741  climuz  45742  climisp  45744  lmbr3  45745  climrescn  45746  climxrrelem  45747  climxrre  45748  liminfcl  45761  liminfval2  45766  limsup10exlem  45770  liminflelimsuplem  45773  limsupgtlem  45775  limsupgt  45776  climliminflimsupd  45799  liminfreuzlem  45800  liminfreuz  45801  liminfltlem  45802  liminflt  45803  limsupub2  45810  xlimpnfxnegmnf  45812  liminflbuz2  45813  liminfpnfuz  45814  liminflimsupxrre  45815  xlimmnfvlem1  45830  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem1  45834  xlimpnfvlem2  45835  xlimpnfv  45836  xlimmnf  45839  xlimpnf  45840  xlimmnfmpt  45841  xlimpnfmpt  45842  climxlim2lem  45843  dfxlim2  45846  cncfshift  45872  icccncfext  45885  cncficcgt0  45886  cncfiooicc  45892  cncfioobd  45895  fprodcncf  45898  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvmptmulf  45935  dvnmptdivc  45936  dvnmul  45941  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  iblsplitf  45968  iblspltprt  45971  itgioocnicc  45975  iblcncfioo  45976  itgspltprt  45977  itgperiod  45979  stoweidlem3  46001  stoweidlem14  46012  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem26  46024  stoweidlem27  46025  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem36  46034  stoweidlem39  46037  stoweidlem42  46040  stoweidlem43  46041  stoweidlem44  46042  stoweidlem46  46044  stoweidlem48  46046  stoweidlem49  46047  stoweidlem50  46048  stoweidlem51  46049  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem56  46054  stoweidlem57  46055  stoweidlem59  46057  stoweidlem60  46058  stoweidlem61  46059  stoweidlem62  46060  stoweid  46061  wallispilem3  46065  stirlinglem13  46084  stirling  46087  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem31  46136  fourierdlem39  46144  fourierdlem48  46152  fourierdlem51  46155  fourierdlem53  46157  fourierdlem68  46172  fourierdlem69  46173  fourierdlem71  46175  fourierdlem73  46177  fourierdlem77  46181  fourierdlem80  46184  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem86  46190  fourierdlem87  46191  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  elaa2  46232  etransclem18  46250  etransclem22  46254  etransclem23  46255  etransclem32  46264  etransclem35  46267  etransclem44  46276  etransclem46  46278  etransclem48  46280  rrndistlt  46288  ioorrnopnlem  46302  saliuncl  46321  saliincl  46325  intsaluni  46327  salexct  46332  subsaliuncl  46356  sge00  46374  sge0revalmpt  46376  sge0sn  46377  sge0f1o  46380  sge0gerp  46393  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resrnlem  46401  sge0resplit  46404  sge0lempt  46408  sge0iunmptlemfi  46411  sge0p1  46412  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0iunmpt  46416  sge0rpcpnf  46419  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xp  46427  sge0ad2en  46429  sge0isummpt2  46430  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0xadd  46433  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  sge0reuzb  46446  iundjiun  46458  meadjiunlem  46463  meadjiun  46464  ismeannd  46465  voliunsge0lem  46470  meaiuninclem  46478  meaiunincf  46481  meaiuninc3v  46482  meaiuninc3  46483  meaiininclem  46484  meaiininc  46485  meaiininc2  46486  caragenfiiuncl  46513  omeiunltfirp  46517  carageniuncllem1  46519  carageniuncllem2  46520  caratheodorylem2  46525  0ome  46527  isomenndlem  46528  hoicvrrex  46554  ovnsupge0  46555  ovnlecvr  46556  ovnlerp  46560  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  ovnsubaddlem2  46569  hoidmvcl  46580  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmvval0  46585  sge0hsphoire  46587  hoidmvval0b  46588  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem1  46599  ovnhoilem2  46600  ovnhoi  46601  ovnlecvr2  46608  hspdifhsp  46614  hoidifhspdmvle  46618  hoiqssbllem3  46622  hspmbllem1  46624  hspmbllem2  46625  opnvonmbllem1  46630  opnvonmbllem2  46631  ovnsubadd2lem  46643  ovolval5lem1  46650  ovnovollem1  46654  ovnovollem2  46655  hoimbl2  46663  vonhoire  46670  iinhoiicclem  46671  iinhoiicc  46672  iunhoiioolem  46673  iunhoiioo  46674  vonioolem1  46678  vonioolem2  46679  vonioo  46680  vonicclem1  46681  vonicclem2  46682  vonicc  46683  vonn0ioo2  46688  vonn0icc2  46690  vonct  46691  pimltmnf2f  46695  pimgtpnf2f  46703  salpreimagelt  46705  salpreimalegt  46707  pimltpnf2f  46710  pimgtmnf2  46712  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  salpreimagtge  46723  salpreimaltle  46724  salpreimalelt  46727  salpreimagtlt  46728  issmff  46732  sssmf  46736  mbfresmf  46737  cnfsmf  46738  incsmflem  46739  incsmf  46740  smfsssmf  46741  issmflelem  46742  issmfle  46743  smfconst  46747  issmfgtlem  46753  issmfgt  46754  smfpimltxrmptf  46756  smfmbfcex  46758  smfaddlem1  46761  smfaddlem2  46762  smfadd  46763  decsmflem  46764  decsmf  46765  smfpreimagtf  46766  issmfgelem  46767  issmfge  46768  smflimlem2  46770  smflimlem4  46772  smflim  46775  smfpimgtxr  46778  smfpimgtxrmptf  46782  smfpimioo  46785  smfresal  46786  smfrec  46787  smfres  46788  smfmullem2  46790  smfmullem4  46792  smfmul  46793  smfpimbor1lem2  46797  smf2id  46799  smfco  46800  smflim2  46804  smfpimcc  46806  smflimmpt  46808  smfsuplem1  46809  smfsuplem3  46811  smfsup  46812  smfsupmpt  46813  smfsupxr  46814  smfinflem  46815  smfinf  46816  smfinfmpt  46817  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  smflimsuplem8  46825  smflimsup  46826  smflimsupmpt  46827  smfliminflem  46828  smfliminf  46829  smfliminfmpt  46830  smfpimne2  46838  fsupdm  46840  smfsupdmmbllem  46842  smfsupdmmbl  46843  finfdm  46844  smfinfdmmbllem  46846  smfinfdmmbl  46847  or2expropbilem1  47033  or2expropbilem2  47034  or2expropbi  47035  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  rexsb  47100  reuf1odnf  47108  2reu8i  47114  ffnafv  47172  tz6.12c-afv2  47243  f1oresf1o2  47292  iccelpart  47434  iccpartdisj  47438  dfich2  47459  ichbi12i  47461  ichnfimlem  47464  ich2exprop  47472  ichnreuop  47473  ichreuopeq  47474  sprsymrelfo  47498  reupr  47523  reuopreuprim  47527  mogoldbb  47786  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