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?
On
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)$$
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)$$