Theorem nfv 1936

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

Syntax hints:  Ⅎwnf 1805

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

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-nf 1806

This theorem is referenced by:  nfvd  1937  cbvaldw  2371  cbval2v  2376  dvelimhw  2378  pm11.53  2379  19.12vv  2380  eeanv  2382  eeeanv  2383  ee4anv  2384  sbnf2  2391  exsb  2392  2exsb  2393  sbbibvv  2395  cbvsbvf  2396  cleljustALT2  2398  spimv  2423  spimev  2425  chvarv  2429  cbvalv  2433  cbvexv  2434  cbvald  2440  cbvaldva  2442  cbvexdva  2443  cbval2  2444  axc16i  2469  dvelimnf  2486  sbel2x  2507  sbiedv  2537  2sbiev  2538  sbid2v  2542  sbhb  2554  2sb8e  2563  nfmod2  2587  nfmodv  2588  mof  2592  mo4f  2596  euf  2605  sb8eulem  2627  cbvmow  2632  sbmo  2643  moexexvw  2657  moexexv  2668  2mo  2677  2eu6  2685  axextmo  2740  nulmo  2741  abbib  2833  cleqh  2893  nfcv  2926  nfeqd  2936  nfeld  2937  nfabdw  2947  nfabd  2948  dvelimdc  2950  nfcvf  2952  cleqf  2954  r19.29af  3273  rexbidvALT  3279  rexbidvaALT  3280  2ralbida  3287  r19.12  3313  reean  3314  cbvrexsvw  3316  cbvralsvwOLD  3317  sbralieOLD  3344  cbvralf  3349  cbvralv  3353  cbvrexv  3354  cbvralsv  3355  cbvrexsv  3356  cbvrmow  3394  cbvreu  3408  cbvrmov  3410  cbvreuv  3411  cbvrabwOLD  3452  cbvrab  3455  cbvexeqsetf  3471  ceqsex2  3506  vtocl2gaf  3545  vtocl3gaf  3546  spc2ed  3562  rspct  3569  rspc  3571  rspce  3572  eqvincf  3611  elrab3t  3651  ralab2  3662  rexab2  3664  mob2  3680  mob  3682  reu2  3690  rmo4f  3700  reu2eqd  3701  cdeqab1  3737  nfcdeq  3742  sbcco  3772  cbvsbcv  3782  elrabsf  3791  sbc2iegf  3820  reu8nf  3832  rmo2  3842  rmo3  3844  rmoanimALT  3850  nfcsb1d  3876  nfcsbd  3879  csbiebt  3883  csbie2t  3892  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  cbvralv2  3900  cbvrexv2  3901  rspc2vd  3902  dfssf  3929  rabss3d  4036  eqrrabd  4041  uniiunlem  4042  ab0orv  4338  ab0orvALT  4339  sbcnestgw  4379  sbcnestg  4384  sbnfc2  4395  r19.3rzvOLD  4460  r19.28zv  4462  r19.27zv  4467  2reu4lem  4479  nfifd  4512  reusngf  4635  reusng  4638  rexreusng  4640  reuprg0  4663  rabsnifsb  4683  euabsn  4687  nfunid  4873  eluniab  4881  nfint  4917  iuneqconst  4963  disjiun  5090  disjxun  5100  nfopabd  5170  cbvopab  5174  cbvopab1  5176  cbvopab1g  5177  cbvopab2  5178  cbvopab1s  5179  mpteq12da  5185  mpteq12f  5187  cbvmptf  5202  cbvmptfg  5203  axrep1  5230  axrep2  5232  axrep3  5233  axrep4OLD  5236  axrep5  5237  zfrepclf  5243  reusv2lem3  5359  reusv2lem4  5360  reusv2  5362  reusv3  5364  alxfr  5366  ralxfrALT  5374  axprlem3OLD  5388  axprlem4OLD  5389  axprlem5OLD  5390  copsex2t  5463  iunopeqop  5492  iunopeqopOLD  5493  rexopabb  5500  opelopabaf  5517  nfso  5564  pofun  5575  isso2i  5594  nffr  5622  opeliunxp  5716  opeliun2xp  5717  opeliunxp2  5812  ralxpf  5820  dfdmf  5874  dfrnf  5928  elrnmpt1  5938  dfrel4  6179  reuop  6282  frpoinsg  6332  frpoins2g  6334  wfis2g  6344  nfiotadw  6482  nfiotad  6484  cbviotaw  6486  cbviota  6488  cbviotav  6489  sb8iota  6490  iota2d  6511  iota2  6512  dffun6f  6538  imadif  6607  isarep1  6612  isarep2  6613  fv3  6887  tz6.12f  6894  funimassd  6935  fvelimad  6936  feqmptdf  6939  fimarab  6943  opabiotafun  6949  funfv2f  6958  fvmptd  6985  fvmptd2f  6994  fvmptdv  6995  fvmptt  6998  fvopab5  7011  eqfnfv2f  7017  ralrnmptw  7077  ralrnmpt  7079  dffo3f  7089  f1ompt  7094  fompt  7101  ffnfv  7102  ffnfvf  7103  f1ossf1o  7112  fmptco  7113  elabrex  7228  elabrexg  7229  dff13f  7241  fsnex  7269  fliftfun  7298  cbvriotaw  7364  cbvriota  7368  cbvriotav  7369  riota2  7380  riotaeqimp  7381  riota5f  7383  oprabv  7458  nfoprab  7462  mpoeq123  7470  cbvoprab1  7485  cbvoprab2  7486  cbvoprab12  7487  cbvoprab3  7489  cbvmpox  7491  ralrnmpo  7537  ovmpodx  7549  ovmpodf  7554  ovmpodv  7555  ov3  7561  ovmpt3rab1  7656  ofrfval2  7683  onminex  7787  tfis  7837  tfis2  7839  tfisi  7841  tfinds  7842  tfindes  7845  findes  7883  fiun  7926  f1iun  7927  abrexex2g  7947  opabex3d  7948  opabex3rd  7949  opabex3  7950  dfoprab4f  8039  fmpox  8050  offval22  8069  ovmptss  8074  ralxpes  8118  ralxp3  8120  ralxp3es  8121  frpoins3xpg  8122  frpoins3xp3g  8123  opeliunxp2f  8192  tposoprab  8244  fvmpocurryd  8253  nffrecs  8266  tfr3  8372  nfrdg  8387  tz7.48-1  8416  tz7.49  8418  naddsuc2  8674  eqerlem  8716  erovlem  8797  mptelixpg  8919  boxcutc  8925  dom2lem  8975  xpf1o  9113  mapxpen  9117  findcard2  9135  pssnn  9139  nneneq  9176  ac6sfi  9230  fiint  9273  indexfi  9305  wdom2d  9530  ixpiunwdom  9540  cantnflem1  9646  nfttrcld  9667  setinds2  9708  frinsg  9711  frins2  9714  r1val1  9746  rankuni2b  9813  scottexs  9847  scott0s  9848  dfac8clem  9990  acni2  10004  aceq1  10075  dfac5lem5  10085  kmlem15  10123  infpssrlem4  10265  fin23lem27  10287  hsmexlem2  10386  hsmexlem4  10388  axcc3  10397  domtriomlem  10401  axdc3lem2  10410  axdc3lem4  10412  axdc4lem  10414  ac6c4  10440  zorn2lem4  10458  zorn2lem5  10459  iunfo  10498  iundom2g  10499  uniimadomf  10504  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  11348  dedekindle  11349  fimaxre3  12140  nn0ind-raph  12675  uzind4s  12911  nnwof  12917  lbzbi  12939  fzrevral  13619  rabssnn0fi  14001  fsuppmapnn0fiublem  14005  fsuppmapnn0fiub  14006  fsuppmapnn0fiubex  14007  seqof2  14075  reuccatpfxs1  14762  cotr2g  14991  rlim2  15525  ello1mpt  15550  climeu  15584  o1compt  15616  summolem2a  15744  zsum  15747  sumss  15753  sumss2  15755  fsumcvg2  15756  fsumclf  15767  fsumsplitf  15771  fsumsplit1  15774  fsum2dlem  15799  fsum00  15828  o1fsum  15843  nfcprod1  15940  nfcprod  15941  prodmolem2a  15966  zprod  15969  fprod  15973  fprodntriv  15974  prodss  15979  fprodn0  16011  fprod2dlem  16012  fprodsplitf  16020  fprodsplit1f  16022  fprodle  16028  fprodmodd  16029  lcmfunsnlem1  16673  lcmfunsnlem2lem1  16674  lcmfunsnlem2  16676  coprmprod  16697  coprmproddvdslem  16698  prmind2  16721  iserodd  16873  pcmpt  16930  pcmptdvds  16932  prmolefac  17084  mreexexd  17682  catpropd  17743  invfuc  18012  natpropd  18014  fucpropd  18015  initoeu2  18051  acsmapd  18588  nfchnd  18645  symgval  19413  gsumsnd  19994  gsumsnf  19995  gsumunsnfd  19999  gsummptf1o  20005  gsummpt1n0  20007  gsum2d2lem  20015  gsumcom2  20017  gsummptnn0fz  20028  dprd2d2  20088  rngqiprngimf1  21372  gsummoncoe1  22373  gsumply1eq  22374  mdetralt2  22671  mdetunilem2  22675  madugsum  22705  gsummatr01lem4  22720  cpmatmcllem  22780  cayleyhamilton1  22954  neiptopnei  23194  neiptopreu  23195  neitr  23242  fiuncmp  23466  iunconnlem  23489  iunconn  23490  2ndcdisj  23518  dissnlocfin  23591  elptr2  23636  ptbasfi  23643  ptcld  23675  ptcldmpt  23676  ptclsg  23677  ptcnplem  23683  ptcnp  23684  cnmpt11  23725  cnmpt21  23733  cnmptcom  23740  imasnopn  23752  imasncld  23753  imasncls  23754  xkocnv  23876  elmptrab  23889  isfildlem  23919  alexsubALTlem3  24111  cnextfvval  24127  utopsnneiplem  24309  isucn2  24340  cfilucfil  24621  blval2  24624  restmetu  24632  ovoliunlem3  25568  ovoliun  25569  ovoliun2  25570  ovoliunnul  25571  finiunmbl  25608  volfiniun  25611  iundisj  25612  iunmbl  25617  voliun  25618  iunmbl2  25621  mbfeqalem1  25705  mbfsup  25728  mbfinf  25729  mbflim  25732  itg2splitlem  25812  itg2split  25813  isibl2  25830  cbvitg  25840  itgeqa  25878  itgss3  25879  itgfsum  25891  itgabs  25899  itggt0  25908  itgcn  25909  limcmpt  25947  limciun  25958  dvmptfsum  26039  dvlipcn  26058  dvfsumlem2  26091  dvfsumlem4  26093  dvfsumrlim  26095  dvfsum2  26098  itgsubst  26113  coeeq2  26304  dgrle  26305  ulmss  26462  leibpi  27009  rlimcnp  27032  rlimcnp2  27033  o1cxp  27041  lgamgulmlem2  27096  lgamgulmlem6  27100  fsumdvdscom  27251  lgseisenlem2  27442  2sqmo  27503  2sqreulem4  27520  dchrisumlema  27554  dchrisumlem2  27556  dchrisumlem3  27557  nosupbnd1  27780  nosupbnd2  27782  noinfbnd1  27795  noinfbnd2  27797  bdayiun  28010  bdaypw2n0bndlem  28558  istrkg2ld  28631  mpteleeOLD  29098  gropd  29234  grstructd  29235  clwwlknonclwlknonf1o  30566  dlwwlknondlwlknonf1o  30569  ex-natded9.26  30623  isch3  31446  atom1d  32558  chirred  32600  sbc2iedf  32667  rspc2daf  32668  19.9d2r  32672  opreu2reuALT  32678  mo5f  32690  reuxfrdf  32692  foresf1o  32705  elabreximdv  32712  iinabrex  32771  cbvdisjf  32773  disjorf  32781  disjabrex  32784  iundisjf  32791  disjunsn  32796  brabgaf  32810  ac6sf2  32826  dfimafnf  32840  2ndresdju  32853  fmptcof2  32861  acunirnmpt2  32864  acunirnmpt2f  32865  aciunf1lem  32866  aciunf1  32867  ofpreima  32869  funcnv5mpt  32871  funcnv4mpt  32872  fnpreimac  32874  f1od2  32923  fpwrelmap  32937  xrofsup  32971  iundisjfi  33000  nnindf  33024  nn0min  33025  fprodex01  33029  fsumiunle  33033  prodindf  33042  gsummpt2d  33231  gsummptf1od  33237  gsummptfsf1o  33242  gsumhashmul  33249  suppgsumssiun  33254  gsumwrd2dccat  33260  isarchiofld  33381  elrgspnsubrunlem2  33431  nsgmgc  33600  nsgqusf1olem1  33601  nsgqusf1olem3  33603  nsgqusf1o  33604  elrspunidl  33616  elrspunsn  33617  deg1prod  33781  ply1gsumz  33797  ig1pmindeg  33800  mplvrpmga  33844  psrgsum  33847  psrmonprod  33851  esplylem  33865  esplyfv1  33868  esplyfval1  33872  esplyfvaln  33873  esplyind  33874  vieta  33879  exsslsb  33896  ply1degltdimlem  33921  fedgmullem2  33929  evls1fldgencl  33969  irngnzply1  33990  extdgfialglem2  33992  ply1annidllem  34000  algextdeglem6  34021  constrfin  34045  reff  34138  locfinreflem  34139  cmpcref  34149  zarclsiin  34170  zarcls  34173  zarcmplem  34180  ordtconnlem1  34223  qqhval2  34281  esumeq12dva  34331  esumeq2dv  34337  esumrnmpt  34351  esumpad  34354  esumpad2  34355  esumadd  34356  gsumesum  34358  esumlub  34359  esumsnf  34363  esumpr  34365  esumrnmpt2  34367  esumfzf  34368  esumfsup  34369  esumpcvgval  34377  esumpmono  34378  esumcocn  34379  hasheuni  34384  esumcvg  34385  esumgect  34389  esum2dlem  34391  esum2d  34392  esumiun  34393  ldsysgenld  34459  sigapildsyslem  34460  sigapildsys  34461  ldgenpisyslem1  34462  fiunelros  34473  measvunilem  34511  measvunilem0  34512  measvuni  34513  measiun  34517  measinblem  34519  voliune  34528  volfiniune  34529  volmeas  34530  ddemeas  34535  oms0  34596  omssubadd  34599  carsgclctunlem1  34616  carsggect  34617  omsmeas  34622  eulerpartlemgvv  34675  dstrvprob  34771  ballotlemodife  34797  reprsuc  34911  reprdifc  34923  breprexplema  34926  breprexplemc  34928  circlemethhgt  34939  hgt750lemd  34944  bnj919  35065  bnj1146  35088  bnj1379  35127  bnj1385  35129  bnj1400  35132  bnj1534  35150  bnj1542  35154  bnj110  35155  bnj121  35167  bnj124  35168  bnj130  35171  bnj207  35178  bnj571  35203  bnj605  35204  bnj580  35210  bnj607  35213  bnj611  35215  bnj873  35221  bnj849  35222  bnj900  35226  bnj916  35230  bnj1000  35238  bnj964  35240  bnj981  35247  bnj985v  35250  bnj985  35251  bnj1014  35258  bnj1123  35283  bnj1128  35287  bnj1228  35308  bnj1204  35309  bnj1279  35315  bnj1307  35320  bnj1321  35324  bnj1388  35330  bnj1398  35331  bnj1408  35333  bnj1417  35338  bnj1444  35340  bnj1445  35341  bnj1446  35342  bnj1449  35345  bnj1467  35351  bnj1489  35353  bnj1312  35355  bnj1497  35357  bnj1518  35361  bnj1525  35366  bnj1529  35367  dvelimalcased  35372  dvelimexcased  35374  fineqvrep  35414  axsepg2  35440  axsepg3  35441  axsepg3ALT  35442  axpowg2  35447  axpowg3  35448  onvf1odlem2  35451  cvmcov  35618  untsucf  36065  dfon2lem1  36136  dfon2lem3  36138  finminlem  36683  weiunpo  36830  weiunso  36831  weiunfr  36832  weiunse  36833  axtcond  36843  regsfromregtco  36903  regsfromsetind  36904  bj-nexdvt  37178  bj-cbvaldv  37289  bj-cbval2vv  37291  bj-cbvex2vv  37292  bj-cbvaldvav  37293  bj-cbvexdvav  37294  ax11-pm2  37326  bj-dvelimdv  37341  bj-nfeel2  37344  bj-ceqsalv  37384  bj-vtocl  37406  bj-inrab2  37418  currysetlem  37435  currysetlem1  37437  bj-axseprep  37564  bj-axreprepsep  37565  bj-opabco  37685  mptsnunlem  37837  exlimim  37841  exellim  37843  topdifinfindis  37845  topdifinffinlem  37846  icorempo  37850  isbasisrelowllem1  37854  isbasisrelowllem2  37855  relowlssretop  37862  finxpreclem2  37889  finxpreclem6  37895  fvineqsneu  37910  fvineqsneq  37911  wl-euequf  38082  wl-sb8eut  38086  wl-issetft  38090  phpreu  38108  matunitlindflem2  38121  ptrest  38123  ptrecube  38124  poimirlem2  38126  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  heicant  38159  mbfposadd  38171  itgabsnc  38193  itggt0cn  38194  ftc1anclem5  38201  upixp  38233  indexa  38237  indexdom  38238  filbcmb  38244  sdclem2  38246  sdclem1  38247  fdc1  38250  totbndbnd  38293  sbcalf  38618  sbcexf  38619  scottexf  38672  scott0f  38673  eqrelf  38762  ralrmo3  38868  disjqmap2  39330  fsumshftd  39581  riotasv2d  39586  riotasv2s  39587  riotasv3d  39589  glbconxN  40007  pmapglbx  40398  pmapglb2xN  40401  cdleme26ee  40989  cdleme31sn  41009  cdleme31sn1  41010  cdlemefr29exN  41031  cdlemefs32sn1aw  41043  cdleme43fsv1snlem  41049  cdleme41sn3a  41062  cdleme32fva  41066  cdleme32d  41073  cdleme32f  41075  cdleme40m  41096  cdleme40n  41097  cdleme42b  41107  cdlemk36  41542  cdlemk38  41544  cdlemkid  41565  cdlemk19x  41572  cdlemk11t  41575  dihvalcqpre  41864  mapdheq  42357  hdmap1eq  42430  hdmapval2lem  42460  lcmineqlem9  42659  lcmineqlem12  42662  aks4d1p1p2  42692  mndmolinv  42717  primrootsunit1  42719  primrootsunit  42720  primrootspoweq0  42728  aks6d1c1p5  42734  aks6d1c3  42745  aks6d1c4  42746  aks6d1c1rh  42747  aks6d1c2lem4  42749  aks6d1c2  42752  deg1gprod  42762  sticksstones1  42768  sticksstones11  42778  sticksstones16  42784  sticksstones22  42790  aks6d1c6lem2  42793  aks6d1c6isolem1  42796  aks6d1c6isolem2  42797  bcled  42800  bcle2d  42801  aks6d1c7lem3  42804  aks6d1c7  42806  rhmqusspan  42807  grpods  42816  unitscyglem1  42817  unitscyglem2  42818  unitscyglem3  42819  unitscyglem4  42820  unitscyglem5  42821  nfa1w  43262  mzpexpmpt  43331  eq0rabdioph  43362  rexrabdioph  43376  rexfrabdioph  43377  elnn0rabdioph  43385  dvdsrabdioph  43392  fphpd  43398  monotuz  43523  monotoddzz  43525  oddcomabszz  43526  setindtr  43606  dford4  43611  wdom2d2  43617  aomclem6  43641  aomclem8  43643  flcidc  43752  areaquad  43798  unielss  43800  onsucf1lem  43851  oaun3lem1  43956  nadd1suc  43974  rababg  44155  ss2iundv  44241  cbviuneq12dv  44243  gneispace  44715  mnringvald  44794  mnringmulrcld  44809  nfscott  44820  scottabf  44821  scottab  44822  mnuprdlem4  44856  ismnushort  44882  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  aaanv  44969  pm11.57  44970  pm11.58  44971  pm11.59  44972  pm11.71  44978  pm14.12  45002  ssralv2  45112  tratrb  45117  iunconnlem2  45515  modelaxreplem3  45561  modelaxrep  45562  permaxrep  45587  evth2f  45600  elunif  45601  fvelrnbf  45603  evthf  45612  fnchoice  45614  sumpair  45620  rfcnnnub  45621  refsum2cn  45623  uzwo4  45638  fiiuncl  45650  fiunicl  45652  elintdv  45664  ssd  45665  cbvmpo2  45680  cbvmpo1  45681  eliin2f  45687  eliuniin2  45703  cbvrabv2  45710  suprnmpt  45757  disjf1  45766  disjrnmpt2  45771  disjf1o  45774  disjinfi  45775  choicefi  45782  iunmapsn  45798  axccdom  45803  dmrelrnrel  45807  axccd  45809  fmptf  45819  rnmptlb  45823  rnmptbddlem  45824  rnmptbd2lem  45828  rnmptbdlem  45835  rnmptbd  45836  fmptff  45849  upbdrech  45889  ssfiunibd  45893  supxrgere  45914  iuneqfzuzlem  45915  supxrgelem  45918  supxrge  45919  suplesup  45920  infrpge  45932  xralrple2  45935  infxr  45947  infxrunb2  45948  infleinf  45952  xrralrecnnle  45963  xrralrecnnge  45970  supxrunb3  45979  supxrleubrnmpt  45985  infleinf2  45993  unb2ltle  45994  rexabslelem  45997  rexabsle  45998  allbutfiinf  45999  suprleubrnmpt  46001  infrnmptle  46002  infxrunb3rnmpt  46007  uzublem  46009  uzub  46010  supminfrnmpt  46024  infxrpnf  46025  supxrleubrnmptf  46030  infxrgelbrnmpt  46033  infrpgernmpt  46044  supminfxr2  46048  monoordxr  46061  monoord2xr  46063  caucvgbf  46068  cvgcaule  46070  rexanuz2nf  46071  iccshift  46099  iooshift  46103  iooiinicc  46123  iooiinioc  46137  fsummulc1f  46152  fsumnncl  46153  fsumf1of  46155  fsumiunss  46156  fsumreclf  46157  fsumlessf  46158  fsumsermpt  46160  fmul01  46161  fmuldfeqlem1  46163  fmuldfeq  46164  fmul01lt1lem1  46165  fmul01lt1lem2  46166  fmul01lt1  46167  fprodsplit1  46174  fprodexp  46175  fprodabs2  46176  mccllem  46178  mccl  46179  fprodcnlem  46180  fprodcn  46181  climexp  46186  climsuse  46189  climrecf  46190  climinff  46192  climaddf  46196  mullimc  46197  ellimcabssub0  46198  islptre  46200  climf  46203  mullimcf  46204  rexlim2d  46206  idlimc  46207  limcperiod  46209  limcrecl  46210  sumnnodd  46211  islpcn  46218  limsupre  46220  limcleqr  46223  neglimc  46226  addlimc  46227  0ellimcdiv  46228  limclner  46230  climsubmpt  46239  climreclf  46243  climf2  46245  fnlimcnv  46246  climeldmeqmpt  46247  clim2f2  46249  climfveqmpt  46250  fnlimfvre  46253  allbutfifvre  46254  climleltrp  46255  fnlimf  46257  fnlimabslt  46258  climfveqmpt3  46261  climeldmeqf  46262  limsupref  46264  limsupbnd1f  46265  climbddf  46266  climeqf  46267  climeldmeqmpt3  46268  limsuplesup  46278  limsuppnfd  46281  limsupub  46283  limsupres  46284  climinf2lem  46285  climinf2  46286  limsuppnf  46290  limsupubuzlem  46291  limsupubuz  46292  climinf2mpt  46293  climinfmpt  46294  climinf3  46295  limsupmnflem  46299  limsupmnf  46300  limsupequz  46302  limsupre2  46304  limsupmnfuzlem  46305  limsupmnfuz  46306  limsupequzmptf  46310  limsupre3lem  46311  limsupre3  46312  limsupre3uzlem  46314  limsupre3uz  46315  limsupreuz  46316  limsupvaluz2  46317  limsupreuzmpt  46318  supcnvlimsup  46319  climuzlem  46322  climuz  46323  climisp  46325  lmbr3  46326  climrescn  46327  climxrrelem  46328  climxrre  46329  liminfcl  46342  liminfval2  46347  limsup10exlem  46351  liminflelimsuplem  46354  limsupgtlem  46356  limsupgt  46357  climliminflimsupd  46380  liminfreuzlem  46381  liminfreuz  46382  liminfltlem  46383  liminflt  46384  limsupub2  46391  xlimpnfxnegmnf  46393  liminflbuz2  46394  liminfpnfuz  46395  liminflimsupxrre  46396  xlimmnfvlem1  46411  xlimmnfvlem2  46412  xlimmnfv  46413  xlimpnfvlem1  46415  xlimpnfvlem2  46416  xlimpnfv  46417  xlimmnf  46420  xlimpnf  46421  xlimmnfmpt  46422  xlimpnfmpt  46423  climxlim2lem  46424  dfxlim2  46427  cncfshift  46453  icccncfext  46466  cncficcgt0  46467  cncfiooicc  46473  cncfioobd  46476  fprodcncf  46479  fprodsubrecnncnvlem  46486  fprodaddrecnncnvlem  46488  dvmptmulf  46516  dvnmptdivc  46517  dvnmul  46522  dvmptfprodlem  46523  dvmptfprod  46524  dvnprodlem1  46525  dvnprodlem2  46526  iblsplitf  46549  iblspltprt  46552  itgioocnicc  46556  iblcncfioo  46557  itgspltprt  46558  itgperiod  46560  stoweidlem3  46582  stoweidlem14  46593  stoweidlem17  46596  stoweidlem19  46598  stoweidlem20  46599  stoweidlem26  46605  stoweidlem27  46606  stoweidlem28  46607  stoweidlem29  46608  stoweidlem31  46610  stoweidlem34  46613  stoweidlem35  46614  stoweidlem36  46615  stoweidlem39  46618  stoweidlem42  46621  stoweidlem43  46622  stoweidlem44  46623  stoweidlem46  46625  stoweidlem48  46627  stoweidlem49  46628  stoweidlem50  46629  stoweidlem51  46630  stoweidlem52  46631  stoweidlem53  46632  stoweidlem54  46633  stoweidlem56  46635  stoweidlem57  46636  stoweidlem59  46638  stoweidlem60  46639  stoweidlem61  46640  stoweidlem62  46641  stoweid  46642  wallispilem3  46646  stirlinglem13  46665  stirling  46668  fourierdlem16  46702  fourierdlem21  46707  fourierdlem22  46708  fourierdlem31  46717  fourierdlem39  46725  fourierdlem48  46733  fourierdlem51  46736  fourierdlem53  46738  fourierdlem68  46753  fourierdlem69  46754  fourierdlem71  46756  fourierdlem73  46758  fourierdlem77  46762  fourierdlem80  46765  fourierdlem81  46766  fourierdlem82  46767  fourierdlem83  46768  fourierdlem86  46771  fourierdlem87  46772  fourierdlem89  46774  fourierdlem91  46776  fourierdlem93  46778  fourierdlem94  46779  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  fourierdlem113  46798  elaa2  46813  etransclem18  46831  etransclem22  46835  etransclem23  46836  etransclem32  46845  etransclem35  46848  etransclem44  46857  etransclem46  46859  etransclem48  46861  rrndistlt  46869  ioorrnopnlem  46883  saliuncl  46902  saliincl  46906  intsaluni  46908  salexct  46913  subsaliuncl  46937  sge00  46955  sge0revalmpt  46957  sge0sn  46958  sge0f1o  46961  sge0gerp  46974  sge0pnffigt  46975  sge0lefi  46977  sge0ltfirp  46979  sge0resrnlem  46982  sge0resplit  46985  sge0lempt  46989  sge0iunmptlemfi  46992  sge0p1  46993  sge0iunmptlemre  46994  sge0fodjrnlem  46995  sge0iunmpt  46997  sge0rpcpnf  47000  sge0ltfirpmpt2  47005  sge0isum  47006  sge0xp  47008  sge0ad2en  47010  sge0isummpt2  47011  sge0xaddlem1  47012  sge0xaddlem2  47013  sge0xadd  47014  sge0pnffsumgt  47021  sge0gtfsumgt  47022  sge0uzfsumgt  47023  sge0seq  47025  sge0reuz  47026  sge0reuzb  47027  iundjiun  47039  meadjiunlem  47044  meadjiun  47045  ismeannd  47046  voliunsge0lem  47051  meaiuninclem  47059  meaiunincf  47062  meaiuninc3v  47063  meaiuninc3  47064  meaiininclem  47065  meaiininc  47066  meaiininc2  47067  caragenfiiuncl  47094  omeiunltfirp  47098  carageniuncllem1  47100  carageniuncllem2  47101  caratheodorylem2  47106  0ome  47108  isomenndlem  47109  hoicvrrex  47135  ovnsupge0  47136  ovnlecvr  47137  ovnlerp  47141  ovncvrrp  47143  ovn0lem  47144  ovnsubaddlem1  47149  ovnsubaddlem2  47150  hoidmvcl  47161  hsphoidmvle2  47164  hsphoidmvle  47165  hoidmvval0  47166  sge0hsphoire  47168  hoidmvval0b  47169  hoidmv1lelem1  47170  hoidmv1lelem2  47171  hoidmv1lelem3  47172  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvlelem4  47177  hoidmvlelem5  47178  hoidmvle  47179  ovnhoilem1  47180  ovnhoilem2  47181  ovnhoi  47182  ovnlecvr2  47189  hspdifhsp  47195  hoidifhspdmvle  47199  hoiqssbllem3  47203  hspmbllem1  47205  hspmbllem2  47206  opnvonmbllem1  47211  opnvonmbllem2  47212  ovnsubadd2lem  47224  ovolval5lem1  47231  ovnovollem1  47235  ovnovollem2  47236  hoimbl2  47244  vonhoire  47251  iinhoiicclem  47252  iinhoiicc  47253  iunhoiioolem  47254  iunhoiioo  47255  vonioolem1  47259  vonioolem2  47260  vonioo  47261  vonicclem1  47262  vonicclem2  47263  vonicc  47264  vonn0ioo2  47269  vonn0icc2  47271  vonct  47272  pimltmnf2f  47276  pimgtpnf2f  47284  salpreimagelt  47286  salpreimalegt  47288  pimltpnf2f  47291  pimgtmnf2  47293  pimdecfgtioc  47294  pimincfltioc  47295  pimdecfgtioo  47296  pimincfltioo  47297  preimageiingt  47299  preimaleiinlt  47300  salpreimagtge  47304  salpreimaltle  47305  salpreimalelt  47308  salpreimagtlt  47309  issmff  47313  sssmf  47317  mbfresmf  47318  cnfsmf  47319  incsmflem  47320  incsmf  47321  smfsssmf  47322  issmflelem  47323  issmfle  47324  smfconst  47328  issmfgtlem  47334  issmfgt  47335  smfpimltxrmptf  47337  smfmbfcex  47339  smfaddlem1  47342  smfaddlem2  47343  smfadd  47344  decsmflem  47345  decsmf  47346  smfpreimagtf  47347  issmfgelem  47348  issmfge  47349  smflimlem2  47351  smflimlem4  47353  smflim  47356  smfpimgtxr  47359  smfpimgtxrmptf  47363  smfpimioo  47366  smfresal  47367  smfrec  47368  smfres  47369  smfmullem2  47371  smfmullem4  47373  smfmul  47374  smfpimbor1lem2  47378  smf2id  47380  smfco  47381  smflim2  47385  smfpimcc  47387  smflimmpt  47389  smfsuplem1  47390  smfsuplem3  47392  smfsup  47393  smfsupmpt  47394  smfsupxr  47395  smfinflem  47396  smfinf  47397  smfinfmpt  47398  smflimsuplem3  47401  smflimsuplem4  47402  smflimsuplem5  47403  smflimsuplem7  47405  smflimsuplem8  47406  smflimsup  47407  smflimsupmpt  47408  smfliminflem  47409  smfliminf  47410  smfliminfmpt  47411  smfpimne2  47419  fsupdm  47421  smfsupdmmbllem  47423  smfsupdmmbl  47424  finfdm  47425  smfinfdmmbllem  47427  smfinfdmmbl  47428  or2expropbilem1  47631  or2expropbilem2  47632  or2expropbi  47633  cfsetsnfsetf  47657  cfsetsnfsetfo  47659  rexsb  47698  reuf1odnf  47706  2reu8i  47712  ffnafv  47770  tz6.12c-afv2  47841  f1oresf1o2  47890  iccelpart  48044  iccpartdisj  48048  dfich2  48069  ichbi12i  48071  ichnfimlem  48074  ich2exprop  48082  ichnreuop  48083  ichreuopeq  48084  sprsymrelfo  48108  reupr  48133  reuopreuprim  48137  mogoldbb  48412  2zrngagrp  48876  2zrngmmgm  48879  cbvmpox2  48963  ovmpordx  48967  1arymaptfo  49270  2arymaptfo  49281  mo0sn  49442  iinfssclem3  49682  iinfssc  49683  iinfsubc  49684  infsubc2  49687  iinfconstbas  49692  isthincd2lem1  50051  nfintd  50299  nfiund  50300  nfiundg  50301  iunord  50302  spcdvw  50305  nfsetrecs  50312  setrec1lem2  50314  setrec1  50317  setrec2fun  50318  pgindnf  50342  pgind  50343  aacllem  50427