Theorem nfv 1915

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

Syntax hints:  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfvd  1916  nfsbv  2338  nfsbvOLD  2339  cbvaldw  2347  cbval2v  2352  cbval2vOLD  2353  dvelimhw  2355  pm11.53  2356  19.12vv  2357  eeanv  2359  eeeanv  2360  sbnf2  2366  exsb  2367  2exsb  2368  sbbibvv  2370  cleljustALT2  2372  spimv  2397  spimev  2399  chvarv  2403  cbvalv  2407  cbvexv  2408  cbvald  2417  cbvaldva  2419  cbvexdva  2420  cbval2  2421  cbval2OLD  2422  axc16i  2447  dvelimnf  2464  sbel2x  2487  sbiedv  2523  2sbiev  2524  sbid2v  2528  sbhb  2540  2sb8e  2552  dfsb7ALT  2593  nfmod2  2617  nfmodv  2618  mof  2622  mo4f  2626  mo4OLD  2627  euf  2636  sb8eulem  2659  cbvmow  2663  sbmo  2675  moexexvw  2690  moexexv  2701  2mo  2710  2mos  2711  2eu6  2719  axextmo  2774  nulmo  2775  abbi  2865  cbvabw  2867  cleqh  2913  clelab  2933  nfcv  2955  nfeqd  2965  nfeld  2966  nfabdw  2976  nfabd  2977  dvelimdc  2979  nfcvf  2981  cleqf  2983  sbabel  2986  2ralbida  3196  rexbidvaALT  3278  rexbidvALT  3280  r19.12  3283  r19.29af  3289  reean  3319  rmobidva  3346  cbvralfwOLD  3383  cbvralf  3385  cbvreuw  3389  cbvrmow  3390  cbvreu  3394  cbvreuvw  3398  cbvralv  3399  cbvrexv  3400  cbvreuv  3401  cbvrmov  3402  cbvralsvw  3414  cbvrexsvw  3415  cbvralsv  3416  cbvrexsv  3417  cbvrabw  3437  cbvrab  3438  abv  3451  issetf  3454  ceqsalv  3479  ceqsralv  3480  ceqsexv  3489  ceqsex2  3491  vtoclgft  3501  vtocld  3504  vtoclALT  3508  vtoclgOLD  3516  vtocl2gaf  3524  vtocl3gaf  3525  vtocl3ga  3526  spcgvOLD  3544  spcegvOLD  3546  spc2ed  3550  rspct  3557  rspc  3559  rspce  3560  rspcvOLD  3567  rspcevOLD  3572  eqvincf  3591  ceqsexgvOLD  3596  clel2g  3600  elabgt  3609  elabg  3614  elab  3615  elab3g  3621  elrab3t  3627  ralab2  3636  ralab2OLD  3637  rexab2  3639  rexab2OLD  3640  mob2  3654  mob  3656  reu2  3664  rmo4f  3674  reu2eqd  3675  cdeqab1  3711  nfcdeq  3716  sbcco  3746  cbvsbcvw  3753  cbvsbcv  3755  sbcieg  3758  sbcied  3762  elrabsf  3764  sbcbidvOLD  3775  sbcg  3793  sbc2iegf  3795  sbc2ie  3796  reu8nf  3806  rmo2  3816  rmo3  3818  rmoanimALT  3824  csbeq2dv  3835  nfcsb1d  3850  nfcsbd  3853  csbiebt  3857  csbied  3864  csbie2t  3866  cbvrabcsfw  3869  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  cbvralv2  3874  cbvrexv2  3875  vtocl2dOLD  3876  rspc2vd  3877  dfss2f  3905  uniiunlem  4012  rspn0OLD  4267  ab0orv  4289  sbcnestgw  4328  sbcnestg  4333  sbnfc2  4344  r19.3rzv  4402  r19.28zv  4404  r19.27zv  4409  2reu4lem  4423  nfifd  4453  reusngf  4572  ralsng  4573  rexsng  4574  reusng  4575  rexreusng  4577  ralprg  4592  rexprg  4593  reuprg0  4598  rabsnifsb  4618  euabsn  4622  nfunid  4806  eluniab  4815  nfint  4848  elintab  4849  iuneqconst  4892  iineq2dv  4906  disjiun  5017  disjxun  5028  opabbidv  5096  nfopab  5098  cbvopab  5101  cbvopabv  5102  cbvopab1  5103  cbvopab1g  5104  cbvopab2  5105  cbvopab1s  5106  cbvopab1v  5107  mpteq12df  5112  mpteq12f  5113  mpteq12dv  5115  mpteq2dva  5125  cbvmptf  5129  cbvmptfg  5130  axrep1  5155  axrep2  5157  axrep3  5158  axrep4  5159  axrep5  5160  zfrepclf  5162  dtru  5236  reusv2lem3  5266  reusv2lem4  5267  reusv2  5269  reusv3  5271  alxfr  5273  ralxfrALT  5281  axprlem3  5291  axprlem4  5292  axprlem5  5293  copsex2t  5348  copsex2g  5349  iunopeqop  5376  rexopabb  5380  opelopabaf  5396  nfso  5444  pofun  5455  isso2i  5472  nffr  5493  opeliunxp  5583  opeliunxp2  5673  ralxpf  5681  dfdmf  5729  dfrnf  5784  elrnmpt1  5794  dfrel4  6015  reuop  6112  wfisg  6151  wfis2g  6155  nfiotadw  6286  nfiotad  6288  cbviotaw  6290  cbviotavw  6291  cbviota  6292  cbviotav  6293  sb8iota  6294  iota2d  6312  iota2  6313  dffun6f  6338  imadif  6408  funimaexg  6410  isarep1  6412  isarep2  6413  fv3  6663  tz6.12f  6669  tz6.12c  6670  fvelimad  6707  feqmptdf  6710  opabiotafun  6719  funfv2f  6727  fvmptd  6752  fvmptd2f  6761  fvmptdv  6762  fvmptt  6765  fvopab5  6777  eqfnfv2f  6783  ralrnmptw  6837  ralrnmpt  6839  f1ompt  6852  ffnfv  6859  ffnfvf  6860  f1ossf1o  6867  fmptco  6868  elabrex  6980  dff13f  6992  fsnex  7017  fliftfun  7044  cbvriotaw  7102  cbvriotavw  7103  cbvriota  7106  cbvriotav  7107  riota2  7118  riotaeqimp  7119  riota5f  7121  oprabv  7193  nfoprab  7197  oprabbidv  7199  mpoeq123  7205  cbvoprab1  7220  cbvoprab2  7221  cbvoprab12  7222  cbvoprab12v  7223  cbvoprab3  7224  cbvoprab3v  7225  cbvmpox  7226  ralrnmpo  7268  ovmpodx  7280  ovmpodf  7285  ovmpodv  7286  ov3  7291  ovmpt3rab1  7383  ofrfval2  7407  onminex  7502  tfis  7549  tfis2  7551  tfisi  7553  tfinds  7554  tfindes  7557  peano5  7585  findes  7593  fiun  7626  f1iun  7627  abrexex2g  7647  opabex3d  7648  opabex3rd  7649  opabex3  7650  dfoprab4f  7736  fmpox  7747  offval22  7766  ovmptss  7771  opeliunxp2f  7859  tposoprab  7911  fvmpocurryd  7920  nfwrecs  7932  tfr3  8018  nfrdg  8033  tz7.48-1  8062  tz7.49  8064  eqerlem  8306  erovlem  8376  mptelixpg  8482  boxcutc  8488  dom2lem  8532  xpf1o  8663  mapxpen  8667  nneneq  8684  pssnn  8720  findcard2  8742  ac6sfi  8746  fiint  8779  indexfi  8816  wdom2d  9028  ixpiunwdom  9038  cantnflem1  9136  r1val1  9199  rankuni2b  9266  scottexs  9300  scott0s  9301  dfac8clem  9443  acni2  9457  aceq1  9528  dfac5lem5  9538  kmlem15  9575  infpssrlem4  9717  fin23lem27  9739  hsmexlem2  9838  hsmexlem4  9840  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  ac6c4  9892  zorn2lem4  9910  zorn2lem5  9911  iunfo  9950  iundom2g  9951  uniimadomf  9956  konigthlem  9979  axrepndlem2  10004  axunnd  10007  axpowndlem2  10009  axpowndlem4  10011  axregndlem2  10014  axacndlem5  10022  zfcndrep  10025  zfcndinf  10029  pwfseqlem4a  10072  pwfseqlem4  10073  tskuni  10194  gruiin  10221  reclem2pr  10459  dedekind  10792  dedekindle  10793  fimaxre3  11575  nn0ind-raph  12070  uzind4s  12296  nnwof  12302  lbzbi  12324  fzrevral  12987  rabssnn0fi  13349  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  fsuppmapnn0fiubex  13355  seqof2  13424  reuccatpfxs1  14100  cotr2g  14327  rlim2  14845  ello1mpt  14870  climeu  14904  o1compt  14936  summolem2a  15064  zsum  15067  sumss  15073  sumss2  15075  fsumcvg2  15076  fsumsplitf  15090  fsum2dlem  15117  fsum00  15145  o1fsum  15160  nfcprod1  15256  nfcprod  15257  prodmolem2a  15280  zprod  15283  fprod  15287  fprodntriv  15288  prodss  15293  fprodn0  15325  fprod2dlem  15326  fprodsplitf  15334  fprodsplit1f  15336  fprodle  15342  fprodmodd  15343  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  coprmprod  15995  coprmproddvdslem  15996  prmind2  16019  iserodd  16162  pcmpt  16218  pcmptdvds  16220  prmolefac  16372  mreexexd  16911  catpropd  16971  invfuc  17236  natpropd  17238  fucpropd  17239  initoeu2  17268  acsmapd  17780  symgval  18489  gsumsnd  19065  gsumsnf  19066  gsumunsnfd  19070  gsummptf1o  19076  gsummpt1n0  19078  gsum2d2lem  19086  gsumcom2  19088  gsummptnn0fz  19099  dprd2d2  19159  gsummoncoe1  20933  gsumply1eq  20934  mdetralt2  21214  mdetunilem2  21218  madugsum  21248  gsummatr01lem4  21263  cpmatmcllem  21323  cayleyhamilton1  21497  neiptopnei  21737  neiptopreu  21738  neitr  21785  fiuncmp  22009  iunconnlem  22032  iunconn  22033  2ndcdisj  22061  dissnlocfin  22134  elptr2  22179  ptbasfi  22186  ptcld  22218  ptcldmpt  22219  ptclsg  22220  ptcnplem  22226  ptcnp  22227  cnmpt11  22268  cnmpt21  22276  cnmptcom  22283  imasnopn  22295  imasncld  22296  imasncls  22297  xkocnv  22419  elmptrab  22432  isfildlem  22462  alexsubALTlem3  22654  cnextfvval  22670  utopsnneiplem  22853  isucn2  22885  cfilucfil  23166  blval2  23169  restmetu  23177  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  ovoliunnul  24111  finiunmbl  24148  volfiniun  24151  iundisj  24152  iunmbl  24157  voliun  24158  iunmbl2  24161  mbfeqalem1  24245  mbfsup  24268  mbfinf  24269  mbflim  24272  itg2splitlem  24352  itg2split  24353  isibl2  24370  cbvitg  24379  itgeqa  24417  itgss3  24418  itgfsum  24430  itgabs  24438  itggt0  24447  itgcn  24448  limcmpt  24486  limciun  24497  dvmptfsum  24578  dvlipcn  24597  dvfsumlem2  24630  dvfsumlem4  24632  dvfsumrlim  24634  dvfsum2  24637  itgsubst  24652  coeeq2  24839  dgrle  24840  ulmss  24992  leibpi  25528  rlimcnp  25551  rlimcnp2  25552  o1cxp  25560  lgamgulmlem2  25615  lgamgulmlem6  25619  fsumdvdscom  25770  lgseisenlem2  25960  2sqmo  26021  2sqreulem4  26038  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  istrkg2ld  26254  mptelee  26689  gropd  26824  grstructd  26825  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1o  28150  ex-natded9.26  28204  isch3  29024  atom1d  30136  chirred  30178  sbc2iedf  30237  rspc2daf  30238  19.9d2r  30243  opreu2reuALT  30247  mo5f  30260  reuxfrdf  30262  eqrrabd  30272  foresf1o  30273  elabreximdv  30279  rabss3d  30285  iinabrex  30332  cbvdisjf  30334  disjorf  30342  disjabrex  30345  iundisjf  30352  disjunsn  30357  brabgaf  30372  ac6sf2  30384  dfimafnf  30395  fimarab  30404  2ndresdju  30411  fmptcof2  30420  acunirnmpt2  30423  acunirnmpt2f  30424  aciunf1lem  30425  aciunf1  30426  ofpreima  30428  funcnv5mpt  30431  funcnv4mpt  30432  fnpreimac  30434  padct  30481  cnvoprabOLD  30482  f1od2  30483  fpwrelmap  30495  xrofsup  30518  iundisjfi  30545  nnindf  30561  nn0min  30562  fprodex01  30567  fsumiunle  30571  gsummpt2d  30734  gsumhashmul  30741  isarchiofld  30941  elrspunidl  31014  fedgmullem2  31114  reff  31192  locfinreflem  31193  cmpcref  31203  zarclsiin  31224  zarcls  31227  zarcmplem  31234  ordtconnlem1  31277  qqhval2  31333  prodindf  31392  esumeq12dva  31401  esumeq2dv  31407  esumrnmpt  31421  esumpad  31424  esumpad2  31425  esumadd  31426  gsumesum  31428  esumlub  31429  esumsnf  31433  esumpr  31435  esumrnmpt2  31437  esumfzf  31438  esumfsup  31439  esumpcvgval  31447  esumpmono  31448  esumcocn  31449  hasheuni  31454  esumcvg  31455  esumgect  31459  esum2dlem  31461  esum2d  31462  esumiun  31463  ldsysgenld  31529  sigapildsyslem  31530  sigapildsys  31531  ldgenpisyslem1  31532  fiunelros  31543  measvunilem  31581  measvunilem0  31582  measvuni  31583  measiun  31587  measinblem  31589  voliune  31598  volfiniune  31599  volmeas  31600  ddemeas  31605  oms0  31665  omssubadd  31668  carsgclctunlem1  31685  carsggect  31686  omsmeas  31691  eulerpartlemgvv  31744  dstrvprob  31839  ballotlemodife  31865  reprsuc  31996  reprdifc  32008  breprexplema  32011  breprexplemc  32013  circlemethhgt  32024  hgt750lemd  32029  bnj919  32148  bnj1146  32173  bnj1379  32212  bnj1385  32214  bnj1400  32217  bnj1534  32235  bnj1542  32239  bnj110  32240  bnj121  32252  bnj124  32253  bnj130  32256  bnj207  32263  bnj571  32288  bnj605  32289  bnj580  32295  bnj607  32298  bnj611  32300  bnj873  32306  bnj849  32307  bnj900  32311  bnj916  32315  bnj1000  32323  bnj964  32325  bnj981  32332  bnj985v  32335  bnj985  32336  bnj1014  32343  bnj1123  32368  bnj1128  32372  bnj1228  32393  bnj1204  32394  bnj1279  32400  bnj1307  32405  bnj1321  32409  bnj1388  32415  bnj1398  32416  bnj1408  32418  bnj1417  32423  bnj1444  32425  bnj1445  32426  bnj1446  32427  bnj1449  32430  bnj1467  32436  bnj1489  32438  bnj1312  32440  bnj1497  32442  bnj1518  32446  bnj1525  32451  bnj1529  32452  cvmcov  32623  untsucf  33049  setinds2  33138  dfon2lem1  33141  dfon2lem3  33143  trpredmintr  33183  frpoinsg  33194  frpoins2g  33196  frinsg  33200  frins2g  33204  frins2  33205  nffrecs  33233  nosupbnd1  33327  nosupbnd2  33329  finminlem  33779  bj-nexdvt  34145  bj-cbvaldv  34236  bj-cbval2vv  34238  bj-cbvex2vv  34239  bj-cbvaldvav  34240  bj-cbvexdvav  34241  ax11-pm2  34274  bj-dvelimdv  34290  bj-nfeel2  34293  bj-ceqsalv  34334  bj-vtocl  34356  bj-inrab2  34370  currysetlem  34380  currysetlem1  34382  bj-opabco  34603  mptsnunlem  34755  exlimim  34759  exellim  34761  topdifinfindis  34763  topdifinffinlem  34764  icorempo  34768  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  finxpreclem2  34807  finxpreclem6  34813  fvineqsneu  34828  fvineqsneq  34829  wl-euequf  34975  wl-sb8eut  34978  wl-clelsb3df  35028  phpreu  35041  matunitlindflem2  35054  ptrest  35056  ptrecube  35057  poimirlem2  35059  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  heicant  35092  mbfposadd  35104  itgabsnc  35126  itggt0cn  35127  ftc1anclem5  35134  upixp  35167  indexa  35171  indexdom  35172  filbcmb  35178  sdclem2  35180  sdclem1  35181  fdc1  35184  totbndbnd  35227  sbcalf  35552  sbcexf  35553  scottexf  35606  scott0f  35607  eqrelf  35677  fsumshftd  36248  riotasv2d  36253  riotasv2s  36254  riotasv3d  36256  glbconxN  36674  pmapglbx  37065  pmapglb2xN  37068  cdleme26ee  37656  cdleme31sn  37676  cdleme31sn1  37677  cdlemefr29exN  37698  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme41sn3a  37729  cdleme32fva  37733  cdleme32d  37740  cdleme32f  37742  cdleme40m  37763  cdleme40n  37764  cdleme42b  37774  cdlemk36  38209  cdlemk38  38211  cdlemkid  38232  cdlemk19x  38239  cdlemk11t  38242  dihvalcqpre  38531  mapdheq  39024  hdmap1eq  39097  hdmapval2lem  39127  lcmineqlem9  39325  lcmineqlem12  39328  metakunt33  39382  mzpexpmpt  39686  eq0rabdioph  39717  rexrabdioph  39735  rexfrabdioph  39736  elnn0rabdioph  39744  dvdsrabdioph  39751  fphpd  39757  monotuz  39882  monotoddzz  39884  oddcomabszz  39885  setindtr  39965  dford4  39970  wdom2d2  39976  aomclem6  40003  aomclem8  40005  flcidc  40118  areaquad  40166  rababg  40273  ss2iundv  40361  cbviuneq12dv  40363  gneispace  40837  mnringvald  40921  mnringmulrcld  40936  nfscott  40947  scottabf  40948  scottab  40949  mnuprdlem4  40983  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  aaanv  41092  pm11.57  41093  pm11.58  41094  pm11.59  41095  pm11.71  41101  pm14.12  41125  ssralv2  41237  tratrb  41242  iunconnlem2  41641  evth2f  41644  elunif  41645  fvelrnbf  41647  evthf  41656  fnchoice  41658  sumpair  41664  rfcnnnub  41665  refsum2cn  41667  elabrexg  41675  uzwo4  41687  fiiuncl  41699  fiunicl  41701  elintdv  41715  ssd  41716  cbvmpo2  41733  cbvmpo1  41734  eliin2f  41740  eliuniin2  41755  cbvrabv2  41762  cbvrabv2w  41763  suprnmpt  41798  dffo3f  41806  disjf1  41809  disjrnmpt2  41815  disjf1o  41818  fompt  41819  disjinfi  41820  choicefi  41829  iunmapsn  41846  axccdom  41853  dmrelrnrel  41856  axccd  41861  funimassd  41863  fmptf  41875  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  rnmptbdlem  41893  rnmptbd  41894  upbdrech  41937  ssfiunibd  41941  supxrgere  41965  iuneqfzuzlem  41966  supxrgelem  41969  supxrge  41970  suplesup  41971  infrpge  41983  xralrple2  41986  infxr  41999  infxrunb2  42000  infleinf  42004  xrralrecnnle  42017  xrralrecnnge  42026  supxrunb3  42036  supxrleubrnmpt  42043  infleinf2  42051  unb2ltle  42052  rexabslelem  42055  rexabsle  42056  allbutfiinf  42057  suprleubrnmpt  42059  infrnmptle  42060  infxrunb3rnmpt  42065  uzublem  42067  uzub  42068  supminfrnmpt  42082  infxrpnf  42084  supxrleubrnmptf  42090  infxrgelbrnmpt  42093  infrpgernmpt  42104  supminfxr2  42108  monoordxr  42122  monoord2xr  42124  iccshift  42155  iooshift  42159  iooiinicc  42179  iooiinioc  42193  fsumclf  42211  fsummulc1f  42212  fsumnncl  42213  fsumsplit1  42214  fsumf1of  42216  fsumiunss  42217  fsumreclf  42218  fsumlessf  42219  fsumsermpt  42221  fmul01  42222  fmuldfeqlem1  42224  fmuldfeq  42225  fmul01lt1lem1  42226  fmul01lt1lem2  42227  fmul01lt1  42228  fprodsplit1  42235  fprodexp  42236  fprodabs2  42237  mccllem  42239  mccl  42240  fprodcnlem  42241  fprodcn  42242  climexp  42247  climsuse  42250  climrecf  42251  climinff  42253  climaddf  42257  mullimc  42258  ellimcabssub0  42259  islptre  42261  climf  42264  mullimcf  42265  rexlim2d  42267  idlimc  42268  limcperiod  42270  limcrecl  42271  sumnnodd  42272  islpcn  42281  limsupre  42283  limcleqr  42286  neglimc  42289  addlimc  42290  0ellimcdiv  42291  limclner  42293  climsubmpt  42302  climreclf  42306  climf2  42308  fnlimcnv  42309  climeldmeqmpt  42310  clim2f2  42312  climfveqmpt  42313  fnlimfvre  42316  allbutfifvre  42317  climleltrp  42318  fnlimf  42320  fnlimabslt  42321  climfveqmpt3  42324  climeldmeqf  42325  limsupref  42327  limsupbnd1f  42328  climbddf  42329  climeqf  42330  climeldmeqmpt3  42331  limsuplesup  42341  limsuppnfd  42344  limsupub  42346  limsupres  42347  climinf2lem  42348  climinf2  42349  limsuppnf  42353  limsupubuzlem  42354  limsupubuz  42355  climinf2mpt  42356  climinfmpt  42357  climinf3  42358  limsupmnflem  42362  limsupmnf  42363  limsupequz  42365  limsupre2  42367  limsupmnfuzlem  42368  limsupmnfuz  42369  limsupequzmptf  42373  limsupre3lem  42374  limsupre3  42375  limsupre3uzlem  42377  limsupre3uz  42378  limsupreuz  42379  limsupvaluz2  42380  limsupreuzmpt  42381  supcnvlimsup  42382  climuzlem  42385  climuz  42386  climisp  42388  lmbr3  42389  climrescn  42390  climxrrelem  42391  climxrre  42392  liminfcl  42405  liminfval2  42410  limsup10exlem  42414  liminflelimsuplem  42417  limsupgtlem  42419  limsupgt  42420  climliminflimsupd  42443  liminfreuzlem  42444  liminfreuz  42445  liminfltlem  42446  liminflt  42447  limsupub2  42454  xlimpnfxnegmnf  42456  liminflbuz2  42457  liminfpnfuz  42458  liminflimsupxrre  42459  xlimmnfvlem1  42474  xlimmnfvlem2  42475  xlimmnfv  42476  xlimpnfvlem1  42478  xlimpnfvlem2  42479  xlimpnfv  42480  xlimmnf  42483  xlimpnf  42484  xlimmnfmpt  42485  xlimpnfmpt  42486  climxlim2lem  42487  dfxlim2  42490  cncfshift  42516  icccncfext  42529  cncficcgt0  42530  cncfiooicc  42536  cncfioobd  42539  fprodcncf  42542  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  dvmptmulf  42579  dvnmptdivc  42580  dvnmul  42585  dvmptfprodlem  42586  dvmptfprod  42587  dvnprodlem1  42588  dvnprodlem2  42589  iblsplitf  42612  iblspltprt  42615  itgioocnicc  42619  iblcncfioo  42620  itgspltprt  42621  itgperiod  42623  stoweidlem3  42645  stoweidlem14  42656  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem26  42668  stoweidlem27  42669  stoweidlem28  42670  stoweidlem29  42671  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem36  42678  stoweidlem39  42681  stoweidlem42  42684  stoweidlem43  42685  stoweidlem44  42686  stoweidlem46  42688  stoweidlem48  42690  stoweidlem49  42691  stoweidlem50  42692  stoweidlem51  42693  stoweidlem52  42694  stoweidlem53  42695  stoweidlem54  42696  stoweidlem56  42698  stoweidlem57  42699  stoweidlem59  42701  stoweidlem60  42702  stoweidlem61  42703  stoweidlem62  42704  stoweid  42705  wallispilem3  42709  stirlinglem13  42728  stirling  42731  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem31  42780  fourierdlem39  42788  fourierdlem48  42796  fourierdlem51  42799  fourierdlem53  42801  fourierdlem68  42816  fourierdlem69  42817  fourierdlem71  42819  fourierdlem73  42821  fourierdlem77  42825  fourierdlem80  42828  fourierdlem81  42829  fourierdlem82  42830  fourierdlem83  42831  fourierdlem86  42834  fourierdlem87  42835  fourierdlem89  42837  fourierdlem91  42839  fourierdlem93  42841  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  elaa2  42876  etransclem18  42894  etransclem22  42898  etransclem23  42899  etransclem32  42908  etransclem35  42911  etransclem44  42920  etransclem46  42922  etransclem48  42924  rrndistlt  42932  ioorrnopnlem  42946  intsaluni  42969  salexct  42974  subsaliuncl  42998  sge00  43015  sge0revalmpt  43017  sge0sn  43018  sge0f1o  43021  sge0gerp  43034  sge0pnffigt  43035  sge0lefi  43037  sge0ltfirp  43039  sge0resrnlem  43042  sge0resplit  43045  sge0lempt  43049  sge0iunmptlemfi  43052  sge0p1  43053  sge0iunmptlemre  43054  sge0fodjrnlem  43055  sge0iunmpt  43057  sge0rpcpnf  43060  sge0ltfirpmpt2  43065  sge0isum  43066  sge0xp  43068  sge0ad2en  43070  sge0isummpt2  43071  sge0xaddlem1  43072  sge0xaddlem2  43073  sge0xadd  43074  sge0pnffsumgt  43081  sge0gtfsumgt  43082  sge0uzfsumgt  43083  sge0seq  43085  sge0reuz  43086  sge0reuzb  43087  iundjiun  43099  meadjiunlem  43104  meadjiun  43105  ismeannd  43106  voliunsge0lem  43111  meaiuninclem  43119  meaiunincf  43122  meaiuninc3v  43123  meaiuninc3  43124  meaiininclem  43125  meaiininc  43126  meaiininc2  43127  caragenfiiuncl  43154  omeiunltfirp  43158  carageniuncllem1  43160  carageniuncllem2  43161  caratheodorylem2  43166  0ome  43168  isomenndlem  43169  hoicvrrex  43195  ovnsupge0  43196  ovnlecvr  43197  ovnlerp  43201  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  ovnsubaddlem2  43210  hoidmvcl  43221  hsphoidmvle2  43224  hsphoidmvle  43225  hoidmvval0  43226  sge0hsphoire  43228  hoidmvval0b  43229  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem1  43240  ovnhoilem2  43241  ovnhoi  43242  ovnlecvr2  43249  hspdifhsp  43255  hoidifhspdmvle  43259  hoiqssbllem3  43263  hspmbllem1  43265  hspmbllem2  43266  opnvonmbllem1  43271  opnvonmbllem2  43272  ovnsubadd2lem  43284  ovolval5lem1  43291  ovnovollem1  43295  ovnovollem2  43296  hoimbl2  43304  vonhoire  43311  iinhoiicclem  43312  iinhoiicc  43313  iunhoiioolem  43314  iunhoiioo  43315  vonioolem1  43319  vonioolem2  43320  vonioo  43321  vonicclem1  43322  vonicclem2  43323  vonicc  43324  vonn0ioo2  43329  vonn0icc2  43331  vonct  43332  pimltmnf2  43336  pimgtpnf2  43342  salpreimagelt  43343  salpreimalegt  43345  pimltpnf2  43348  pimgtmnf2  43349  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  preimageiingt  43355  preimaleiinlt  43356  salpreimagtge  43359  salpreimaltle  43360  salpreimalelt  43363  salpreimagtlt  43364  issmff  43368  sssmf  43372  mbfresmf  43373  cnfsmf  43374  incsmflem  43375  incsmf  43376  smfsssmf  43377  issmflelem  43378  issmfle  43379  smfconst  43383  issmfgtlem  43389  issmfgt  43390  smfpimltxrmpt  43392  smfmbfcex  43393  smfaddlem1  43396  smfaddlem2  43397  smfadd  43398  decsmflem  43399  decsmf  43400  smfpreimagtf  43401  issmfgelem  43402  issmfge  43403  smflimlem2  43405  smflimlem4  43407  smflim  43410  smfpimgtxr  43413  smfpimgtxrmpt  43417  smfpimioo  43419  smfresal  43420  smfrec  43421  smfres  43422  smfmullem2  43424  smfmullem4  43426  smfmul  43427  smfpimbor1lem2  43431  smf2id  43433  smfco  43434  smflim2  43437  smfpimcc  43439  smflimmpt  43441  smfsuplem1  43442  smfsuplem3  43444  smfsup  43445  smfsupmpt  43446  smfsupxr  43447  smfinflem  43448  smfinf  43449  smfinfmpt  43450  smflimsuplem3  43453  smflimsuplem4  43454  smflimsuplem5  43455  smflimsuplem7  43457  smflimsuplem8  43458  smflimsup  43459  smflimsupmpt  43460  smfliminflem  43461  smfliminf  43462  smfliminfmpt  43463  or2expropbilem1  43624  or2expropbilem2  43625  or2expropbi  43626  rexsb  43654  reuf1odnf  43663  2reu8i  43669  ffnafv  43727  tz6.12c-afv2  43798  f1oresf1o2  43847  iccelpart  43950  iccpartdisj  43954  dfich2  43975  ichbi12i  43977  ichnfimlem  43980  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990  sprsymrelfo  44014  reupr  44039  reuopreuprim  44043  mogoldbb  44303  2zrngagrp  44567  2zrngmmgm  44570  opeliun2xp  44734  cbvmpox2  44737  ovmpordx  44741  1arymaptfo  45057  2arymaptfo  45068  nfintd  45203  nfiund  45204  nfiundg  45205  iunord  45206  spcdvw  45209  nfsetrecs  45216  setrec1lem2  45218  setrec1  45221  setrec2fun  45222  aacllem  45329