Is there a formal difference between $f:X \to X$ and $f\in X \to X$?
No, they're mostly notational variations. There are different connotations to the different notations, and different notations are common in different fields where they can mean quite different things. Also, sometimes they are used in a particular context for different (but usually related) things. You'll, of course, have to see how it has been defined in that context.

Any use of $\in$ usually strongly suggests a set-theoretic context (though you occasionally see it in a type-theoretic context). The $f:X\to Y$ notation was, I believe, popularized in mathematics by category theory. In this case, it means $f\in\mathsf{Hom}(X,Y)$. This is compatible with $f\in Y^X$ in the case that the category is the category of sets and functions. In a general categorical context, $Y^X$ is usually reserved for exponential objects for which it makes no sense to ask if $f\in Y^X$, though you (usually) can ask if there is an arrow $1 \to Y^X$.

In logic, when $X$ and $Y$ are sorts, usually $f:X\to Y$ means that $f$ is a function symbol. In this case, $X$ and $Y$ aren't sets and neither is $X \to Y$. It makes no sense to say $f\in X\to Y$ unless $\in$ isn't being thought of as set membership or we want to say $X\to Y$ means the set of function symbols from $X$ to $Y$. This latter view starts to get rather similar to the categorical view.

In type theory, usually $f:X\to Y$ means something like $f$ has type $X\to Y$ and $X\to Y$ is the type of functions from $X$ to $Y$. Types are not sets and part of the purpose of this notation is to remind one of that fact. Indeed, types are more like sorts and this notation is similar to how it is used in logic. Sometimes $Y^X$ is also used where $Y^X$ is used in a more first-class sense in a way that is compatible with the similar distinction I mentioned for category theory, so we might write $X\to Z^Y$ rather than $X\to(Y\to Z)$. Sometimes no distinction is being made and the notation is completely synonymous and the choice is made purely for typographical reasons. For computer programming, the choice is mostly typographical, f : X -&gt; Y is easier to write and easier to read, though programming languages are also closely related to type  theories.

It doesn't really make sense to talk about which of these notations is "more fundamental" than the others in general. That said, the $f:X\to Y$ notation is usually making the least commitments if multiple notations are in use. Often $f:X\to Y$ isn't a proposition with a truth value, so it wouldn't make much sense to write $\{f\mid f:X\to Y\}$. Admittedly, in the context where it isn't a proposition, you usually aren't using set theory. If you really wanted to, you could meta-theoretically write $\{t\mid \cdot\vdash t:X\to Y\}$ to mean the set of closed terms of type $X\to Y$, say. This would have nothing to do with a set of functions though.