Shauder basis for Hilbert spaces

[cianfa72]

TL;DR

About the existence of Shauder or Hilbert basis for separable Hilbert spaces.

Consider the Hilbert space on $\mathbb C$ of square integrable functions of one variable $L^2(\mathbb R)$. As claimed in a recent thread in QM subforum, there exists a "good" Hilbert basis for it given by the set of Hermite functions defined on $\mathbb R$. This set is countable hence $L^2(\mathbb R)$ is separable infinite-dimensional Hilbert space.

I know that, by Zorn's lemma (equivalent to Axiom of Choice/AC), it can be shown that any vector space has an Hamel/algebraic basis. For Hilbert spaces we can go further and prove the existence of maximal orthonormal sets. Then, by using the completeness property of Hilbert spaces, prove that any of such maximal orthonormal sets is actually a Shauder basis (i.e. an Hilbert basis). So far so good.

In the specific case of $L^2(\mathbb R)$ we're able to exhibit an Hilbert basis (Hermite functions) so, even if one doesn't include AC is the underlying set theory, there is a "constructive" proof/evidence for its existence. Now all separable infinite dimensional Hilbert spaces are unitarily isomorphic to $l^2(\mathbb N)$ and so to $L^2(\mathbb R)$.

Does this mean that any separable Hilbert space admits a Shauder basis even though it can't be proven by discarding AC from the underlying set theory?