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?

Establish Domain and Codomain:
$$\forall y~ \forall x~ F(x) = y \implies (x \in A \land y \in B)$$
Surjection:
$$\forall y \in B ~ \exists x ~F(x)=y$$
Injection:
$$\forall y ~ \forall x_1 ~ \forall x_2 ~ (F(x_1) = y \land F(x_2) = y) \implies (x_1 = x_2)$$
