How can we express the statement "$f$ is a bijection from $A$ to $B$" in predicate logic? How can we express the statement

$f$ is a bijection from $A$ to $B$

in predicate logic? Can it be expressed in first-order logic?
A problem seems to be that the sets $A$ and $B$ are different sets, while predicate logic applies to a single set. Is that correct?

Let $R(x,y)$ be the relation "$f(x)=y$", then we want,
To express that $f$ is defined everywhere in its domain:
$$\forall x( x\in A \implies\exists y R(x,y) \land y\in B)$$
To express that for a function $f$, each input can only have one output:
$$\forall x \forall y \forall z (x\in A \land y \in B \land z\in B \land R(x,y) \land R(x,z)\implies y=z)$$
To expression the one-to-oneness of $f$:
$$\forall x \forall y \forall z (x\in A \land y \in A \land z\in B \land R(x,z) \land R(y,z)\implies x=y)$$
To express that $f$ is onto:
$$\forall y( y\in B \implies\exists x R(x,y) \land x\in A)$$
