Theorem nfv 1920

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

Syntax hints:  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 210  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfvd  1921  nfsbv  2331  cbvaldw  2339  cbval2v  2344  cbval2vOLD  2345  dvelimhw  2347  pm11.53  2348  19.12vv  2349  eeanv  2351  eeeanv  2352  sbnf2  2358  exsb  2359  2exsb  2360  sbbibvv  2362  cleljustALT2  2364  spimv  2389  spimev  2391  chvarv  2395  cbvalv  2399  cbvexv  2400  cbvald  2406  cbvaldva  2408  cbvexdva  2409  cbval2  2410  axc16i  2435  dvelimnf  2452  sbel2x  2474  sbiedv  2508  2sbiev  2509  sbid2v  2513  sbhb  2525  2sb8e  2535  nfmod2  2558  nfmodv  2559  mof  2563  mo4f  2567  mo4OLD  2568  euf  2577  sb8eulem  2599  cbvmow  2604  sbmo  2617  moexexvw  2631  moexexv  2642  2mo  2651  2mos  2652  2eu6  2659  axextmo  2714  nulmo  2715  abbi  2805  cbvabw  2807  cleqh  2856  clelabOLD  2876  nfcv  2899  nfeqd  2909  nfeld  2910  nfabdw  2922  nfabdwOLD  2923  nfabd  2924  dvelimdc  2926  nfcvf  2928  cleqf  2930  sbabel  2933  2ralbida  3145  rexbidvaALT  3228  rexbidvALT  3230  r19.12  3233  r19.29af  3239  reean  3268  rmobidva  3295  cbvralfwOLD  3335  cbvralf  3337  cbvreuw  3341  cbvrmow  3342  cbvreu  3346  cbvreuvwOLD  3352  cbvralv  3353  cbvrexv  3354  cbvreuv  3355  cbvrmov  3356  cbvralsvw  3367  cbvrexsvw  3368  cbvralsv  3369  cbvrexsv  3370  cbvrabw  3390  cbvrab  3391  abv  3408  abvALT  3409  issetf  3411  ceqsalvOLD  3433  ceqsralvOLD  3435  ceqsexv  3444  ceqsex2  3446  vtoclgft  3456  vtocldOLD  3460  vtoclALT  3464  vtoclgOLD  3471  vtocl2gaf  3479  vtocl3gaf  3480  vtocl3ga  3481  spc2ed  3503  rspct  3510  rspc  3512  rspce  3513  rspcvOLD  3520  rspcevOLD  3525  eqvincf  3544  ceqsexgvOLD  3549  clel2gOLD  3554  elabgt  3565  elabg  3570  elab  3571  elab3g  3577  elrab3t  3584  ralab2  3594  ralab2OLD  3595  rexab2  3597  rexab2OLD  3598  mob2  3612  mob  3614  reu2  3622  rmo4f  3632  reu2eqd  3633  cdeqab1  3669  nfcdeq  3674  sbcco  3705  cbvsbcv  3715  sbcieg  3718  sbcied  3722  elrabsf  3724  sbcbidvOLD  3735  sbcg  3753  sbc2iegf  3755  sbc2ie  3756  reu8nf  3766  rmo2  3776  rmo3  3778  rmoanimALT  3784  csbeq2dv  3795  nfcsb1d  3810  nfcsbd  3813  csbiebt  3817  csbied  3824  csbie2t  3826  cbvrabcsfw  3829  cbvralcsf  3830  cbvreucsf  3832  cbvrabcsf  3833  cbvralv2  3834  cbvrexv2  3835  vtocl2dOLD  3836  rspc2vd  3837  dfss2f  3865  uniiunlem  3973  rspn0OLD  4240  ab0OLD  4261  ab0orv  4264  ab0orvALT  4265  sbcnestgw  4307  sbcnestg  4312  sbnfc2  4323  r19.3rzv  4382  r19.28zv  4384  r19.27zv  4389  2reu4lem  4409  nfifd  4440  reusngf  4560  reusng  4563  ralsngOLD  4565  rexsngOLD  4566  rexreusng  4567  ralprgOLD  4583  rexprgOLD  4585  reuprg0  4590  rabsnifsb  4610  euabsn  4614  nfunid  4799  eluniab  4808  nfint  4843  elintab  4844  iuneqconst  4889  iineq2dv  4903  disjiun  5014  disjxun  5025  nfopab  5095  cbvopab  5098  cbvopabv  5099  cbvopab1  5100  cbvopab1g  5101  cbvopab2  5102  cbvopab1s  5103  cbvopab1v  5104  mpteq12df  5109  mpteq12f  5110  mpteq12dv  5112  mpteq2dva  5122  cbvmptf  5126  cbvmptfg  5127  axrep1  5152  axrep2  5154  axrep3  5155  axrep4  5156  axrep5  5157  zfrepclf  5159  dtru  5234  reusv2lem3  5264  reusv2lem4  5265  reusv2  5267  reusv3  5269  alxfr  5271  ralxfrALT  5279  axprlem3  5289  axprlem4  5290  axprlem5  5291  copsex2t  5346  copsex2gOLD  5348  iunopeqop  5375  rexopabb  5380  opelopabaf  5396  nfso  5444  pofun  5455  isso2i  5472  nffr  5493  opeliunxp  5584  opeliunxp2  5675  ralxpf  5683  dfdmf  5733  dfrnf  5787  elrnmpt1  5795  dfrel4  6017  reuop  6119  wfisg  6158  wfis2g  6162  nfiotadw  6294  nfiotad  6296  cbviotaw  6298  cbviotavwOLD  6300  cbviota  6301  cbviotav  6302  sb8iota  6303  iota2d  6321  iota2  6322  dffun6f  6347  imadif  6417  funimaexg  6419  isarep1  6421  isarep2  6422  fv3  6686  tz6.12f  6692  tz6.12c  6693  fvelimad  6730  feqmptdf  6733  opabiotafun  6743  funfv2f  6751  fvmptd  6776  fvmptd2f  6785  fvmptdv  6786  fvmptt  6789  fvopab5  6801  eqfnfv2f  6807  ralrnmptw  6864  ralrnmpt  6866  f1ompt  6879  ffnfv  6886  ffnfvf  6887  f1ossf1o  6894  fmptco  6895  elabrex  7007  dff13f  7019  fsnex  7044  fliftfun  7072  cbvriotaw  7130  cbvriotavwOLD  7132  cbvriota  7135  cbvriotav  7136  riota2  7147  riotaeqimp  7148  riota5f  7150  oprabv  7222  nfoprab  7226  oprabbidv  7228  mpoeq123  7234  cbvoprab1  7249  cbvoprab2  7250  cbvoprab12  7251  cbvoprab12v  7252  cbvoprab3  7253  cbvoprab3v  7254  cbvmpox  7255  ralrnmpo  7298  ovmpodx  7310  ovmpodf  7315  ovmpodv  7316  ov3  7321  ovmpt3rab1  7413  ofrfval2  7439  onminex  7535  tfis  7582  tfis2  7584  tfisi  7586  tfinds  7587  tfindes  7590  peano5  7618  findes  7626  fiun  7662  f1iun  7663  abrexex2g  7683  opabex3d  7684  opabex3rd  7685  opabex3  7686  dfoprab4f  7772  fmpox  7783  offval22  7802  ovmptss  7807  opeliunxp2f  7898  tposoprab  7950  fvmpocurryd  7959  nfwrecs  7971  tfr3  8057  nfrdg  8072  tz7.48-1  8101  tz7.49  8103  eqerlem  8347  erovlem  8417  mptelixpg  8538  boxcutc  8544  dom2lem  8588  xpf1o  8722  mapxpen  8726  nneneq  8743  findcard2  8756  pssnn  8760  pssnnOLD  8808  findcard2OLD  8827  ac6sfi  8829  fiint  8862  indexfi  8898  wdom2d  9110  ixpiunwdom  9120  cantnflem1  9218  r1val1  9281  rankuni2b  9348  scottexs  9382  scott0s  9383  dfac8clem  9525  acni2  9539  aceq1  9610  dfac5lem5  9620  kmlem15  9657  infpssrlem4  9799  fin23lem27  9821  hsmexlem2  9920  hsmexlem4  9922  axcc3  9931  domtriomlem  9935  axdc3lem2  9944  axdc3lem4  9946  axdc4lem  9948  ac6c4  9974  zorn2lem4  9992  zorn2lem5  9993  iunfo  10032  iundom2g  10033  uniimadomf  10038  konigthlem  10061  axrepndlem2  10086  axunnd  10089  axpowndlem2  10091  axpowndlem4  10093  axregndlem2  10096  axacndlem5  10104  zfcndrep  10107  zfcndinf  10111  pwfseqlem4a  10154  pwfseqlem4  10155  tskuni  10276  gruiin  10303  reclem2pr  10541  dedekind  10874  dedekindle  10875  fimaxre3  11657  nn0ind-raph  12156  uzind4s  12383  nnwof  12389  lbzbi  12411  fzrevral  13076  rabssnn0fi  13438  fsuppmapnn0fiublem  13442  fsuppmapnn0fiub  13443  fsuppmapnn0fiubex  13444  seqof2  13513  reuccatpfxs1  14191  cotr2g  14418  rlim2  14936  ello1mpt  14961  climeu  14995  o1compt  15027  summolem2a  15158  zsum  15161  sumss  15167  sumss2  15169  fsumcvg2  15170  fsumsplitf  15184  fsum2dlem  15211  fsum00  15239  o1fsum  15254  nfcprod1  15349  nfcprod  15350  prodmolem2a  15373  zprod  15376  fprod  15380  fprodntriv  15381  prodss  15386  fprodn0  15418  fprod2dlem  15419  fprodsplitf  15427  fprodsplit1f  15429  fprodle  15435  fprodmodd  15436  lcmfunsnlem1  16071  lcmfunsnlem2lem1  16072  lcmfunsnlem2  16074  coprmprod  16095  coprmproddvdslem  16096  prmind2  16119  iserodd  16265  pcmpt  16321  pcmptdvds  16323  prmolefac  16475  mreexexd  17015  catpropd  17076  invfuc  17342  natpropd  17344  fucpropd  17345  initoeu2  17381  acsmapd  17897  symgval  18608  gsumsnd  19184  gsumsnf  19185  gsumunsnfd  19189  gsummptf1o  19195  gsummpt1n0  19197  gsum2d2lem  19205  gsumcom2  19207  gsummptnn0fz  19218  dprd2d2  19278  gsummoncoe1  21072  gsumply1eq  21073  mdetralt2  21353  mdetunilem2  21357  madugsum  21387  gsummatr01lem4  21402  cpmatmcllem  21462  cayleyhamilton1  21636  neiptopnei  21876  neiptopreu  21877  neitr  21924  fiuncmp  22148  iunconnlem  22171  iunconn  22172  2ndcdisj  22200  dissnlocfin  22273  elptr2  22318  ptbasfi  22325  ptcld  22357  ptcldmpt  22358  ptclsg  22359  ptcnplem  22365  ptcnp  22366  cnmpt11  22407  cnmpt21  22415  cnmptcom  22422  imasnopn  22434  imasncld  22435  imasncls  22436  xkocnv  22558  elmptrab  22571  isfildlem  22601  alexsubALTlem3  22793  cnextfvval  22809  utopsnneiplem  22992  isucn2  23024  cfilucfil  23305  blval2  23308  restmetu  23316  ovoliunlem3  24249  ovoliun  24250  ovoliun2  24251  ovoliunnul  24252  finiunmbl  24289  volfiniun  24292  iundisj  24293  iunmbl  24298  voliun  24299  iunmbl2  24302  mbfeqalem1  24386  mbfsup  24409  mbfinf  24410  mbflim  24413  itg2splitlem  24493  itg2split  24494  isibl2  24511  cbvitg  24520  itgeqa  24558  itgss3  24559  itgfsum  24571  itgabs  24579  itggt0  24588  itgcn  24589  limcmpt  24627  limciun  24638  dvmptfsum  24719  dvlipcn  24738  dvfsumlem2  24771  dvfsumlem4  24773  dvfsumrlim  24775  dvfsum2  24778  itgsubst  24793  coeeq2  24983  dgrle  24984  ulmss  25136  leibpi  25672  rlimcnp  25695  rlimcnp2  25696  o1cxp  25704  lgamgulmlem2  25759  lgamgulmlem6  25763  fsumdvdscom  25914  lgseisenlem2  26104  2sqmo  26165  2sqreulem4  26182  dchrisumlema  26216  dchrisumlem2  26218  dchrisumlem3  26219  istrkg2ld  26398  mptelee  26833  gropd  26968  grstructd  26969  clwwlknonclwlknonf1o  28291  dlwwlknondlwlknonf1o  28294  ex-natded9.26  28348  isch3  29168  atom1d  30280  chirred  30322  sbc2iedf  30381  rspc2daf  30382  19.9d2r  30387  opreu2reuALT  30391  mo5f  30403  reuxfrdf  30405  eqrrabd  30415  foresf1o  30416  elabreximdv  30422  rabss3d  30427  iinabrex  30474  cbvdisjf  30476  disjorf  30484  disjabrex  30487  iundisjf  30494  disjunsn  30499  brabgaf  30514  ac6sf2  30526  dfimafnf  30537  fimarab  30546  2ndresdju  30552  fmptcof2  30561  acunirnmpt2  30564  acunirnmpt2f  30565  aciunf1lem  30566  aciunf1  30567  ofpreima  30569  funcnv5mpt  30572  funcnv4mpt  30573  fnpreimac  30575  padct  30621  cnvoprabOLD  30622  f1od2  30623  fpwrelmap  30635  xrofsup  30657  iundisjfi  30684  nnindf  30700  nn0min  30701  fprodex01  30706  fsumiunle  30710  gsummpt2d  30878  gsumhashmul  30885  isarchiofld  31085  nsgmgc  31161  nsgqusf1olem1  31162  nsgqusf1olem3  31164  nsgqusf1o  31165  elrspunidl  31170  fedgmullem2  31275  reff  31353  locfinreflem  31354  cmpcref  31364  zarclsiin  31385  zarcls  31388  zarcmplem  31395  ordtconnlem1  31438  qqhval2  31494  prodindf  31553  esumeq12dva  31562  esumeq2dv  31568  esumrnmpt  31582  esumpad  31585  esumpad2  31586  esumadd  31587  gsumesum  31589  esumlub  31590  esumsnf  31594  esumpr  31596  esumrnmpt2  31598  esumfzf  31599  esumfsup  31600  esumpcvgval  31608  esumpmono  31609  esumcocn  31610  hasheuni  31615  esumcvg  31616  esumgect  31620  esum2dlem  31622  esum2d  31623  esumiun  31624  ldsysgenld  31690  sigapildsyslem  31691  sigapildsys  31692  ldgenpisyslem1  31693  fiunelros  31704  measvunilem  31742  measvunilem0  31743  measvuni  31744  measiun  31748  measinblem  31750  voliune  31759  volfiniune  31760  volmeas  31761  ddemeas  31766  oms0  31826  omssubadd  31829  carsgclctunlem1  31846  carsggect  31847  omsmeas  31852  eulerpartlemgvv  31905  dstrvprob  32000  ballotlemodife  32026  reprsuc  32157  reprdifc  32169  breprexplema  32172  breprexplemc  32174  circlemethhgt  32185  hgt750lemd  32190  bnj919  32309  bnj1146  32334  bnj1379  32373  bnj1385  32375  bnj1400  32378  bnj1534  32396  bnj1542  32400  bnj110  32401  bnj121  32413  bnj124  32414  bnj130  32417  bnj207  32424  bnj571  32449  bnj605  32450  bnj580  32456  bnj607  32459  bnj611  32461  bnj873  32467  bnj849  32468  bnj900  32472  bnj916  32476  bnj1000  32484  bnj964  32486  bnj981  32493  bnj985v  32496  bnj985  32497  bnj1014  32504  bnj1123  32529  bnj1128  32533  bnj1228  32554  bnj1204  32555  bnj1279  32561  bnj1307  32566  bnj1321  32570  bnj1388  32576  bnj1398  32577  bnj1408  32579  bnj1417  32584  bnj1444  32586  bnj1445  32587  bnj1446  32588  bnj1449  32591  bnj1467  32597  bnj1489  32599  bnj1312  32601  bnj1497  32603  bnj1518  32607  bnj1525  32612  bnj1529  32613  fineqvrep  32627  cvmcov  32788  untsucf  33214  ralxpes  33244  ralxp3  33252  ralxp3es  33254  setinds2  33320  dfon2lem1  33323  dfon2lem3  33325  trpredmintr  33365  frpoinsg  33376  frpoins2g  33378  frpoins3xpg  33380  frpoins3xp3g  33381  frinsg  33385  frins2g  33389  frins2  33390  nffrecs  33430  nosupbnd1  33550  nosupbnd2  33552  noinfbnd1  33565  noinfbnd2  33567  no3indslem  33744  finminlem  34137  bj-nexdvt  34507  bj-cbvaldv  34601  bj-cbval2vv  34603  bj-cbvex2vv  34604  bj-cbvaldvav  34605  bj-cbvexdvav  34606  ax11-pm2  34639  bj-dvelimdv  34655  bj-nfeel2  34658  bj-ceqsalv  34700  bj-vtocl  34722  bj-inrab2  34736  currysetlem  34746  currysetlem1  34748  bj-opabco  34969  mptsnunlem  35121  exlimim  35125  exellim  35127  topdifinfindis  35129  topdifinffinlem  35130  icorempo  35134  isbasisrelowllem1  35138  isbasisrelowllem2  35139  relowlssretop  35146  finxpreclem2  35173  finxpreclem6  35179  fvineqsneu  35194  fvineqsneq  35195  wl-euequf  35341  wl-sb8eut  35344  phpreu  35373  matunitlindflem2  35386  ptrest  35388  ptrecube  35389  poimirlem2  35391  poimirlem23  35412  poimirlem24  35413  poimirlem25  35414  poimirlem26  35415  poimirlem27  35416  poimirlem28  35417  heicant  35424  mbfposadd  35436  itgabsnc  35458  itggt0cn  35459  ftc1anclem5  35466  upixp  35499  indexa  35503  indexdom  35504  filbcmb  35510  sdclem2  35512  sdclem1  35513  fdc1  35516  totbndbnd  35559  sbcalf  35884  sbcexf  35885  scottexf  35938  scott0f  35939  eqrelf  36007  fsumshftd  36578  riotasv2d  36583  riotasv2s  36584  riotasv3d  36586  glbconxN  37004  pmapglbx  37395  pmapglb2xN  37398  cdleme26ee  37986  cdleme31sn  38006  cdleme31sn1  38007  cdlemefr29exN  38028  cdlemefs32sn1aw  38040  cdleme43fsv1snlem  38046  cdleme41sn3a  38059  cdleme32fva  38063  cdleme32d  38070  cdleme32f  38072  cdleme40m  38093  cdleme40n  38094  cdleme42b  38104  cdlemk36  38539  cdlemk38  38541  cdlemkid  38562  cdlemk19x  38569  cdlemk11t  38572  dihvalcqpre  38861  mapdheq  39354  hdmap1eq  39427  hdmapval2lem  39457  lcmineqlem9  39654  lcmineqlem12  39657  aks4d1p1p2  39686  sticksstones1  39697  metakunt33  39737  mzpexpmpt  40123  eq0rabdioph  40154  rexrabdioph  40172  rexfrabdioph  40173  elnn0rabdioph  40181  dvdsrabdioph  40188  fphpd  40194  monotuz  40319  monotoddzz  40321  oddcomabszz  40322  setindtr  40402  dford4  40407  wdom2d2  40413  aomclem6  40440  aomclem8  40442  flcidc  40555  areaquad  40603  rababg  40710  ss2iundv  40798  cbviuneq12dv  40800  gneispace  41274  mnringvald  41357  mnringmulrcld  41372  nfscott  41383  scottabf  41384  scottab  41385  mnuprdlem4  41419  binomcxplemdvsum  41495  binomcxplemnotnn0  41496  aaanv  41528  pm11.57  41529  pm11.58  41530  pm11.59  41531  pm11.71  41537  pm14.12  41561  ssralv2  41673  tratrb  41678  iunconnlem2  42077  evth2f  42080  elunif  42081  fvelrnbf  42083  evthf  42092  fnchoice  42094  sumpair  42100  rfcnnnub  42101  refsum2cn  42103  elabrexg  42111  uzwo4  42123  fiiuncl  42135  fiunicl  42137  elintdv  42151  ssd  42152  cbvmpo2  42169  cbvmpo1  42170  eliin2f  42176  eliuniin2  42191  cbvrabv2  42198  cbvrabv2w  42199  suprnmpt  42232  dffo3f  42239  disjf1  42242  disjrnmpt2  42248  disjf1o  42251  fompt  42252  disjinfi  42253  choicefi  42262  iunmapsn  42279  axccdom  42284  dmrelrnrel  42287  axccd  42290  funimassd  42292  fmptf  42304  rnmptlb  42309  rnmptbddlem  42310  rnmptbd2lem  42315  rnmptbdlem  42322  rnmptbd  42323  upbdrech  42366  ssfiunibd  42370  supxrgere  42394  iuneqfzuzlem  42395  supxrgelem  42398  supxrge  42399  suplesup  42400  infrpge  42412  xralrple2  42415  infxr  42428  infxrunb2  42429  infleinf  42433  xrralrecnnle  42444  xrralrecnnge  42452  supxrunb3  42461  supxrleubrnmpt  42468  infleinf2  42476  unb2ltle  42477  rexabslelem  42480  rexabsle  42481  allbutfiinf  42482  suprleubrnmpt  42484  infrnmptle  42485  infxrunb3rnmpt  42490  uzublem  42492  uzub  42493  supminfrnmpt  42507  infxrpnf  42509  supxrleubrnmptf  42515  infxrgelbrnmpt  42518  infrpgernmpt  42529  supminfxr2  42533  monoordxr  42547  monoord2xr  42549  iccshift  42580  iooshift  42584  iooiinicc  42604  iooiinioc  42618  fsumclf  42636  fsummulc1f  42637  fsumnncl  42638  fsumsplit1  42639  fsumf1of  42641  fsumiunss  42642  fsumreclf  42643  fsumlessf  42644  fsumsermpt  42646  fmul01  42647  fmuldfeqlem1  42649  fmuldfeq  42650  fmul01lt1lem1  42651  fmul01lt1lem2  42652  fmul01lt1  42653  fprodsplit1  42660  fprodexp  42661  fprodabs2  42662  mccllem  42664  mccl  42665  fprodcnlem  42666  fprodcn  42667  climexp  42672  climsuse  42675  climrecf  42676  climinff  42678  climaddf  42682  mullimc  42683  ellimcabssub0  42684  islptre  42686  climf  42689  mullimcf  42690  rexlim2d  42692  idlimc  42693  limcperiod  42695  limcrecl  42696  sumnnodd  42697  islpcn  42706  limsupre  42708  limcleqr  42711  neglimc  42714  addlimc  42715  0ellimcdiv  42716  limclner  42718  climsubmpt  42727  climreclf  42731  climf2  42733  fnlimcnv  42734  climeldmeqmpt  42735  clim2f2  42737  climfveqmpt  42738  fnlimfvre  42741  allbutfifvre  42742  climleltrp  42743  fnlimf  42745  fnlimabslt  42746  climfveqmpt3  42749  climeldmeqf  42750  limsupref  42752  limsupbnd1f  42753  climbddf  42754  climeqf  42755  climeldmeqmpt3  42756  limsuplesup  42766  limsuppnfd  42769  limsupub  42771  limsupres  42772  climinf2lem  42773  climinf2  42774  limsuppnf  42778  limsupubuzlem  42779  limsupubuz  42780  climinf2mpt  42781  climinfmpt  42782  climinf3  42783  limsupmnflem  42787  limsupmnf  42788  limsupequz  42790  limsupre2  42792  limsupmnfuzlem  42793  limsupmnfuz  42794  limsupequzmptf  42798  limsupre3lem  42799  limsupre3  42800  limsupre3uzlem  42802  limsupre3uz  42803  limsupreuz  42804  limsupvaluz2  42805  limsupreuzmpt  42806  supcnvlimsup  42807  climuzlem  42810  climuz  42811  climisp  42813  lmbr3  42814  climrescn  42815  climxrrelem  42816  climxrre  42817  liminfcl  42830  liminfval2  42835  limsup10exlem  42839  liminflelimsuplem  42842  limsupgtlem  42844  limsupgt  42845  climliminflimsupd  42868  liminfreuzlem  42869  liminfreuz  42870  liminfltlem  42871  liminflt  42872  limsupub2  42879  xlimpnfxnegmnf  42881  liminflbuz2  42882  liminfpnfuz  42883  liminflimsupxrre  42884  xlimmnfvlem1  42899  xlimmnfvlem2  42900  xlimmnfv  42901  xlimpnfvlem1  42903  xlimpnfvlem2  42904  xlimpnfv  42905  xlimmnf  42908  xlimpnf  42909  xlimmnfmpt  42910  xlimpnfmpt  42911  climxlim2lem  42912  dfxlim2  42915  cncfshift  42941  icccncfext  42954  cncficcgt0  42955  cncfiooicc  42961  cncfioobd  42964  fprodcncf  42967  fprodsubrecnncnvlem  42974  fprodaddrecnncnvlem  42976  dvmptmulf  43004  dvnmptdivc  43005  dvnmul  43010  dvmptfprodlem  43011  dvmptfprod  43012  dvnprodlem1  43013  dvnprodlem2  43014  iblsplitf  43037  iblspltprt  43040  itgioocnicc  43044  iblcncfioo  43045  itgspltprt  43046  itgperiod  43048  stoweidlem3  43070  stoweidlem14  43081  stoweidlem17  43084  stoweidlem19  43086  stoweidlem20  43087  stoweidlem26  43093  stoweidlem27  43094  stoweidlem28  43095  stoweidlem29  43096  stoweidlem31  43098  stoweidlem34  43101  stoweidlem35  43102  stoweidlem36  43103  stoweidlem39  43106  stoweidlem42  43109  stoweidlem43  43110  stoweidlem44  43111  stoweidlem46  43113  stoweidlem48  43115  stoweidlem49  43116  stoweidlem50  43117  stoweidlem51  43118  stoweidlem52  43119  stoweidlem53  43120  stoweidlem54  43121  stoweidlem56  43123  stoweidlem57  43124  stoweidlem59  43126  stoweidlem60  43127  stoweidlem61  43128  stoweidlem62  43129  stoweid  43130  wallispilem3  43134  stirlinglem13  43153  stirling  43156  fourierdlem16  43190  fourierdlem21  43195  fourierdlem22  43196  fourierdlem31  43205  fourierdlem39  43213  fourierdlem48  43221  fourierdlem51  43224  fourierdlem53  43226  fourierdlem68  43241  fourierdlem69  43242  fourierdlem71  43244  fourierdlem73  43246  fourierdlem77  43250  fourierdlem80  43253  fourierdlem81  43254  fourierdlem82  43255  fourierdlem83  43256  fourierdlem86  43259  fourierdlem87  43260  fourierdlem89  43262  fourierdlem91  43264  fourierdlem93  43266  fourierdlem94  43267  fourierdlem103  43276  fourierdlem104  43277  fourierdlem112  43285  fourierdlem113  43286  elaa2  43301  etransclem18  43319  etransclem22  43323  etransclem23  43324  etransclem32  43333  etransclem35  43336  etransclem44  43345  etransclem46  43347  etransclem48  43349  rrndistlt  43357  ioorrnopnlem  43371  intsaluni  43394  salexct  43399  subsaliuncl  43423  sge00  43440  sge0revalmpt  43442  sge0sn  43443  sge0f1o  43446  sge0gerp  43459  sge0pnffigt  43460  sge0lefi  43462  sge0ltfirp  43464  sge0resrnlem  43467  sge0resplit  43470  sge0lempt  43474  sge0iunmptlemfi  43477  sge0p1  43478  sge0iunmptlemre  43479  sge0fodjrnlem  43480  sge0iunmpt  43482  sge0rpcpnf  43485  sge0ltfirpmpt2  43490  sge0isum  43491  sge0xp  43493  sge0ad2en  43495  sge0isummpt2  43496  sge0xaddlem1  43497  sge0xaddlem2  43498  sge0xadd  43499  sge0pnffsumgt  43506  sge0gtfsumgt  43507  sge0uzfsumgt  43508  sge0seq  43510  sge0reuz  43511  sge0reuzb  43512  iundjiun  43524  meadjiunlem  43529  meadjiun  43530  ismeannd  43531  voliunsge0lem  43536  meaiuninclem  43544  meaiunincf  43547  meaiuninc3v  43548  meaiuninc3  43549  meaiininclem  43550  meaiininc  43551  meaiininc2  43552  caragenfiiuncl  43579  omeiunltfirp  43583  carageniuncllem1  43585  carageniuncllem2  43586  caratheodorylem2  43591  0ome  43593  isomenndlem  43594  hoicvrrex  43620  ovnsupge0  43621  ovnlecvr  43622  ovnlerp  43626  ovncvrrp  43628  ovn0lem  43629  ovnsubaddlem1  43634  ovnsubaddlem2  43635  hoidmvcl  43646  hsphoidmvle2  43649  hsphoidmvle  43650  hoidmvval0  43651  sge0hsphoire  43653  hoidmvval0b  43654  hoidmv1lelem1  43655  hoidmv1lelem2  43656  hoidmv1lelem3  43657  hoidmvlelem1  43659  hoidmvlelem2  43660  hoidmvlelem3  43661  hoidmvlelem4  43662  hoidmvlelem5  43663  hoidmvle  43664  ovnhoilem1  43665  ovnhoilem2  43666  ovnhoi  43667  ovnlecvr2  43674  hspdifhsp  43680  hoidifhspdmvle  43684  hoiqssbllem3  43688  hspmbllem1  43690  hspmbllem2  43691  opnvonmbllem1  43696  opnvonmbllem2  43697  ovnsubadd2lem  43709  ovolval5lem1  43716  ovnovollem1  43720  ovnovollem2  43721  hoimbl2  43729  vonhoire  43736  iinhoiicclem  43737  iinhoiicc  43738  iunhoiioolem  43739  iunhoiioo  43740  vonioolem1  43744  vonioolem2  43745  vonioo  43746  vonicclem1  43747  vonicclem2  43748  vonicc  43749  vonn0ioo2  43754  vonn0icc2  43756  vonct  43757  pimltmnf2  43761  pimgtpnf2  43767  salpreimagelt  43768  salpreimalegt  43770  pimltpnf2  43773  pimgtmnf2  43774  pimdecfgtioc  43775  pimincfltioc  43776  pimdecfgtioo  43777  pimincfltioo  43778  preimageiingt  43780  preimaleiinlt  43781  salpreimagtge  43784  salpreimaltle  43785  salpreimalelt  43788  salpreimagtlt  43789  issmff  43793  sssmf  43797  mbfresmf  43798  cnfsmf  43799  incsmflem  43800  incsmf  43801  smfsssmf  43802  issmflelem  43803  issmfle  43804  smfconst  43808  issmfgtlem  43814  issmfgt  43815  smfpimltxrmpt  43817  smfmbfcex  43818  smfaddlem1  43821  smfaddlem2  43822  smfadd  43823  decsmflem  43824  decsmf  43825  smfpreimagtf  43826  issmfgelem  43827  issmfge  43828  smflimlem2  43830  smflimlem4  43832  smflim  43835  smfpimgtxr  43838  smfpimgtxrmpt  43842  smfpimioo  43844  smfresal  43845  smfrec  43846  smfres  43847  smfmullem2  43849  smfmullem4  43851  smfmul  43852  smfpimbor1lem2  43856  smf2id  43858  smfco  43859  smflim2  43862  smfpimcc  43864  smflimmpt  43866  smfsuplem1  43867  smfsuplem3  43869  smfsup  43870  smfsupmpt  43871  smfsupxr  43872  smfinflem  43873  smfinf  43874  smfinfmpt  43875  smflimsuplem3  43878  smflimsuplem4  43879  smflimsuplem5  43880  smflimsuplem7  43882  smflimsuplem8  43883  smflimsup  43884  smflimsupmpt  43885  smfliminflem  43886  smfliminf  43887  smfliminfmpt  43888  or2expropbilem1  44049  or2expropbilem2  44050  or2expropbi  44051  cfsetsnfsetf  44074  cfsetsnfsetfo  44076  rexsb  44107  reuf1odnf  44116  2reu8i  44122  ffnafv  44180  tz6.12c-afv2  44251  f1oresf1o2  44300  iccelpart  44403  iccpartdisj  44407  dfich2  44428  ichbi12i  44430  ichnfimlem  44433  ich2exprop  44441  ichnreuop  44442  ichreuopeq  44443  sprsymrelfo  44467  reupr  44492  reuopreuprim  44496  mogoldbb  44755  2zrngagrp  45019  2zrngmmgm  45022  opeliun2xp  45186  cbvmpox2  45189  ovmpordx  45193  1arymaptfo  45507  2arymaptfo  45518  mo0sn  45677  isthincd2lem1  45768  nfintd  45816  nfiund  45817  nfiundg  45818  iunord  45819  spcdvw  45822  nfsetrecs  45829  setrec1lem2  45831  setrec1  45834  setrec2fun  45835  aacllem  45942