Theorem nfv 1947

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

This proof depends on syntax axioms:  Ⅎwnf 1816

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

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfvd  1948  cbvaldw  2369  cbval2v  2374  dvelimhw  2376  pm11.53  2377  19.12vv  2378  eeanv  2380  eeeanv  2381  ee4anv  2382  sbnf2  2389  exsb  2390  2exsb  2391  sbbibvv  2393  cbvsbvf  2394  cleljustALT2  2396  spimv  2421  spimev  2423  chvarv  2427  cbvalv  2431  cbvexv  2432  cbvald  2438  cbvaldva  2440  cbvexdva  2441  cbval2  2442  axc16i  2467  dvelimnf  2484  sbel2x  2505  sbiedv  2535  2sbiev  2536  sbid2v  2540  sbhb  2552  2sb8e  2561  nfmod2  2585  nfmodv  2586  mof  2590  mo4f  2594  euf  2603  sb8eulem  2625  cbvmow  2630  sbmo  2641  moexexvw  2655  moexexv  2666  2mo  2675  2eu6  2683  axextmo  2738  nulmo  2739  abbib  2831  cleqh  2891  nfcv  2924  nfeqd  2934  nfeld  2935  nfabdw  2945  nfabd  2946  dvelimdc  2948  nfcvf  2950  cleqf  2952  r19.29af  3273  rexbidvALT  3279  rexbidvaALT  3280  2ralbida  3287  r19.12  3313  reean  3314  cbvrexsvw  3316  sbralieOLD  3342  cbvralf  3347  cbvralv  3351  cbvrexv  3352  cbvralsv  3353  cbvrexsv  3354  cbvrmow  3392  cbvreu  3406  cbvrmov  3408  cbvreuv  3409  cbvrab  3452  cbvexeqsetf  3468  ceqsex2  3503  vtocl2gaf  3541  vtocl3gaf  3542  spc2ed  3558  rspct  3565  rspc  3567  rspce  3568  eqvincf  3607  elrab3t  3647  ralab2  3658  rexab2  3660  mob2  3676  mob  3678  reu2  3686  rmo4f  3696  reu2eqd  3697  cdeqab1  3733  nfcdeq  3738  sbcco  3768  cbvsbcv  3778  elrabsf  3787  sbc2iegf  3816  reu8nf  3827  rmo2  3837  rmo3  3839  rmoanimALT  3846  nfcsb1d  3872  nfcsbd  3875  csbiebt  3879  csbie2t  3888  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  cbvralv2  3896  cbvrexv2  3897  rspc2vd  3898  dfssf  3925  rabss3d  4032  eqrrabd  4037  uniiunlem  4038  ab0orv  4335  ab0orvALT  4336  sbcnestgw  4384  sbcnestg  4389  sbnfc2  4400  r19.3rzvOLD  4463  r19.28zv  4465  r19.27zv  4470  2reu4lem  4482  nfifd  4515  reusngf  4638  reusng  4641  rexreusng  4643  reuprg0  4666  rabsnifsb  4686  euabsn  4690  nfunid  4876  eluniab  4884  nfint  4920  iuneqconst  4966  disjiun  5095  disjxun  5105  nfopabd  5177  cbvopab  5181  cbvopab1  5183  cbvopab1g  5184  cbvopab2  5185  cbvopab1s  5186  mpteq12da  5192  mpteq12f  5194  cbvmptf  5209  cbvmptfg  5210  axrep1  5237  axrep2  5239  axrep3  5240  axrep4OLD  5243  axrep5  5244  zfrepclf  5250  reusv2lem3  5369  reusv2lem4  5370  reusv2  5372  reusv3  5374  alxfr  5376  ralxfrALT  5384  axprlem3OLD  5398  axprlem4OLD  5399  axprlem5OLD  5400  copsex2t  5473  iunopeqop  5502  iunopeqopOLD  5503  rexopabb  5510  opelopabaf  5527  nfso  5574  pofun  5585  isso2i  5604  nffr  5632  opeliunxp  5726  opeliun2xp  5727  opeliunxp2  5822  ralxpf  5830  dfdmf  5884  dfrnf  5938  elrnmpt1  5948  dfrel4  6188  reuop  6295  frpoinsg  6345  frpoins2g  6347  wfis2g  6357  nfiotadw  6496  nfiotad  6498  cbviotaw  6500  cbviota  6502  cbviotav  6503  sb8iota  6504  iota2d  6525  iota2  6526  dffun6f  6552  imadif  6621  isarep1  6625  isarep2  6626  fv3  6900  tz6.12f  6907  funimassd  6948  fvelimad  6949  feqmptdf  6952  fimarab  6956  opabiotafun  6962  funfv2f  6971  fvmptd  6998  fvmptd2f  7007  fvmptdv  7008  fvmptt  7011  fvopab5  7024  eqfnfv2f  7030  ralrnmptw  7091  ralrnmpt  7093  dffo3f  7103  f1ompt  7108  fompt  7115  ffnfv  7116  ffnfvf  7117  f1ossf1o  7126  fmptco  7127  elabrex  7243  elabrexg  7244  dff13f  7256  fsnex  7288  fliftfun  7317  cbvriotaw  7383  cbvriota  7387  cbvriotav  7388  riota2  7399  riotaeqimp  7400  riota5f  7402  oprabv  7477  nfoprab  7481  mpoeq123  7489  cbvoprab1  7504  cbvoprab2  7505  cbvoprab12  7506  cbvoprab3  7508  cbvmpox  7510  ralrnmpo  7556  ovmpodx  7568  ovmpodf  7573  ovmpodv  7574  ov3  7580  ovmpt3rab1  7676  ofrfval2  7703  onminex  7805  tfis  7855  tfis2  7857  tfisi  7859  tfinds  7860  tfindes  7863  findes  7901  fiun  7944  f1iun  7945  abrexex2g  7965  opabex3d  7966  opabex3rd  7967  opabex3  7968  dfoprab4f  8057  fmpox  8068  offval22  8089  ovmptss  8094  ralxpes  8138  ralxp3  8140  ralxp3es  8141  frpoins3xpg  8142  frpoins3xp3g  8143  opeliunxp2f  8212  tposoprab  8264  fvmpocurryd  8273  nffrecs  8286  tfr3  8392  nfrdg  8407  tz7.48-1  8436  tz7.49  8438  naddsuc2  8694  eqerlem  8736  erovlem  8817  mptelixpg  8946  boxcutc  8952  dom2lem  9002  xpf1o  9141  mapxpen  9145  findcard2  9163  pssnn  9167  nneneq  9204  ac6sfi  9258  fiint  9300  indexfi  9331  wdom2d  9556  ixpiunwdom  9566  cantnflem1  9672  nfttrcld  9693  setinds2  9734  frinsg  9737  frins2  9740  r1val1  9772  rankuni2b  9839  nfscott  9875  scottabf  9882  scottab  9883  scottexsOLD  9886  scott0bsOLD  9888  dfac8clem  10039  acni2  10053  aceq1  10124  dfac5lem5  10134  kmlem15  10171  infpssrlem4  10312  fin23lem27  10334  hsmexlem2  10433  hsmexlem4  10435  axcc3  10444  domtriomlem  10448  axdc3lem2  10457  axdc3lem4  10459  axdc4lem  10461  ac6c4  10487  zorn2lem4  10505  zorn2lem5  10506  iunfo  10551  iundom2g  10552  uniimadomf  10557  konigthlem  10581  axrepndlem2  10606  axunnd  10609  axpowndlem2  10611  axpowndlem4  10613  axregndlem2  10616  axacndlem5  10624  zfcndrep  10627  zfcndinf  10631  pwfseqlem4a  10674  pwfseqlem4  10675  tskuni  10796  gruiin  10823  reclem2pr  11061  dedekind  11401  dedekindle  11402  fimaxre3  12189  nn0ind-raph  12725  uzind4s  12961  nnwof  12967  lbzbi  12989  fzrevral  13671  rabssnn0fi  14054  fsuppmapnn0fiublem  14058  fsuppmapnn0fiub  14059  fsuppmapnn0fiubex  14060  seqof2  14128  reuccatpfxs1  14820  cotr2g  15053  rlim2  15587  ello1mpt  15612  climeu  15646  o1compt  15678  summolem2a  15805  zsum  15808  sumss  15814  sumss2  15816  fsumcvg2  15817  fsumclf  15828  fsumsplitf  15832  fsumsplit1  15835  fsum2dlem  15860  fsum00  15889  o1fsum  15904  nfcprod1  16001  nfcprod  16002  prodmolem2a  16027  zprod  16030  fprod  16034  fprodntriv  16035  prodss  16040  fprodn0  16072  fprod2dlem  16073  fprodsplitf  16081  fprodsplit1f  16083  fprodle  16089  fprodmodd  16090  lcmfunsnlem1  16733  lcmfunsnlem2lem1  16734  lcmfunsnlem2  16736  coprmprod  16757  coprmproddvdslem  16758  prmind2  16781  iserodd  16933  pcmpt  16990  pcmptdvds  16992  prmolefac  17144  mreexexd  17742  catpropd  17803  invfuc  18072  natpropd  18074  fucpropd  18075  initoeu2  18111  acsmapd  18648  nfchnd  18705  symgval  19504  gsumsnd  20085  gsumsnf  20086  gsumunsnfd  20090  gsummptf1o  20096  gsummpt1n0  20098  gsum2d2lem  20106  gsumcom2  20108  gsummptnn0fz  20119  dprd2d2  20179  rngqiprngimf1  21509  gsummoncoe1  22539  gsumply1eq  22540  mdetralt2  22837  mdetunilem2  22841  madugsum  22871  gsummatr01lem4  22886  matunitlindflem2  22908  cpmatmcllem  22949  cayleyhamilton1  23123  neiptopnei  23363  neiptopreu  23364  neitr  23411  fiuncmp  23635  iunconnlem  23658  iunconn  23659  2ndcdisj  23688  dissnlocfin  23761  elptr2  23806  ptbasfi  23813  ptcld  23845  ptcldmpt  23846  ptclsg  23847  ptcnplem  23853  ptcnp  23854  cnmpt11  23895  cnmpt21  23903  cnmptcom  23910  imasnopn  23922  imasncld  23923  imasncls  23924  xkocnv  24046  elmptrab  24059  isfildlem  24089  alexsubALTlem3  24281  cnextfvval  24297  utopsnneiplem  24479  isucn2  24510  cfilucfil  24791  blval2  24794  restmetu  24802  ovoliunlem3  25738  ovoliun  25739  ovoliun2  25740  ovoliunnul  25741  finiunmbl  25778  volfiniun  25781  iundisj  25782  iunmbl  25787  voliun  25788  iunmbl2  25791  mbfeqalem1  25875  mbfsup  25898  mbfinf  25899  mbflim  25902  itg2splitlem  25982  itg2split  25983  isibl2  26000  cbvitg  26010  itgeqa  26048  itgss3  26049  itgfsum  26061  itgabs  26069  itggt0  26078  itgcn  26079  limcmpt  26117  limciun  26128  dvmptfsum  26209  dvlipcn  26228  dvfsumlem2  26261  dvfsumlem4  26263  dvfsumrlim  26265  dvfsum2  26268  itgsubst  26283  coeeq2  26475  dgrle  26476  ulmss  26640  leibpi  27187  rlimcnp  27210  rlimcnp2  27211  o1cxp  27219  lgamgulmlem2  27274  lgamgulmlem6  27278  fsumdvdscom  27429  lgseisenlem2  27620  2sqmo  27681  2sqreulem4  27698  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  nosupbnd1  27958  nosupbnd2  27960  noinfbnd1  27973  noinfbnd2  27975  bdayiun  28188  bdaypw2n0bndlem  28736  istrkg2ld  28809  prlngmo2  29321  mpteleeOLD  29360  gropd  29496  grstructd  29497  clwwlknonclwlknonf1o  30850  dlwwlknondlwlknonf1o  30853  ex-natded9.26  30907  isch3  31730  atom1d  32842  chirred  32884  sbc2iedf  32949  rspc2daf  32950  19.9d2r  32954  opreu2reuALT  32960  mo5f  32972  reuxfrdf  32974  foresf1o  32987  elabreximdv  32994  iinabrex  33050  cbvdisjf  33052  disjorf  33060  disjabrex  33063  iundisjf  33070  disjunsn  33075  brabgaf  33087  ac6sf2  33103  dfimafnf  33117  2ndresdju  33130  fmptcof2  33138  acunirnmpt2  33141  acunirnmpt2f  33142  aciunf1lem  33143  aciunf1  33144  ofpreima  33146  funcnv5mpt  33148  funcnv4mpt  33149  fnpreimac  33151  f1od2  33198  fpwrelmap  33212  xrofsup  33246  iundisjfi  33275  nnindf  33298  nn0min  33299  fprodex01  33303  fsumiunle  33307  prodindf  33316  gsummpt2d  33497  gsummptf1od  33503  gsummptfsf1o  33508  gsumhashmul  33515  suppgsumssiun  33520  gsumwrd2dccat  33526  isarchiofld  33647  elrgspnsubrunlem2  33696  nsgmgc  33849  nsgqusf1olem1  33850  nsgqusf1olem3  33852  nsgqusf1o  33853  elrspunidl  33864  elrspunsn  33865  deg1prod  34001  ply1gsumz  34017  ig1pmindeg  34020  mplvrpmga  34063  psrgsum  34066  psrmonprod  34070  esplylem  34084  esplyfv1  34087  esplyfval1  34091  esplyfvaln  34092  esplyind  34093  vieta  34098  exsslsb  34115  ply1degltdimlem  34140  fedgmullem2  34148  evls1fldgencl  34188  irngnzply1  34209  extdgfialglem2  34211  ply1annidllem  34219  algextdeglem6  34240  constrfin  34264  reff  34357  locfinreflem  34358  cmpcref  34368  zarclsiin  34389  zarcls  34392  zarcmplem  34399  ordtconnlem1  34442  qqhval2  34500  esumeq12dva  34550  esumeq2dv  34556  esumrnmpt  34570  esumpad  34573  esumpad2  34574  esumadd  34575  gsumesum  34577  esumlub  34578  esumsnf  34582  esumpr  34584  esumrnmpt2  34586  esumfzf  34587  esumfsup  34588  esumpcvgval  34596  esumpmono  34597  esumcocn  34598  hasheuni  34603  esumcvg  34604  esumgect  34608  esum2dlem  34610  esum2d  34611  esumiun  34612  ldsysgenld  34679  sigapildsyslem  34680  sigapildsys  34681  ldgenpisyslem1  34682  fiunelros  34693  measvunilem  34731  measvunilem0  34732  measvuni  34733  measiun  34737  measinblem  34739  voliune  34748  volfiniune  34749  volmeas  34750  ddemeas  34755  oms0  34816  omssubadd  34819  carsgclctunlem1  34836  carsggect  34837  omsmeas  34842  eulerpartlemgvv  34895  dstrvprob  34991  ballotlemodife  35017  reprsuc  35131  reprdifc  35143  breprexplema  35146  breprexplemc  35148  circlemethhgt  35159  hgt750lemd  35164  bnj919  35285  bnj1146  35308  bnj1379  35347  bnj1385  35349  bnj1400  35352  bnj1534  35370  bnj1542  35374  bnj110  35375  bnj121  35387  bnj124  35388  bnj130  35391  bnj207  35398  bnj571  35423  bnj605  35424  bnj580  35430  bnj607  35433  bnj611  35435  bnj873  35441  bnj849  35442  bnj900  35446  bnj916  35450  bnj1000  35458  bnj964  35460  bnj981  35467  bnj985v  35470  bnj985  35471  bnj1014  35478  bnj1123  35503  bnj1128  35507  bnj1228  35528  bnj1204  35529  bnj1279  35535  bnj1307  35540  bnj1321  35544  bnj1388  35550  bnj1398  35551  bnj1408  35553  bnj1417  35558  bnj1444  35560  bnj1445  35561  bnj1446  35562  bnj1449  35565  bnj1467  35571  bnj1489  35573  bnj1312  35575  bnj1497  35577  bnj1518  35581  bnj1525  35586  bnj1529  35587  dvelimalcased  35592  dvelimexcased  35594  fineqvrep  35648  axsepg2  35674  axsepg3  35675  axsepg3ALT  35676  axpowg2  35681  axpowg3  35682  onvf1odlem2  35709  cvmcov  35850  untsucf  36297  dfon2lem1  36368  dfon2lem3  36370  finminlem  36945  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  axtcond  37105  regsfromregtco  37165  regsfromsetind  37166  bj-nexdvt  37439  bj-cbvaldv  37550  bj-cbval2vv  37552  bj-cbvex2vv  37553  bj-cbvaldvav  37554  bj-cbvexdvav  37555  ax11-pm2  37587  bj-dvelimdv  37602  bj-nfeel2  37605  bj-ceqsalv  37645  bj-vtocl  37667  bj-inrab2  37680  currysetlem  37697  currysetlem1  37699  bj-axseprep  37827  bj-axreprepsep  37828  bj-opabco  37948  mptsnunlem  38100  exlimim  38104  exellim  38106  topdifinfindis  38108  topdifinffinlem  38109  icorempo  38113  isbasisrelowllem1  38117  isbasisrelowllem2  38118  relowlssretop  38125  finxpreclem2  38152  finxpreclem6  38158  fvineqsneu  38173  fvineqsneq  38174  wl-euequf  38345  wl-sb8eut  38349  wl-issetft  38353  phpreu  38366  ptrest  38376  ptrecube  38377  poimirlem2  38379  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  heicant  38412  mbfposadd  38424  itgabsnc  38446  itggt0cn  38447  ftc1anclem5  38454  upixp  38487  indexa  38491  indexdom  38492  filbcmb  38498  sdclem2  38500  sdclem1  38501  fdc1  38504  totbndbnd  38547  sbcalf  38870  sbcexf  38871  scottexf  38924  scott0f  38925  eqrelf  39014  ralrmo3  39120  disjqmap2  39582  fsumshftd  39833  riotasv2d  39838  riotasv2s  39839  riotasv3d  39841  glbconxN  40259  pmapglbx  40650  pmapglb2xN  40653  cdleme26ee  41241  cdleme31sn  41261  cdleme31sn1  41262  cdlemefr29exN  41283  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme41sn3a  41314  cdleme32fva  41318  cdleme32d  41325  cdleme32f  41327  cdleme40m  41348  cdleme40n  41349  cdleme42b  41359  cdlemk36  41794  cdlemk38  41796  cdlemkid  41817  cdlemk19x  41824  cdlemk11t  41827  dihvalcqpre  42116  mapdheq  42609  hdmap1eq  42682  hdmapval2lem  42712  lcmineqlem9  42911  lcmineqlem12  42914  aks4d1p1p2  42944  mndmolinv  42969  primrootsunit1  42971  primrootsunit  42972  primrootspoweq0  42980  aks6d1c1p5  42986  aks6d1c3  42997  aks6d1c4  42998  aks6d1c1rh  42999  aks6d1c2lem4  43001  aks6d1c2  43004  deg1gprod  43014  sticksstones1  43020  sticksstones11  43030  sticksstones16  43036  sticksstones22  43042  aks6d1c6lem2  43045  aks6d1c6isolem1  43048  aks6d1c6isolem2  43049  bcled  43052  bcle2d  43053  aks6d1c7lem3  43056  aks6d1c7  43058  rhmqusspan  43059  grpods  43068  unitscyglem1  43069  unitscyglem2  43070  unitscyglem3  43071  unitscyglem4  43072  unitscyglem5  43073  nfa1w  43529  mzpexpmpt  43598  eq0rabdioph  43629  rexrabdioph  43643  rexfrabdioph  43644  elnn0rabdioph  43652  dvdsrabdioph  43659  fphpd  43665  monotuz  43790  monotoddzz  43792  oddcomabszz  43793  setindtr  43873  dford4  43878  wdom2d2  43884  aomclem6  43908  aomclem8  43910  flcidc  44019  areaquad  44065  unielss  44067  onsucf1lem  44118  oaun3lem1  44223  nadd1suc  44241  rababg  44422  ss2iundv  44508  cbviuneq12dv  44510  gneispace  44982  mnringvald  45059  mnringmulrcld  45074  mnuprdlem4  45107  ismnushort  45133  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  aaanv  45220  pm11.57  45221  pm11.58  45222  pm11.59  45223  pm11.71  45229  pm14.12  45253  ssralv2  45362  tratrb  45367  iunconnlem2  45765  modelaxreplem3  45811  modelaxrep  45812  permaxrep  45837  evth2f  45857  elunif  45858  fvelrnbf  45860  evthf  45869  fnchoice  45871  sumpair  45877  rfcnnnub  45878  refsum2cn  45880  uzwo4  45895  fiiuncl  45907  fiunicl  45909  elintdv  45921  ssd  45922  cbvmpo2  45937  cbvmpo1  45938  eliin2f  45944  eliuniin2  45960  cbvrabv2  45967  suprnmpt  46014  disjf1  46023  disjrnmpt2  46028  disjf1o  46031  disjinfi  46032  choicefi  46039  iunmapsn  46055  axccdom  46060  dmrelrnrel  46064  axccd  46066  fmptf  46076  rnmptlb  46080  rnmptbddlem  46081  rnmptbd2lem  46085  rnmptbdlem  46092  rnmptbd  46093  fmptff  46106  upbdrech  46146  ssfiunibd  46150  supxrgere  46171  iuneqfzuzlem  46172  supxrgelem  46175  supxrge  46176  suplesup  46177  infrpge  46189  xralrple2  46192  infxr  46204  infxrunb2  46205  infleinf  46209  xrralrecnnle  46220  xrralrecnnge  46227  supxrunb3  46236  supxrleubrnmpt  46242  infleinf2  46250  unb2ltle  46251  rexabslelem  46254  rexabsle  46255  allbutfiinf  46256  suprleubrnmpt  46258  infrnmptle  46259  infxrunb3rnmpt  46264  uzublem  46266  uzub  46267  supminfrnmpt  46281  infxrpnf  46282  supxrleubrnmptf  46287  infxrgelbrnmpt  46290  infrpgernmpt  46301  supminfxr2  46305  monoordxr  46318  monoord2xr  46320  caucvgbf  46325  cvgcaule  46327  rexanuz2nf  46328  iccshift  46356  iooshift  46360  iooiinicc  46380  iooiinioc  46394  fsummulc1f  46409  fsumnncl  46410  fsumf1of  46412  fsumiunss  46413  fsumreclf  46414  fsumlessf  46415  fsumsermpt  46417  fmul01  46418  fmuldfeqlem1  46420  fmuldfeq  46421  fmul01lt1lem1  46422  fmul01lt1lem2  46423  fmul01lt1  46424  fprodsplit1  46431  fprodexp  46432  fprodabs2  46433  mccllem  46435  mccl  46436  fprodcnlem  46437  fprodcn  46438  climexp  46443  climsuse  46446  climrecf  46447  climinff  46449  climaddf  46453  mullimc  46454  ellimcabssub0  46455  islptre  46457  climf  46460  mullimcf  46461  rexlim2d  46463  idlimc  46464  limcperiod  46466  limcrecl  46467  sumnnodd  46468  islpcn  46475  limsupre  46477  limcleqr  46480  neglimc  46483  addlimc  46484  0ellimcdiv  46485  limclner  46487  climsubmpt  46496  climreclf  46500  climf2  46502  fnlimcnv  46503  climeldmeqmpt  46504  clim2f2  46506  climfveqmpt  46507  fnlimfvre  46510  allbutfifvre  46511  climleltrp  46512  fnlimf  46514  fnlimabslt  46515  climfveqmpt3  46518  climeldmeqf  46519  limsupref  46521  limsupbnd1f  46522  climbddf  46523  climeqf  46524  climeldmeqmpt3  46525  limsuplesup  46535  limsuppnfd  46538  limsupub  46540  limsupres  46541  climinf2lem  46542  climinf2  46543  limsuppnf  46547  limsupubuzlem  46548  limsupubuz  46549  climinf2mpt  46550  climinfmpt  46551  climinf3  46552  limsupmnflem  46556  limsupmnf  46557  limsupequz  46559  limsupre2  46561  limsupmnfuzlem  46562  limsupmnfuz  46563  limsupequzmptf  46567  limsupre3lem  46568  limsupre3  46569  limsupre3uzlem  46571  limsupre3uz  46572  limsupreuz  46573  limsupvaluz2  46574  limsupreuzmpt  46575  supcnvlimsup  46576  climuzlem  46579  climuz  46580  climisp  46582  lmbr3  46583  climrescn  46584  climxrrelem  46585  climxrre  46586  liminfcl  46599  liminfval2  46604  limsup10exlem  46608  liminflelimsuplem  46611  limsupgtlem  46613  limsupgt  46614  climliminflimsupd  46637  liminfreuzlem  46638  liminfreuz  46639  liminfltlem  46640  liminflt  46641  limsupub2  46648  xlimpnfxnegmnf  46650  liminflbuz2  46651  liminfpnfuz  46652  liminflimsupxrre  46653  xlimmnfvlem1  46668  xlimmnfvlem2  46669  xlimmnfv  46670  xlimpnfvlem1  46672  xlimpnfvlem2  46673  xlimpnfv  46674  xlimmnf  46677  xlimpnf  46678  xlimmnfmpt  46679  xlimpnfmpt  46680  climxlim2lem  46681  dfxlim2  46684  cncfshift  46710  icccncfext  46723  cncficcgt0  46724  cncfiooicc  46730  cncfioobd  46733  fprodcncf  46736  fprodsubrecnncnvlem  46743  fprodaddrecnncnvlem  46745  dvmptmulf  46773  dvnmptdivc  46774  dvnmul  46779  dvmptfprodlem  46780  dvmptfprod  46781  dvnprodlem1  46782  dvnprodlem2  46783  iblsplitf  46806  iblspltprt  46809  itgioocnicc  46813  iblcncfioo  46814  itgspltprt  46815  itgperiod  46817  stoweidlem3  46839  stoweidlem14  46850  stoweidlem17  46853  stoweidlem19  46855  stoweidlem20  46856  stoweidlem26  46862  stoweidlem27  46863  stoweidlem28  46864  stoweidlem29  46865  stoweidlem31  46867  stoweidlem34  46870  stoweidlem35  46871  stoweidlem36  46872  stoweidlem39  46875  stoweidlem42  46878  stoweidlem43  46879  stoweidlem44  46880  stoweidlem46  46882  stoweidlem48  46884  stoweidlem49  46885  stoweidlem50  46886  stoweidlem51  46887  stoweidlem52  46888  stoweidlem53  46889  stoweidlem54  46890  stoweidlem56  46892  stoweidlem57  46893  stoweidlem59  46895  stoweidlem60  46896  stoweidlem61  46897  stoweidlem62  46898  stoweid  46899  wallispilem3  46903  stirlinglem13  46922  stirling  46925  fourierdlem16  46959  fourierdlem21  46964  fourierdlem22  46965  fourierdlem31  46974  fourierdlem39  46982  fourierdlem48  46990  fourierdlem51  46993  fourierdlem53  46995  fourierdlem68  47010  fourierdlem69  47011  fourierdlem71  47013  fourierdlem73  47015  fourierdlem77  47019  fourierdlem80  47022  fourierdlem81  47023  fourierdlem82  47024  fourierdlem83  47025  fourierdlem86  47028  fourierdlem87  47029  fourierdlem89  47031  fourierdlem91  47033  fourierdlem93  47035  fourierdlem94  47036  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fourierdlem113  47055  elaa2  47070  etransclem18  47088  etransclem22  47092  etransclem23  47093  etransclem32  47102  etransclem35  47105  etransclem44  47114  etransclem46  47116  etransclem48  47118  rrndistlt  47126  ioorrnopnlem  47140  saliuncl  47159  saliincl  47163  intsaluni  47165  salexct  47170  subsaliuncl  47194  sge00  47212  sge0revalmpt  47214  sge0sn  47215  sge0f1o  47218  sge0gerp  47231  sge0pnffigt  47232  sge0lefi  47234  sge0ltfirp  47236  sge0resrnlem  47239  sge0resplit  47242  sge0lempt  47246  sge0iunmptlemfi  47249  sge0p1  47250  sge0iunmptlemre  47251  sge0fodjrnlem  47252  sge0iunmpt  47254  sge0rpcpnf  47257  sge0ltfirpmpt2  47262  sge0isum  47263  sge0xp  47265  sge0ad2en  47267  sge0isummpt2  47268  sge0xaddlem1  47269  sge0xaddlem2  47270  sge0xadd  47271  sge0pnffsumgt  47278  sge0gtfsumgt  47279  sge0uzfsumgt  47280  sge0seq  47282  sge0reuz  47283  sge0reuzb  47284  iundjiun  47296  meadjiunlem  47301  meadjiun  47302  ismeannd  47303  voliunsge0lem  47308  meaiuninclem  47316  meaiunincf  47319  meaiuninc3v  47320  meaiuninc3  47321  meaiininclem  47322  meaiininc  47323  meaiininc2  47324  caragenfiiuncl  47351  omeiunltfirp  47355  carageniuncllem1  47357  carageniuncllem2  47358  caratheodorylem2  47363  0ome  47365  isomenndlem  47366  hoicvrrex  47392  ovnsupge0  47393  ovnlecvr  47394  ovnlerp  47398  ovncvrrp  47400  ovn0lem  47401  ovnsubaddlem1  47406  ovnsubaddlem2  47407  hoidmvcl  47418  hsphoidmvle2  47421  hsphoidmvle  47422  hoidmvval0  47423  sge0hsphoire  47425  hoidmvval0b  47426  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1lelem3  47429  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hoidmvlelem5  47435  hoidmvle  47436  ovnhoilem1  47437  ovnhoilem2  47438  ovnhoi  47439  ovnlecvr2  47446  hspdifhsp  47452  hoidifhspdmvle  47456  hoiqssbllem3  47460  hspmbllem1  47462  hspmbllem2  47463  opnvonmbllem1  47468  opnvonmbllem2  47469  ovnsubadd2lem  47481  ovolval5lem1  47488  ovnovollem1  47492  ovnovollem2  47493  hoimbl2  47501  vonhoire  47508  iinhoiicclem  47509  iinhoiicc  47510  iunhoiioolem  47511  iunhoiioo  47512  vonioolem1  47516  vonioolem2  47517  vonioo  47518  vonicclem1  47519  vonicclem2  47520  vonicc  47521  vonn0ioo2  47526  vonn0icc2  47528  vonct  47529  pimltmnf2f  47533  pimgtpnf2f  47541  salpreimagelt  47543  salpreimalegt  47545  pimltpnf2f  47548  pimgtmnf2  47550  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  preimageiingt  47556  preimaleiinlt  47557  salpreimagtge  47561  salpreimaltle  47562  salpreimalelt  47565  salpreimagtlt  47566  issmff  47570  sssmf  47574  mbfresmf  47575  cnfsmf  47576  incsmflem  47577  incsmf  47578  smfsssmf  47579  issmflelem  47580  issmfle  47581  smfconst  47585  issmfgtlem  47591  issmfgt  47592  smfpimltxrmptf  47594  smfmbfcex  47596  smfaddlem1  47599  smfaddlem2  47600  smfadd  47601  decsmflem  47602  decsmf  47603  smfpreimagtf  47604  issmfgelem  47605  issmfge  47606  smflimlem2  47608  smflimlem4  47610  smflim  47613  smfpimgtxr  47616  smfpimgtxrmptf  47620  smfpimioo  47623  smfresal  47624  smfrec  47625  smfres  47626  smfmullem2  47628  smfmullem4  47630  smfmul  47631  smfpimbor1lem2  47635  smf2id  47637  smfco  47638  smflim2  47642  smfpimcc  47644  smflimmpt  47646  smfsuplem1  47647  smfsuplem3  47649  smfsup  47650  smfsupmpt  47651  smfsupxr  47652  smfinflem  47653  smfinf  47654  smfinfmpt  47655  smflimsuplem3  47658  smflimsuplem4  47659  smflimsuplem5  47660  smflimsuplem7  47662  smflimsuplem8  47663  smflimsup  47664  smflimsupmpt  47665  smfliminflem  47666  smfliminf  47667  smfliminfmpt  47668  smfpimne2  47676  fsupdm  47678  smfsupdmmbllem  47680  smfsupdmmbl  47681  finfdm  47682  smfinfdmmbllem  47684  smfinfdmmbl  47685  tmachlem-agreesn  47783  or2expropbilem1  47928  or2expropbilem2  47929  or2expropbi  47930  cfsetsnfsetf  47954  cfsetsnfsetfo  47956  rexsb  47995  reuf1odnf  48003  2reu8i  48009  ffnafv  48067  tz6.12c-afv2  48138  f1oresf1o2  48187  iccelpart  48341  iccpartdisj  48345  dfich2  48366  ichbi12i  48368  ichnfimlem  48371  ich2exprop  48379  ichnreuop  48380  ichreuopeq  48381  sprsymrelfo  48405  reupr  48430  reuopreuprim  48434  mogoldbb  48709  2zrngagrp  49172  2zrngmmgm  49175  cbvmpox2  49274  ovmpordx  49278  1arymaptfo  49581  2arymaptfo  49592  mo0sn  49752  iinfssclem3  49990  iinfssc  49991  iinfsubc  49992  infsubc2  49995  iinfconstbas  50000  isthincd2lem1  50359  nfintd  50607  nfiund  50608  nfiundg  50609  iunord  50610  spcdvw  50613  nfsetrecs  50620  setrec1lem2  50622  setrec1  50625  setrec2fun  50626  pgindnf  50650  pgind  50651  aacllem  50780