different domains for each variable in predicate logic Before I begin, note that this is significantly outside what I've studied, so if it's a load of crap just let me know.
Up till now, everything I've covered assumes the same domain for all variables.
I'm trying to define an arbitrary one-to-one relationship between elements in two different sets, and want each of the variables x and y in the formula below to be in the domain of its particular set:

X = {X1, X2, X3}
Y = {Y1, Y2, Y3}

That is, I want:

x ∈ X, y ∈ Y

If possible, how would I go about specifying this?
Also, I've phrased the formula

∀x ∃y [ A(x, y) ∧ ¬A(¬x, y) ]

Where A(x, y) indicates an relationship between x and y. Is this statement well formed? Particularly the ¬x in ¬A(¬x, y)? And does it mean what I think it means - That A(x, y) for all x ∈ X except the x in question, and for the y in question, must be false in order for the statement ot be true? That is, does it define a one-to-one relationship?
Thanks a lot,
Wyatt
 A: No, I don't think it makes sense to write $\neg x$ in this context. 
The simplest way to specify that $x\in X$ and $y\in Y$ is to make them clauses in your statement. For example, to write that for every $x\in X$ there should exist a $y\in Y$ such that $A(x,y)$ holds, you would usually write:

$$\forall x \left(x\in X\rightarrow \exists y(y\in Y\wedge A(x,y)\right).$$

For the second part: to say that no other $z\in X$ will also be associated to $y$, the easiest why is to say that anyone who is associated to $y$ is going to be equal to $x$; so you would want a clause $A(z,y)\rightarrow x=z$.
To put it all together:

$$\forall x\left( x\in X\rightarrow \exists y(y\in Y\wedge A(x,y)\wedge \forall z(z\in X\wedge A(z,y)\rightarrow x=z))\right).$$

It is also possible to use common (but perhaps slightly abusive) notation and write

$$\forall x\in X\Bigl(\exists y\in Y\Bigl(\forall z\in X\Bigl(A(x,y)\wedge (A(z,y)\rightarrow x=z)\Bigr)\Bigr).$$

Added: As noted in several comments, the above does not completely describe a one-to-one function; it only describes a relation with domain $X$, codomain $Y$, such that for each $y\in Y$ there is at most one $x\in X$ such that $A(x,y)$ holds; this does not fully describe a function (unless you happen to know some other things about $X$ and $Y$, e.g., that they are both finite and of equal size, in which case the other condition will follow), nor a bijective function. In general, the clause you want for "function-ness" is the dual of the condition you have: for all $x\in X$, and for all $y\in Y$, $A(x,y)\wedge A(x,y')\rightarrow y=y'$ (so each input has at most one output). For bijectivity (so you have a true correspondence) you also need that for all $y\in Y$ there exists $x\in X$ such that $A(x,y)$. 
A: It seems to me what you're trying to do is formulate a first-order theory. This has non-logical axioms. Your theory uses two one-place predicates, say "F" for the Xs and "G" for the Ys. It has one non-logical axiom, perhaps, which says there are Fs and there are Gs. Then it has another which says nothing is both F and G. Then you have a two-place predicate "R" to represent the relationship, and another non-logical axiom for that, one that uses "F" and "G" as well as "R". From the point of view of logic, there's still only one domain; it's your non-logical axioms that divide it up. -- It's the predicates and axioms that are important, not the variables "x" and "y". Shoenfield's text Mathematical Logic is good for examples of first-order theories.
Edit: by non-logical axiom I mean an axiom that's not itself already provable in first-order logic.
A: There are lots of ways to write a formula A(x,y) that defines a bijection between two sets. If you're trying to keep the depth of quantifiers to a minimum, you could use
$$
\begin{align}
&  (\forall x)(\exists y) [ x \in X \to y \in Y \land A(x,y)] \\
& {} \land (\forall y)(\exists x) [ y \in Y \to x \in X \land A(x,y)]\\
& {} \land (\forall x,x',y,y') ([x \in X \land y \in Y) \\
& \qquad {} \to [(A(x,y) \land A(x',y) \to x=x'] 
 \land [A(x,y) \land A(x,y') \to y = y'])]\\
\end{align}
$$
This can be written more elegantly with the abbreviations $(\forall x \in X) $ and $(\exists x \in X)$:
$$
\begin{align}
(\forall x \in X)\Phi &\equiv (\forall x) [ x \in X \to \Phi] \\
(\exists x \in X)\Phi &\equiv (\exists x) [ x \in X \land \Phi] \\
\end{align}
$$
like so: 
$$
\begin{align}
&  (\forall x \in X)(\exists y\in Y) A(x,y) \land (\forall y \in Y )(\exists x \in X) A(x,y)\\
& {} \land (\forall x \in X)(\forall x' \in X)(\forall y \in Y)(\forall y' \in Y)([(A(x,y) \land A(x',y) \to x=x'] \\
& \qquad \qquad {} \land [A(x,y) \land A(x,y') \to y = y'])\\
\end{align}
$$
