Here are a few different ways of defining the same predicate:
$$\forall x, y \in \mathbb{R}, P(x, y): x = y \tag{1}$$
$$P(x, y): x = y \text{, where $x$ and $y$ are real numbers} \tag{2}$$
$$\text{Let $x$ and $y$ be real numbers. }$$ $$P(x, y): x = y \tag{3}$$
Are there any problems with any of them? Is there a preferred way among mathematicians/logicians? Or does it come down mostly to subjective preference?
I'm especially curious about $(1)$, and whether it's okay to put a quantifier in front of a predicate like that, as I haven't seen it done much.
I, personally, would do $(2)$ out of those options. Though I'd probably say something like "Define $P(x,y)$ ...".
$(3)$ doesn't make sense at all. It reads as you are picking a particular $x$ and $y$ and asserting that $P(x,y)$ is equivalent to $x=y$ for that particular $x$ and $y$. It would not at all follow that $P(1,1)$ should (or should not) hold.
The most natural thing when defining a predicate (or function) is to view it as a binding form.1 Saying "Define $P(x,y)$ to be ..." binds $x$ and $y$ in the body of the definition. As such, you could just say, "Define $P(x,y)$ to be $x=y$." Depending on what you mean by "where $x$ and $y$ are real numbers", this may be appropriate in a multi-sorted logic or a type theory to indicate the sort/type of $P$. In typical set theories, it would appear that what you'd actually want is to define $P(x,y)$ as $x\in\mathbb R\land y\in\mathbb R\land x = y$. Alternatively, you may mean for $P(x,y)$ to be defined as $x=y$ for real numbers but arbitrary for other inputs. This should be handled differently since you are not actually (fully) defining $P$, see below.
From this perspective, $(1)$ doesn't make sense because $P(x,y)$ binds $x$ and $y$. The $\forall$ would be talking about different $x$ and $y$. Also, this isn't a formula, so using formal notation is misleading. Typically definitions are happening at a meta-logical level.
Now in understanding definitions, we can think of them as adding predicate symbols ($P$ in this case) and then axioms (or assumptions), e.g. $\forall x,y.P(x,y)\leftrightarrow x = y$. Here $\forall x,y.P(x,y)\leftrightarrow x = y$ is a formula. Stating this formula as an axiom or assuming it presupposes $P$ is a predicate symbol, so is not in itself definitional.
This two-step process can be useful. Let's say we did want $P(x,y)$ to be $x=y$ when $x\in\mathbb R$ and $y\in\mathbb R$ but otherwise unconstrained. You could go about that as follows. First, assert $P$ is a predicate: "Let $P$ be a binary predicate symbol." Then constrain it, but with an axiom/assumption that doesn't fully specify it: "Assume $\forall x,y\in\mathbb R.P(x,y)\leftrightarrow x=y$."
(As a minor note, I'd prefer $P(x,y):\equiv\dots$ or $P(x,y):\leftrightarrow\dots$ to $P(x,y) : \dots$ [and $f(x,y):=\dots$ for functions]. Definition is an asymmetric operation, so it's nice for the notation to indicate that. As indicated above, the definitions lead to assertions of equivalences/equalities and this notation suggests that as well and makes it clear which. Most commonly, definitions are just written as equivalence/equalities and the surrounding text explains that they are definitional.)
1 This is how definitions of functions and other things work in virtually all programming languages.