I have come across this variant of the implicit function theorem in the book "Topics in Nonlinear Functional Analysis" by Ralph A. Artino.
Theorem 2.7.2 (Implicit Function Theorem) Let $X, Y$, and $Z$ be Banach spaces and $f$ a continuous mapping of an open set $U \subset X \times Y \rightarrow Z$. Assume that $f$ has a Frechet derivative with respect to $x, f_x(x, y)$, which is continuous in $U$. Let $\left(x_0, y_0\right) \in U$ and $f\left(x_0, y_0\right)=0$. If $A=f_x\left(x_0, y_0\right)$ is an isomorphism of $X$ onto $Z$ then:
- (i) There is a ball $\left\{y:\left\|y-y_0\right\|<r\right\}=B_r\left(y_0\right)$ and a unique continuous map $u: B_r\left(y_0\right) \rightarrow X$ such that $u\left(y_0\right)=x_0$ and $f(u(y), y) \equiv 0$.
- (ii) If $f$ is of class $C^1$, then $u(y)$ is of class $C^1$ and $$ u_y(y)=-\left[f_x(u(y), y)\right]^{-1} \circ f_y(u(y), y) . $$
- (iii) $u_y(y)$ belongs to $C^p$ if $f$ is in $C^p, p>1$.
My main interest is in part (i), which I need for a proof. What confuses me, and I wanted to check, was that this version of the Implicit Function Theorem seems to require no differentiability of $f$ with respect to $y$... is this correct?! I cannot find another version with such relaxed conditions anywhere. It seems the theorem always usually requires differentiability on both $x$ and $y$, no?
Update: The book cites another paper found here as a reference for the implicit function theorem but this paper does not prove it and instead states:
This theorem is certainly well-known, but we did not find a convenient reference for the precise statement we have used.
Another update: I found the version of the proof I was looking for here (pdf link).