Writing out a (set) relation in terms of predicate logic Revisiting some elementary binary relations on $\mathbb{R}$ while studying predicate logic (at a graduate level), I wanted to receive some criticism on the following thoughts I have.

Lets take a look at this binary relation (that is a function) on $\mathbb{R}$ such that $x,y \in \mathbb{R}$:
$f :=$ {$(x,y)| y = x^{2}$}. Since we know that a relation is just a predicate of two variables (or "subjects", if you will) that produces a truth value, couldn't we write the  relation $f$ as the following  assuming I was a student who had never taken set theory (but knew that $x$ and $y$ are real numbers in the proposition $f(x,y)$)? That is, knowing that “is the square of” is the predicate $f$ where $x$ and $y$ are the subjects:
$f(x,y) :=$ $y$ is the square of $x$
Since a course in the logic of propositions and predicates is usually taken before set theory at my university, I feel like this would occur naturally as an example. Of course, reoccurring later in a set theory course as $f :=$ {$(x,y)| y = x^{2}$} where the proposition $f(x,y)$ is rewritten (set-theoretically) as $y = f(x):= x^{2}$.
 A: I think there are some subtleties that can be unpacked here.
In the context of first-order logic; "$y$ is the square of $x$" is an informal describtion of the relation you want to have. This is fine, as long as you can justfy it with a formal describtion.
In your question, we find ourselfs in the context of the real numbers. A first-order language for $\mathbb{R}$ would surely provide us with the symbols "$\cdot$" and "$=$", so we could properly state the relation as:
$$
f(x,y) := (x \cdot x = y)
$$
which is then a relation in the first-order language of $\mathbb{R}$.
In set theory we can realize the relation as a set by using the axiom of specifictiation
$$
F := \{(x,y) \mid x \cdot x =y~\}
$$
Now one can be nitpicky here as well. The linked article mentions that the specifying formula on the right (in this case $x \cdot x =y$) has to be a formula in the language of set theory. So the above is only jsutified if "$\cdot$" was at some point defined by a formula in the language of set-theory.
But to answer your question:

Couldn't we write the relation $f$ as the following [...] ?

Yes that is completely fine. Everything mentioned above are only very technical nitpicks that rarely come up and do not pose unsurmountable problems.

There is one bit of notation you used, that you do have to be carefull about.

[...] where the proposition $f(x,y)$ is rewritten (set-theoretically) as $y=f(x):=x^2$.

Not every binary relation is a function. The notation $f(x) = y$ is only used when $f$ is a functional relation. With your definition, $f$ indeed turns out to be functional. However, if we were to define
$$
g(x, y) := x \text{ is the square of } y 
$$
Then $g$ would not be functional, since for example $g(4,2) ~\land~ g (4 ,-2)$ but $2 \neq -2$. So we can not write something like $g(4) = 2$.
