Quantify in logic over elements of cartesian product such that they fulfill specifc properties

Question

Say I have a structure $\mathcal{A} = (A \times A, <', =')$ and $A$ is a totally ordered, countably-infinite set and the interpretation of $<'$ and $='$ are such that $A \times A$ is a total order as well.
I want to axiomatize this given structure as a specific first order theory (or in MSO), where I have to quantify over elements that have a specific property, in concreto something like this: $\forall(x,x): P(x)$ with $x \in A$.
Those elements exist but is it possible to access them via first order logic or MSO?

Answer 1

This is mostly a Comment.

You can have $\forall x$ , you can have $\forall(x,y)$ , you can not have $\forall(x,x)$

Instead you can try something like this :
$\forall x \in A : (x,x) \in \mathbb{A} \land P(x)$

In Case , not all the $x$ values are valid & you want a Sub-Set with the validity , you can try something like this :
$X = \{ \ x \ | \ x \in A \land (x,x) \in \mathbb{A} \land P(x) \ \}$ : gives Sub-Set of $A$
$Y = \{ \ (x,x) \ | \ x \in A \land (x,x) \in \mathbb{A} \land P(x) \ \}$ : gives Sub-Set of $\mathbb{A}$