Theorem nfv 1946

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

This proof depends on syntax axioms:  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfvd  1947  cbvaldw  2367  cbval2v  2372  dvelimhw  2374  pm11.53  2375  19.12vv  2376  eeanv  2378  eeeanv  2379  ee4anv  2380  sbnf2  2387  exsb  2388  2exsb  2389  sbbibvv  2391  cbvsbvf  2392  cleljustALT2  2394  spimv  2419  spimev  2421  chvarv  2425  cbvalv  2429  cbvexv  2430  cbvald  2436  cbvaldva  2438  cbvexdva  2439  cbval2  2440  axc16i  2465  dvelimnf  2482  sbel2x  2503  sbiedv  2533  2sbiev  2534  sbid2v  2538  sbhb  2550  2sb8e  2559  nfmod2  2583  nfmodv  2584  mof  2588  mo4f  2592  euf  2601  sb8eulem  2623  cbvmow  2628  sbmo  2639  moexexvw  2653  moexexv  2664  2mo  2673  2eu6  2681  axextmo  2736  nulmo  2737  abbib  2829  cleqh  2889  nfcv  2922  nfeqd  2932  nfeld  2933  nfabdw  2943  nfabd  2944  dvelimdc  2946  nfcvf  2948  cleqf  2950  r19.29af  3271  rexbidvALT  3277  rexbidvaALT  3278  2ralbida  3285  r19.12  3311  reean  3312  cbvrexsvw  3314  sbralieOLD  3340  cbvralf  3345  cbvralv  3349  cbvrexv  3350  cbvralsv  3351  cbvrexsv  3352  cbvrmow  3390  cbvreu  3404  cbvrmov  3406  cbvreuv  3407  cbvrab  3449  cbvexeqsetf  3465  ceqsex2  3500  vtocl2gaf  3538  vtocl3gaf  3539  spc2ed  3555  rspct  3562  rspc  3564  rspce  3565  eqvincf  3603  elrab3t  3643  ralab2  3654  rexab2  3656  mob2  3672  mob  3674  reu2  3682  rmo4f  3692  reu2eqd  3693  cdeqab1  3729  nfcdeq  3734  sbcco  3764  cbvsbcv  3774  elrabsf  3783  sbc2iegf  3812  reu8nf  3823  rmo2  3833  rmo3  3835  rmoanimALT  3842  nfcsb1d  3868  nfcsbd  3871  csbiebt  3875  csbie2t  3884  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  cbvralv2  3892  cbvrexv2  3893  rspc2vd  3894  dfssf  3899  rabss3d  4006  eqrrabd  4011  uniiunlem  4012  ab0orv  4331  ab0orvALT  4332  sbcnestgw  4380  sbcnestg  4385  sbnfc2  4396  r19.3rzvOLD  4459  r19.28zv  4461  r19.27zv  4466  2reu4lem  4478  nfifd  4511  reusngf  4634  reusng  4637  rexreusng  4639  reuprg0  4662  rabsnifsb  4682  euabsn  4686  nfunid  4872  eluniab  4880  nfint  4916  iuneqconst  4962  disjiun  5090  disjxun  5100  nfopabd  5172  cbvopab  5176  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  mpteq12da  5187  mpteq12f  5189  cbvmptf  5204  cbvmptfg  5205  axrep1  5232  axrep2  5234  axrep3  5235  axrep5  5238  zfrepclf  5243  reusv2lem3  5361  reusv2lem4  5362  reusv2  5364  reusv3  5366  alxfr  5368  ralxfrALT  5376  copsex2t  5463  iunopeqop  5493  iunopeqopOLD  5494  rexopabb  5501  opelopabaf  5518  nfso  5565  pofun  5576  isso2i  5595  nffr  5623  opeliunxp  5717  opeliun2xp  5718  opeliunxp2  5814  ralxpf  5823  dfdmf  5877  dfrnf  5931  elrnmpt1  5941  dfrel4  6182  reuop  6296  frpoinsg  6346  frpoins2g  6348  wfis2g  6358  nfiotadw  6497  nfiotad  6499  cbviotaw  6501  cbviota  6503  cbviotav  6504  sb8iota  6505  iota2d  6526  iota2  6527  dffun6f  6553  imadif  6624  isarep1  6628  isarep2  6629  fv3  6903  tz6.12f  6910  funimassd  6951  fvelimad  6952  feqmptdf  6955  fimarab  6959  opabiotafun  6965  funfv2f  6974  fvmptd  7001  fvmptd2f  7010  fvmptdv  7011  fvmptt  7014  fvopab5  7027  eqfnfv2f  7033  ralrnmptw  7094  ralrnmpt  7096  dffo3f  7106  f1ompt  7111  fompt  7118  ffnfv  7119  ffnfvf  7120  f1ossf1o  7129  fmptco  7130  elabrex  7246  elabrexg  7247  dff13f  7259  fsnex  7291  fliftfun  7320  cbvriotaw  7386  cbvriota  7390  cbvriotav  7391  riota2  7402  riotaeqimp  7403  riota5f  7405  oprabv  7480  nfoprab  7484  mpoeq123  7492  cbvoprab1  7507  cbvoprab2  7508  cbvoprab12  7509  cbvoprab3  7511  cbvmpox  7513  ralrnmpo  7559  ovmpodx  7571  ovmpodf  7576  ovmpodv  7577  ov3  7583  ovmpt3rab1  7679  ofrfval2  7714  onminex  7816  tfis  7866  tfis2  7868  tfisi  7870  tfinds  7871  tfindes  7874  findes  7912  fiun  7955  f1iun  7956  abrexex2g  7976  opabex3d  7977  opabex3rd  7978  opabex3  7979  dfoprab4f  8067  fmpox  8078  offval22  8099  ovmptss  8104  ralxpes  8153  ralxp3  8155  ralxp3es  8156  frpoins3xpg  8157  frpoins3xp3g  8158  opeliunxp2f  8227  tposoprab  8279  fvmpocurryd  8288  nffrecs  8301  tfr3  8407  nfrdg  8422  tz7.48-1  8453  tz7.49  8455  naddsuc2  8711  eqerlem  8753  erovlem  8834  mptelixpg  8963  boxcutc  8969  dom2lem  9019  xpf1o  9158  mapxpen  9162  findcard2  9180  pssnn  9184  nneneq  9221  ac6sfi  9275  fiint  9318  indexfi  9349  wdom2d  9574  ixpiunwdom  9584  cantnflem1  9690  nfttrcld  9711  setinds2  9752  frinsg  9755  frins2  9758  r1val1  9793  rankuni2b  9867  nfscott  9932  scottabf  9939  scottab  9940  scottexsOLD  9943  scott0bsOLD  9945  setrec1lem2  9967  spcdvw  9970  setrec1  9972  setrec2fun  9973  dfac8clem  10111  acni2  10125  aceq1  10196  dfac5lem5  10206  kmlem15  10243  infpssrlem4  10384  fin23lem27  10406  hsmexlem2  10505  hsmexlem4  10507  axcc3  10516  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  ac6c4  10559  zorn2lem4  10577  zorn2lem5  10578  iunfo  10623  iundom2g  10624  uniimadomf  10629  konigthlem  10653  axrepndlem2  10678  axunnd  10681  axpowndlem2  10683  axpowndlem4  10685  axregndlem2  10688  axacndlem5  10696  zfcndrep  10699  zfcndinf  10703  pwfseqlem4a  10746  pwfseqlem4  10747  tskuni  10868  gruiin  10895  reclem2pr  11133  dedekind  11473  dedekindle  11474  fimaxre3  12263  nn0ind-raph  12799  uzind4s  13035  nnwof  13041  lbzbi  13063  fzrevral  13746  rabssnn0fi  14129  fsuppmapnn0fiublem  14133  fsuppmapnn0fiub  14134  fsuppmapnn0fiubex  14135  seqof2  14203  reuccatpfxs1  14896  cotr2g  15129  rlim2  15663  ello1mpt  15688  climeu  15722  o1compt  15754  summolem2a  15881  zsum  15884  sumss  15890  sumss2  15892  fsumcvg2  15893  fsumclf  15904  fsumsplitf  15908  fsumsplit1  15911  fsum2dlem  15936  fsum00  15965  o1fsum  15980  nfcprod1  16077  nfcprod  16078  prodmolem2a  16101  zprod  16104  fprod  16108  fprodntriv  16109  prodss  16114  fprodn0  16146  fprod2dlem  16147  fprodsplitf  16155  fprodsplit1f  16157  fprodle  16163  fprodmodd  16164  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2  16815  coprmprod  16836  coprmproddvdslem  16837  prmind2  16860  iserodd  17013  pcmpt  17070  pcmptdvds  17072  prmolefac  17224  mreexexd  17822  catpropd  17883  invfuc  18152  natpropd  18154  fucpropd  18155  initoeu2  18191  acsmapd  18728  nfchnd  18785  symgval  19585  gsumsnd  20166  gsumsnf  20167  gsumunsnfd  20171  gsummptf1o  20177  gsummpt1n0  20179  gsum2d2lem  20187  gsumcom2  20189  gsummptnn0fz  20200  dprd2d2  20260  rngqiprngimf1  21596  gsummoncoe1  22626  gsumply1eq  22627  mdetralt2  22924  mdetunilem2  22928  madugsum  22958  gsummatr01lem4  22973  matunitlindflem2  22995  cpmatmcllem  23036  cayleyhamilton1  23210  neiptopnei  23450  neiptopreu  23451  neitr  23498  fiuncmp  23722  iunconnlem  23745  iunconn  23746  2ndcdisj  23775  dissnlocfin  23848  elptr2  23893  ptbasfi  23900  ptcld  23932  ptcldmpt  23933  ptclsg  23934  ptcnplem  23940  ptcnp  23941  cnmpt11  23982  cnmpt21  23990  cnmptcom  23997  imasnopn  24009  imasncld  24010  imasncls  24011  xkocnv  24133  elmptrab  24146  isfildlem  24176  alexsubALTlem3  24368  cnextfvval  24384  utopsnneiplem  24566  isucn2  24597  cfilucfil  24878  blval2  24881  restmetu  24889  ovoliunlem3  25825  ovoliun  25826  ovoliun2  25827  ovoliunnul  25828  finiunmbl  25865  volfiniun  25868  iundisj  25869  iunmbl  25874  voliun  25875  iunmbl2  25878  mbfeqalem1  25962  mbfsup  25985  mbfinf  25986  mbflim  25989  itg2splitlem  26069  itg2split  26070  isibl2  26087  cbvitg  26096  itgeqa  26134  itgss3  26135  itgfsum  26147  itgabs  26155  itggt0  26164  itgcn  26165  limcmpt  26203  limciun  26214  dvmptfsum  26295  dvlipcn  26314  dvfsumlem2  26347  dvfsumlem4  26349  dvfsumrlim  26351  dvfsum2  26354  itgsubst  26369  coeeq2  26561  dgrle  26562  ulmss  26724  leibpi  27270  rlimcnp  27293  rlimcnp2  27294  o1cxp  27302  lgamgulmlem2  27357  lgamgulmlem6  27361  fsumdvdscom  27512  lgseisenlem2  27703  2sqmo  27764  2sqreulem4  27781  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  nosupbnd1  28071  nosupbnd2  28073  noinfbnd1  28086  noinfbnd2  28088  bdayiun  28301  bdaypw2n0bndlem  28849  istrkg2ld  28922  prlngmo2  29434  mpteleeOLD  29473  gropd  29609  grstructd  29610  clwwlknonclwlknonf1o  30963  dlwwlknondlwlknonf1o  30966  ex-natded9.26  31020  isch3  31843  atom1d  32955  chirred  32997  sbc2iedf  33062  rspc2daf  33063  19.9d2r  33067  opreu2reuALT  33073  mo5f  33085  reuxfrdf  33087  foresf1o  33100  elabreximdv  33107  iinabrex  33163  cbvdisjf  33165  disjorf  33173  disjabrex  33176  iundisjf  33183  disjunsn  33188  brabgaf  33200  ac6sf2  33216  dfimafnf  33230  2ndresdju  33243  fmptcof2  33251  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1lem  33256  aciunf1  33257  ofpreima  33259  funcnv5mpt  33261  funcnv4mpt  33262  fnpreimac  33264  f1od2  33311  fpwrelmap  33325  xrofsup  33359  iundisjfi  33388  nnindf  33411  nn0min  33412  fprodex01  33416  fsumiunle  33420  prodindf  33429  gsummpt2d  33610  gsummptf1od  33616  gsummptfsf1o  33621  gsumhashmul  33628  suppgsumssiun  33633  gsumwrd2dccat  33639  isarchiofld  33760  elrgspnsubrunlem2  33809  nsgmgc  33963  nsgqusf1olem1  33964  nsgqusf1olem3  33966  nsgqusf1o  33967  elrspunidl  33978  elrspunsn  33979  deg1prod  34115  ply1gsumz  34131  ig1pmindeg  34134  mplvrpmga  34177  psrgsum  34180  psrmonprod  34184  esplylem  34198  esplyfv1  34201  esplyfval1  34205  esplyfvaln  34206  esplyind  34207  vieta  34212  exsslsb  34229  ply1degltdimlem  34254  fedgmullem2  34262  evls1fldgencl  34302  irngnzply1  34323  extdgfialglem2  34325  ply1annidllem  34333  algextdeglem6  34354  constrfin  34378  reff  34471  locfinreflem  34472  cmpcref  34482  zarclsiin  34503  zarcls  34506  zarcmplem  34513  ordtconnlem1  34556  qqhval2  34614  esumeq12dva  34664  esumeq2dv  34670  esumrnmpt  34684  esumpad  34687  esumpad2  34688  esumadd  34689  gsumesum  34691  esumlub  34692  esumsnf  34696  esumpr  34698  esumrnmpt2  34700  esumfzf  34701  esumfsup  34702  esumpcvgval  34710  esumpmono  34711  esumcocn  34712  hasheuni  34717  esumcvg  34718  esumgect  34722  esum2dlem  34724  esum2d  34725  esumiun  34726  ldsysgenld  34793  sigapildsyslem  34794  sigapildsys  34795  ldgenpisyslem1  34796  fiunelros  34807  measvunilem  34845  measvunilem0  34846  measvuni  34847  measiun  34851  measinblem  34853  voliune  34862  volfiniune  34863  volmeas  34864  ddemeas  34869  oms0  34929  omssubadd  34932  carsgclctunlem1  34949  carsggect  34950  omsmeas  34955  eulerpartlemgvv  35008  dstrvprob  35104  ballotlemodife  35130  reprsuc  35244  reprdifc  35256  breprexplema  35259  breprexplemc  35261  circlemethhgt  35272  hgt750lemd  35277  bnj919  35398  bnj1146  35421  bnj1379  35460  bnj1385  35462  bnj1400  35465  bnj1534  35483  bnj1542  35487  bnj110  35488  bnj121  35500  bnj124  35501  bnj130  35504  bnj207  35511  bnj571  35536  bnj605  35537  bnj580  35543  bnj607  35546  bnj611  35548  bnj873  35554  bnj849  35555  bnj900  35559  bnj916  35563  bnj1000  35571  bnj964  35573  bnj981  35580  bnj985v  35583  bnj985  35584  bnj1014  35591  bnj1123  35616  bnj1128  35620  bnj1228  35641  bnj1204  35642  bnj1279  35648  bnj1307  35653  bnj1321  35657  bnj1388  35663  bnj1398  35664  bnj1408  35666  bnj1417  35671  bnj1444  35673  bnj1445  35674  bnj1446  35675  bnj1449  35678  bnj1467  35684  bnj1489  35686  bnj1312  35688  bnj1497  35690  bnj1518  35694  bnj1525  35699  bnj1529  35700  dvelimalcased  35705  dvelimexcased  35707  fineqvrep  35782  axsepg2  35808  axsepg3  35809  axsepg3ALT  35810  axpowg2  35815  axpowg3  35816  onvf1odlem2  35883  cvmcov  36028  untsucf  36475  dfon2lem3  36547  finminlem  37106  weiunpo  37253  weiunso  37254  weiunfr  37255  weiunse  37256  axtcond  37266  regsfromregtco  37326  regsfromsetind  37327  mh-inf3f1  37329  bj-nexdvt  37600  bj-cbvaldv  37711  bj-cbval2vv  37713  bj-cbvex2vv  37714  bj-cbvaldvav  37715  bj-cbvexdvav  37716  ax11-pm2  37748  bj-dvelimdv  37763  bj-nfeel2  37766  bj-ceqsalv  37806  bj-vtocl  37828  bj-inrab2  37841  currysetlem  37858  currysetlem1  37860  bj-axseprep  37990  bj-axreprepsep  37991  bj-opabco  38110  mptsnunlem  38262  exlimim  38266  exellim  38268  topdifinfindis  38270  topdifinffinlem  38271  icorempo  38275  isbasisrelowllem1  38279  isbasisrelowllem2  38280  relowlssretop  38287  finxpreclem2  38314  finxpreclem6  38320  fvineqsneu  38335  fvineqsneq  38336  wl-euequf  38507  wl-sb8eut  38511  wl-issetft  38515  phpreu  38528  ptrest  38538  ptrecube  38539  poimirlem2  38541  poimirlem23  38562  poimirlem24  38563  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  heicant  38574  mbfposadd  38586  itgabsnc  38608  itggt0cn  38609  ftc1anclem5  38616  upixp  38664  indexa  38668  indexdom  38669  filbcmb  38675  sdclem2  38677  sdclem1  38678  fdc1  38681  totbndbnd  38724  sbcalf  39047  sbcexf  39048  scottexf  39101  scott0f  39102  eqrelf  39191  ralrmo3  39297  disjqmap2  39759  fsumshftd  40010  riotasv2d  40015  riotasv2s  40016  riotasv3d  40018  glbconxN  40436  pmapglbx  40827  pmapglb2xN  40830  cdleme26ee  41418  cdleme31sn  41438  cdleme31sn1  41439  cdlemefr29exN  41460  cdlemefs32sn1aw  41472  cdleme43fsv1snlem  41478  cdleme41sn3a  41491  cdleme32fva  41495  cdleme32d  41502  cdleme32f  41504  cdleme40m  41525  cdleme40n  41526  cdleme42b  41536  cdlemk36  41971  cdlemk38  41973  cdlemkid  41994  cdlemk19x  42001  cdlemk11t  42004  dihvalcqpre  42293  mapdheq  42786  hdmap1eq  42859  hdmapval2lem  42889  lcmineqlem9  43088  lcmineqlem12  43091  aks4d1p1p2  43121  mndmolinv  43146  primrootsunit1  43148  primrootsunit  43149  primrootspoweq0  43157  aks6d1c1p5  43163  aks6d1c3  43174  aks6d1c4  43175  aks6d1c1rh  43176  aks6d1c2lem4  43178  aks6d1c2  43181  deg1gprod  43191  sticksstones1  43197  sticksstones11  43207  sticksstones16  43213  sticksstones22  43219  aks6d1c6lem2  43222  aks6d1c6isolem1  43225  aks6d1c6isolem2  43226  bcled  43229  bcle2d  43230  aks6d1c7lem3  43233  aks6d1c7  43235  rhmqusspan  43236  grpods  43245  unitscyglem1  43246  unitscyglem2  43247  unitscyglem3  43248  unitscyglem4  43249  unitscyglem5  43250  nfa1w  43687  mzpexpmpt  43756  eq0rabdioph  43787  rexrabdioph  43801  rexfrabdioph  43802  elnn0rabdioph  43810  dvdsrabdioph  43817  fphpd  43823  monotuz  43948  monotoddzz  43950  oddcomabszz  43951  setindtr  44031  dford4  44036  wdom2d2  44042  aomclem6  44061  aomclem8  44063  flcidc  44172  areaquad  44218  unielss  44220  onsucf1lem  44271  oaun3lem1  44376  nadd1suc  44394  rababg  44575  ss2iundv  44660  cbviuneq12dv  44662  gneispace  45134  mnringvald  45211  mnringmulrcld  45226  mnuprdlem4  45259  ismnushort  45285  binomcxplemdvsum  45339  binomcxplemnotnn0  45340  aaanv  45372  pm11.57  45373  pm11.58  45374  pm11.59  45375  pm11.71  45381  pm14.12  45405  ssralv2  45514  tratrb  45519  iunconnlem2  45917  modelaxreplem3  45970  modelaxrep  45971  permaxrep  45996  evth2f  46032  elunif  46033  fvelrnbf  46035  evthf  46044  fnchoice  46046  sumpair  46052  rfcnnnub  46053  refsum2cn  46055  uzwo4  46070  fiiuncl  46082  fiunicl  46084  elintdv  46096  ssd  46097  cbvmpo2  46112  cbvmpo1  46113  eliin2f  46119  eliuniin2  46135  cbvrabv2  46142  suprnmpt  46189  disjf1  46198  disjrnmpt2  46203  disjf1o  46206  disjinfi  46207  choicefi  46214  iunmapsn  46230  axccdom  46235  dmrelrnrel  46239  axccd  46241  fmptf  46251  rnmptlb  46255  rnmptbddlem  46256  rnmptbd2lem  46260  rnmptbdlem  46267  rnmptbd  46268  fmptff  46281  upbdrech  46321  ssfiunibd  46325  supxrgere  46345  iuneqfzuzlem  46346  supxrgelem  46349  supxrge  46350  suplesup  46351  infrpge  46363  xralrple2  46366  infxr  46378  infxrunb2  46379  infleinf  46383  xrralrecnnle  46394  xrralrecnnge  46401  supxrunb3  46410  supxrleubrnmpt  46416  infleinf2  46424  unb2ltle  46425  rexabslelem  46428  rexabsle  46429  allbutfiinf  46430  suprleubrnmpt  46432  infrnmptle  46433  infxrunb3rnmpt  46438  uzublem  46440  uzub  46441  supminfrnmpt  46455  infxrpnf  46456  supxrleubrnmptf  46461  infxrgelbrnmpt  46464  infrpgernmpt  46475  supminfxr2  46479  monoordxr  46492  monoord2xr  46494  caucvgbf  46499  cvgcaule  46501  rexanuz2nf  46502  iccshift  46530  iooshift  46534  iooiinicc  46554  iooiinioc  46568  fsummulc1f  46583  fsumnncl  46584  fsumf1of  46586  fsumiunss  46587  fsumreclf  46588  fsumlessf  46589  fsumsermpt  46591  fmul01  46592  fmuldfeqlem1  46594  fmuldfeq  46595  fmul01lt1lem1  46596  fmul01lt1lem2  46597  fmul01lt1  46598  fprodsplit1  46605  fprodexp  46606  fprodabs2  46607  mccllem  46609  mccl  46610  fprodcnlem  46611  fprodcn  46612  climexp  46617  climsuse  46620  climrecf  46621  climinff  46623  climaddf  46627  mullimc  46628  ellimcabssub0  46629  islptre  46631  climf  46634  mullimcf  46635  rexlim2d  46637  idlimc  46638  limcperiod  46640  limcrecl  46641  sumnnodd  46642  islpcn  46649  limsupre  46651  limcleqr  46654  neglimc  46657  addlimc  46658  0ellimcdiv  46659  limclner  46661  climsubmpt  46670  climreclf  46674  climf2  46676  fnlimcnv  46677  climeldmeqmpt  46678  clim2f2  46680  climfveqmpt  46681  fnlimfvre  46684  allbutfifvre  46685  climleltrp  46686  fnlimf  46688  fnlimabslt  46689  climfveqmpt3  46692  climeldmeqf  46693  limsupref  46695  limsupbnd1f  46696  climbddf  46697  climeqf  46698  climeldmeqmpt3  46699  limsuplesup  46709  limsuppnfd  46712  limsupub  46714  limsupres  46715  climinf2lem  46716  climinf2  46717  limsuppnf  46721  limsupubuzlem  46722  limsupubuz  46723  climinf2mpt  46724  climinfmpt  46725  climinf3  46726  limsupmnflem  46730  limsupmnf  46731  limsupequz  46733  limsupre2  46735  limsupmnfuzlem  46736  limsupmnfuz  46737  limsupequzmptf  46741  limsupre3lem  46742  limsupre3  46743  limsupre3uzlem  46745  limsupre3uz  46746  limsupreuz  46747  limsupvaluz2  46748  limsupreuzmpt  46749  supcnvlimsup  46750  climuzlem  46753  climuz  46754  climisp  46756  lmbr3  46757  climrescn  46758  climxrrelem  46759  climxrre  46760  liminfcl  46773  liminfval2  46778  limsup10exlem  46782  liminflelimsuplem  46785  limsupgtlem  46787  limsupgt  46788  climliminflimsupd  46811  liminfreuzlem  46812  liminfreuz  46813  liminfltlem  46814  liminflt  46815  limsupub2  46822  xlimpnfxnegmnf  46824  liminflbuz2  46825  liminfpnfuz  46826  liminflimsupxrre  46827  xlimmnfvlem1  46842  xlimmnfvlem2  46843  xlimmnfv  46844  xlimpnfvlem1  46846  xlimpnfvlem2  46847  xlimpnfv  46848  xlimmnf  46851  xlimpnf  46852  xlimmnfmpt  46853  xlimpnfmpt  46854  climxlim2lem  46855  dfxlim2  46858  cncfshift  46884  icccncfext  46897  cncficcgt0  46898  cncfiooicc  46904  cncfioobd  46907  fprodcncf  46910  fprodsubrecnncnvlem  46917  fprodaddrecnncnvlem  46919  dvmptmulf  46947  dvnmptdivc  46948  dvnmul  46953  dvmptfprodlem  46954  dvmptfprod  46955  dvnprodlem1  46956  dvnprodlem2  46957  iblsplitf  46980  iblspltprt  46983  itgioocnicc  46987  iblcncfioo  46988  itgspltprt  46989  itgperiod  46991  stoweidlem3  47013  stoweidlem14  47024  stoweidlem17  47027  stoweidlem19  47029  stoweidlem20  47030  stoweidlem26  47036  stoweidlem27  47037  stoweidlem28  47038  stoweidlem29  47039  stoweidlem31  47041  stoweidlem34  47044  stoweidlem35  47045  stoweidlem36  47046  stoweidlem39  47049  stoweidlem42  47052  stoweidlem43  47053  stoweidlem44  47054  stoweidlem46  47056  stoweidlem48  47058  stoweidlem49  47059  stoweidlem50  47060  stoweidlem51  47061  stoweidlem52  47062  stoweidlem53  47063  stoweidlem54  47064  stoweidlem56  47066  stoweidlem57  47067  stoweidlem59  47069  stoweidlem60  47070  stoweidlem61  47071  stoweidlem62  47072  stoweid  47073  wallispilem3  47077  stirlinglem13  47096  stirling  47099  fourierdlem16  47133  fourierdlem21  47138  fourierdlem22  47139  fourierdlem31  47148  fourierdlem39  47156  fourierdlem48  47164  fourierdlem51  47167  fourierdlem53  47169  fourierdlem68  47184  fourierdlem69  47185  fourierdlem71  47187  fourierdlem73  47189  fourierdlem77  47193  fourierdlem80  47196  fourierdlem81  47197  fourierdlem82  47198  fourierdlem83  47199  fourierdlem86  47202  fourierdlem87  47203  fourierdlem89  47205  fourierdlem91  47207  fourierdlem93  47209  fourierdlem94  47210  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  fourierdlem113  47229  elaa2  47244  etransclem18  47262  etransclem22  47266  etransclem23  47267  etransclem32  47276  etransclem35  47279  etransclem44  47288  etransclem46  47290  etransclem48  47292  rrndistlt  47300  ioorrnopnlem  47314  saliuncl  47333  saliincl  47337  intsaluni  47339  salexct  47344  subsaliuncl  47368  sge00  47386  sge0revalmpt  47388  sge0sn  47389  sge0f1o  47392  sge0gerp  47405  sge0pnffigt  47406  sge0lefi  47408  sge0ltfirp  47410  sge0resrnlem  47413  sge0resplit  47416  sge0lempt  47420  sge0iunmptlemfi  47423  sge0p1  47424  sge0iunmptlemre  47425  sge0fodjrnlem  47426  sge0iunmpt  47428  sge0rpcpnf  47431  sge0ltfirpmpt2  47436  sge0isum  47437  sge0xp  47439  sge0ad2en  47441  sge0isummpt2  47442  sge0xaddlem1  47443  sge0xaddlem2  47444  sge0xadd  47445  sge0pnffsumgt  47452  sge0gtfsumgt  47453  sge0uzfsumgt  47454  sge0seq  47456  sge0reuz  47457  sge0reuzb  47458  iundjiun  47470  meadjiunlem  47475  meadjiun  47476  ismeannd  47477  voliunsge0lem  47482  meaiuninclem  47490  meaiunincf  47493  meaiuninc3v  47494  meaiuninc3  47495  meaiininclem  47496  meaiininc  47497  meaiininc2  47498  caragenfiiuncl  47525  omeiunltfirp  47529  carageniuncllem1  47531  carageniuncllem2  47532  caratheodorylem2  47537  0ome  47539  isomenndlem  47540  hoicvrrex  47566  ovnsupge0  47567  ovnlecvr  47568  ovnlerp  47572  ovncvrrp  47574  ovn0lem  47575  ovnsubaddlem1  47580  ovnsubaddlem2  47581  hoidmvcl  47592  hsphoidmvle2  47595  hsphoidmvle  47596  hoidmvval0  47597  sge0hsphoire  47599  hoidmvval0b  47600  hoidmv1lelem1  47601  hoidmv1lelem2  47602  hoidmv1lelem3  47603  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvlelem4  47608  hoidmvlelem5  47609  hoidmvle  47610  ovnhoilem1  47611  ovnhoilem2  47612  ovnhoi  47613  ovnlecvr2  47620  hspdifhsp  47626  hoidifhspdmvle  47630  hoiqssbllem3  47634  hspmbllem1  47636  hspmbllem2  47637  opnvonmbllem1  47642  opnvonmbllem2  47643  ovnsubadd2lem  47655  ovolval5lem1  47662  ovnovollem1  47666  ovnovollem2  47667  hoimbl2  47675  vonhoire  47682  iinhoiicclem  47683  iinhoiicc  47684  iunhoiioolem  47685  iunhoiioo  47686  vonioolem1  47690  vonioolem2  47691  vonioo  47692  vonicclem1  47693  vonicclem2  47694  vonicc  47695  vonn0ioo2  47700  vonn0icc2  47702  vonct  47703  pimltmnf2f  47707  pimgtpnf2f  47715  salpreimagelt  47717  salpreimalegt  47719  pimltpnf2f  47722  pimgtmnf2  47724  pimdecfgtioc  47725  pimincfltioc  47726  pimdecfgtioo  47727  pimincfltioo  47728  preimageiingt  47730  preimaleiinlt  47731  salpreimagtge  47735  salpreimaltle  47736  salpreimalelt  47739  salpreimagtlt  47740  issmff  47744  sssmf  47748  mbfresmf  47749  cnfsmf  47750  incsmflem  47751  incsmf  47752  smfsssmf  47753  issmflelem  47754  issmfle  47755  smfconst  47759  issmfgtlem  47765  issmfgt  47766  smfpimltxrmptf  47768  smfmbfcex  47770  smfaddlem1  47773  smfaddlem2  47774  smfadd  47775  decsmflem  47776  decsmf  47777  smfpreimagtf  47778  issmfgelem  47779  issmfge  47780  smflimlem2  47782  smflimlem4  47784  smflim  47787  smfpimgtxr  47790  smfpimgtxrmptf  47794  smfpimioo  47797  smfresal  47798  smfrec  47799  smfres  47800  smfmullem2  47802  smfmullem4  47804  smfmul  47805  smfpimbor1lem2  47809  smf2id  47811  smfco  47812  smflim2  47816  smfpimcc  47818  smflimmpt  47820  smfsuplem1  47821  smfsuplem3  47823  smfsup  47824  smfsupmpt  47825  smfsupxr  47826  smfinflem  47827  smfinf  47828  smfinfmpt  47829  smflimsuplem3  47832  smflimsuplem4  47833  smflimsuplem5  47834  smflimsuplem7  47836  smflimsuplem8  47837  smflimsup  47838  smflimsupmpt  47839  smfliminflem  47840  smfliminf  47841  smfliminfmpt  47842  smfpimne2  47850  fsupdm  47852  smfsupdmmbllem  47854  smfsupdmmbl  47855  finfdm  47856  smfinfdmmbllem  47858  smfinfdmmbl  47859  tmachlem-agreesn  47957  or2expropbilem1  48102  or2expropbilem2  48103  or2expropbi  48104  cfsetsnfsetf  48128  cfsetsnfsetfo  48130  rexsb  48169  reuf1odnf  48177  2reu8i  48183  ffnafv  48241  tz6.12c-afv2  48312  f1oresf1o2  48361  iccelpart  48515  iccpartdisj  48519  dfich2  48540  ichbi12i  48542  ichnfimlem  48545  ich2exprop  48553  ichnreuop  48554  ichreuopeq  48555  sprsymrelfo  48579  reupr  48604  reuopreuprim  48608  mogoldbb  48883  2zrngagrp  49346  2zrngmmgm  49349  cbvmpox2  49448  ovmpordx  49452  1arymaptfo  49755  2arymaptfo  49766  mo0sn  49926  iinfssclem3  50164  iinfssc  50165  iinfsubc  50166  infsubc2  50169  iinfconstbas  50174  isthincd2lem1  50533  nfintd  50781  nfiund  50782  nfiundg  50783  iunord  50784  nfsetrecs  50789  pgindnf  50809  pgind  50810  aacllem  50939